Hacker News Reader

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)

View on HN

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.

Maybe you can explain or give a hint, why a function that never returns could prove anything?

Reply on news.ycombinator.com