pi/README.md

# 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
-												add readme

											
										
										
											2022-05-16 17:40:01 +02:00
+								# pi
-												implemented types ⊤, ⊥, and ℕ

											
										
										
											2022-07-21 00:05:45 +02:00
-												add readme

											
										
										
											2022-05-16 17:40:01 +02:00
+								A dependently typed system
-												implemented types ⊤, ⊥, and ℕ

											
										
										
											2022-07-21 00:05:45 +02:00
+								# Implemented
 								* A Basic dependent lambda calculus
 								  * lambda abstractions
 								  * variables
 								  * pi types
 								  * type of types
-												added let ... in ...

											
										
										
											2022-07-21 19:51:55 +02:00
+								* let ... in ...
-												implemented types ⊤, ⊥, and ℕ

											
										
										
											2022-07-21 00:05:45 +02:00
+								* Unit type
 								* Empty type
 								* Natural numbers
-												added Σ types to readme also

											
										
										
											2022-07-21 04:20:20 +02:00
+								* Σ Types
-												updated readme

											
										
										
											2022-07-28 04:47:54 +02:00
+								* Martin-Löf Identity types
-												add readme

											
										
										
											2022-05-16 17:40:01 +02:00
-												update expectations in readme

											
										
										
											2022-08-22 20:49:49 +02:00
+								# Lacking
-												added let ... in ...

											
										
										
											2022-07-21 19:51:55 +02:00
-												update expectations in readme

											
										
										
											2022-08-22 20:49:49 +02:00
+								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
-												update readme

											
										
										
											2022-07-26 06:11:57 +02:00
-												updated readme

											
										
										
											2022-07-28 04:47:54 +02:00
+								* Elaboration
 								  * Implicit arguments
 								  * Universe family application
-												update readme

											
										
										
											2022-07-28 15:46:00 +02:00
+								    * Syntax level russel universes
 								    * Universe of all other universes? (universe polymorphism)
-												updated readme

											
										
										
											2022-07-28 04:47:54 +02:00
-												add some references to useful material in the readme

											
										
										
											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