diff options
Diffstat (limited to 'README.md')
-rw-r--r-- | README.md | 40 |
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) +- ... |