1022 B

Raw Blame History

pi

A dependently typed system

Implemented

A Basic dependent lambda calculus
- lambda abstractions
- variables
- pi types
- type of types
let … in …
Unit type
Empty type
Natural numbers
Σ Types
Martin-Löf Identity types

TODO

Universes (a la tarksi)
Elaboration
- Implicit arguments
- Universe family application
  - Syntax level russel universes
  - Universe of all other universes? (universe polymorphism)
Inductives
- Indexed inductives

Things that could be fun to do sometime eventually

Pattern matching in elaborator
Write down the rules
Performence optimisation?
Compile to scheme

References

Some of the material I found helpful in groking dependent type checking:

Coquand, Thierry. “An Algorithm for Type-Checking Dependent Types.” Science of Computer Programming 26, no. 1–3 (May 1996): 167–77. https://doi.org/10.1016/0167-6423(95)00021-6.
Brady, Edwin. “SPLV20 course notes”. GitHub. https://github.com/edwinb/SPLV20