2022-05-16 17:40:01 +02:00
|
|
|
|
# pi
|
2022-07-21 00:05:45 +02:00
|
|
|
|
|
2022-05-16 17:40:01 +02:00
|
|
|
|
A dependently typed system
|
|
|
|
|
|
|
2022-07-21 00:05:45 +02:00
|
|
|
|
# Implemented
|
|
|
|
|
|
|
|
|
|
|
|
* A Basic dependent lambda calculus
|
|
|
|
|
|
* lambda abstractions
|
|
|
|
|
|
* variables
|
|
|
|
|
|
* pi types
|
|
|
|
|
|
* type of types
|
|
|
|
|
|
|
2022-07-21 19:51:55 +02:00
|
|
|
|
* let ... in ...
|
|
|
|
|
|
|
2022-07-21 00:05:45 +02:00
|
|
|
|
* Unit type
|
|
|
|
|
|
|
|
|
|
|
|
* Empty type
|
|
|
|
|
|
|
|
|
|
|
|
* Natural numbers
|
|
|
|
|
|
|
2022-07-21 04:20:20 +02:00
|
|
|
|
* Σ Types
|
|
|
|
|
|
|
2022-07-28 04:47:54 +02:00
|
|
|
|
* Martin-Löf Identity types
|
2022-05-16 17:40:01 +02:00
|
|
|
|
|
2022-07-28 04:47:54 +02:00
|
|
|
|
# TODO
|
2022-07-21 19:51:55 +02:00
|
|
|
|
|
2022-07-26 06:11:57 +02:00
|
|
|
|
* Universes
|
|
|
|
|
|
|
2022-07-28 04:47:54 +02:00
|
|
|
|
* Elaboration
|
|
|
|
|
|
* Implicit arguments
|
|
|
|
|
|
* Universe family application
|
|
|
|
|
|
|
|
|
|
|
|
* Inductives
|
|
|
|
|
|
* Indexed inductives
|
|
|
|
|
|
|
|
|
|
|
|
## Things that could be fun to do sometime eventually
|
|
|
|
|
|
|
|
|
|
|
|
* Pattern matching in elaborator
|
2022-05-16 17:40:01 +02:00
|
|
|
|
|
2022-07-28 04:47:54 +02:00
|
|
|
|
* Write down the rules
|
2022-07-21 00:05:45 +02:00
|
|
|
|
|
2022-07-28 04:47:54 +02:00
|
|
|
|
* Performence optimisation?
|
2022-07-21 00:05:45 +02:00
|
|
|
|
|
2022-07-21 19:51:55 +02:00
|
|
|
|
* Compile to scheme
|
|
|
|
|
|
|
2022-05-16 17:49:56 +02:00
|
|
|
|
# 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
|
