Comment by LightMachine
12 hours ago
There 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!)
Does Bend have linear types? I didn't see anything on them in a quick skim of the GUIDE file.
the entire language is based on linear types! it says so in the GUIDE yes
Ah, thanks, was looking at the readme instead of the guide
Thank you.