3 ms·
I think the author's title is kind of misleading. The lambda calculus is simple. It consists of only four essential things, and with those four things we can c
by DonaldPShimoda 3y ago
I think the author's title is kind of misleading.
The lambda calculus is simple. It consists of only four essential things, and with those four things we can compute anything that is computable. (I don't claim that the lambda calculus is simple to understand — certainly there are people who have a hard time grasping it. But that's a different issue.)
What the author is doing is not "the lambda calculus"; it's an extended lambda calculus for dependent types. That's a huge step in terms of complexity. Yes, it might be the simplest lambda calculus for the task (I didn't check), but that is not at all "how to keep lambda calculus simple". Just a very odd choice for a title, in my opinion.
- solomonb 3y agoThe Author is _not_ implementing dependent types. They specifically are implementing Simply Typed Lambda Calculus. They have stripped out the Pi and Sigma types from the original paper.
- dunham 3y agoThe original paper also does plain STLC first in section 2, and then adds dependent types in section 3. (And finally it adds the naturals in section 4.) In the Idris2 github repository, Guillaume Allais goes a step further and shows a well-named version. There the types of terms and values are indexed by the list of names in the environment and the compiler checks that the manipulation of deBruin levels and indices is correct: https://github.com/idris-lang/Idris2/blob/main/libs/papers/Language/IntrinsicScoping/TypeTheory.idr https://github.com/idris-lang/Idris2/blob/main/libs/papers/L...