add README

1 files changed, 40 insertions, 0 deletions

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..9a9f6c9
--- /dev/null
+++ b/README.md
@@ -0,0 +1,40 @@
+# toytt
+
+this is an attempt of mine to implement a typechecker for a minimal dependent
+type theory in the style of martin-löf. at the time of writing this, it has the
+following features:
+
+- type of booleans w/ dependent eliminator
+- pi and sigma connectives
+- universe that contains itself (lol)
+- that's it
+
+it probably has lots of bugs as well.
+
+## example
+
+```
+$ dune exec toytt
+(\b -> bool-elim b at x -> bool [ true => false, false => true ] :: (b : bool) -> bool) false
+true : bool
+```
+
+at the moment the interface is a broken REPL which exits if you make a mistake
+(TODO). the above example illustrates the syntax for lambdas, boolean
+intro & elim, inline type annotations (`::`) and pi types with the boolean
+not-function applied to `false` (which evaluates to `true`).
+
+## todo list (in descending order of importance and/or realizability)
+
+- figure out how to recover variable names in pretty-printing so we don't
+  have to print de bruijn indices all the time
+- implement top-level definitions
+- implement less aggrevating syntax for non-dependent function & pair types
+- add a type of natural numbers
+- replace type-in-type with a proper (cumulative?) hierarchy of universes
+  -> maybe use the mugen library or figure out typical ambiguity?
+- implement inductive types/families
+- implement axioms (probably easy)
+- do HoTT stuff (maybe implement a form of cubical type theory? or stick with
+  book HoTT, which is probably much easier)
+- ...