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!
Presently, everything is tested on Racket 6.3. Older versions probably don’t work.
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))
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.