2 ms·
The Author is _not_ implementing dependent types. They specifically are implementing Simply Typed Lambda Calculus. They have stripped out the Pi and Sigma types
by solomonb 3y ago
The 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...