Join 10350+ others. No spamming.
I promise!

Follow us at github.



david-christiansen / tt-playground


A playground for type theory implementations in Racket


A type theory playground

This is a place for experimental implementations of type theories that may well be busted, as well as a place for me to learn Racket.

No guarantees about any of it!

Racket versions

Presently, everything is tested on Racket 6.3. Older versions probably don’t work.

A Refiner for a CTT Dialect

tt.rkt and tt-interface.rkt contain a simple refiner and proof editor for a vaguely Nuprl-inspired theory. To try it out, load up tt-interface.rkt in Racket and evaluate the following at the REPL:

(prove (⊢ empty
          '(⋂ ((t Type))
              (Π ((y t))

You’ll get a little proof editor. In the top of the proof editor, there’s a tree view that shows the overall structure of the proof. Click on the proof goal, and the bottom half of the proof editor will display its details. In the text field labeled “by”, type intersection-membership and click the Refine button. You’ll get two new goals.

In the first of these subgoals, type (lambda-intro '(x)) and refine. This will give two goals: solve them with (hypothesis 0) and (hypothesis-equality 0) respectively. As you solve these goals, the goal overview is updated to show the incrementally-constructed program.

Solve the last goal with type-in-type. Proper universe polymorphism and perhaps typical ambiguity remain to be implemented.