52 lines
1.1 KiB
Markdown
52 lines
1.1 KiB
Markdown
# 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
|
||
|
||
# Lacking
|
||
|
||
Here are some things which are *not* present but could be.
|
||
|
||
This project has served me well by teaching me about typechecking dependently typed systems. It's likely that the features listed below will not be implemented as I'll move onto other projects and learn more about elaboration.
|
||
|
||
|
||
* Universes
|
||
* a la tarksi
|
||
|
||
* Inductives
|
||
* W types
|
||
* Indexed inductives
|
||
|
||
* Elaboration
|
||
* Implicit arguments
|
||
* Universe family application
|
||
* Syntax level russel universes
|
||
* Universe of all other universes? (universe polymorphism)
|
||
|
||
# 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
|