Browse files


  • Loading branch information...
1 parent bb868ec commit abab9f12403863a7194c311ece233451fb70f1db @andrejbauer andrejbauer committed Nov 7, 2012
Showing with 23 additions and 2 deletions.
  1. +23 −2 README.markdown
25 README.markdown
@@ -1,11 +1,18 @@
-A minimalist implementation of type theory with universes and dependent products. The
-concrete syntax is as follows:
+A minimalist implementation of type theory in fewer than 500 lines of Ocaml code,
+including comments.
+## The type theory
+The dependent type theory `tt` has the following ingridients:
* The universes are `Type 0`, `Type 1`, `Type 2`, ...
* A dependent product is written as `forall x : T1, T2`
* A function is written as `fun x : T => e`
* Application is written as `e1 e2`
+The hierarchy of universes is not commulative, i.e., even though `Type k` has type `Type
+(k+1)`, `Type k` is *not* a subuniverse of `Type (k+1)`.
## Compilation
You need `ocamlbuild` and `make`. You can type
@@ -60,3 +67,17 @@ The code is meant to be short and sweet, and close to how type theory is present
paper. Therefore, it is not suitable for a real implementation, as it will get horribly
inefficient as soon as you try anything complicated. But it should be useful for
+## What experiments should I perform to learn more?
+There are many things you can try, for example:
+* basic types `unit`, `bool` and `nat`
+* the eta rule for functions
+* dependent sums
+* de Bruijn indices
+* cummulative universes, so that [A : Type k] implies [A : Type (k+1)]
+* better type inference so that variables need not be explicitly typed
+* flexible syntax, e.g., allow `fun x y : nat => ...` instead of `fun x : nat => fun y : nat => ...`
+* prefix and infix operators

0 comments on commit abab9f1

Please sign in to comment.