3 ms·
Could you recommed literature (preferrably a single book) that does not require prior knowledge and allows to fully understand the logical foundation of it? (W
by avodonosov 17d ago
Could you recommed literature (preferrably a single book) that does not require prior knowledge and allows to fully understand the logical foundation of it?
(Why it is done the way it is, what problems are solved by affinity, why closure can be called at most once, how a function that never returns can prove anything, and everything else)
- LightMachine 17d agoThere isn't a single book that covers all of it... Bend's theory touches various domains (dependent types, substructural types, termination). And then there's the runtime, compiler, GPU kernels... If you mean about the type theory specifically, "Type Theory and Formal Proof by Nederpelt and Geuvers" is a good introduction. Not sure what I'd recommend on linear types, no book I know of is very introductory? Perhaps "Idris 2: Quantitative Type Theory in Practice", which is a language with similar foundations to Bend, and the author wrote a book on it (and inspired myself!)
- avodonosov 17d agoThank you.
- avodonosov 17d agoMaybe you can explain or give a hint, why a function that never returns could prove anything?
- alew1 17d agoDoes Bend have linear types? I didn't see anything on them in a quick skim of the GUIDE file.
- LightMachine 17d agothe entire language is based on linear types! it says so in the GUIDE yes
- alew1 17d agoAh, thanks, was looking at the readme instead of the guide