This is an implementation of the language T from PFPL. It uses the CMU ABT library (the one used in the 15-312 course at CMU).

The aim is to closely follow the description in PFPL. All typing rules can be found in src/statics/typechecker.sml and all dynamics rules in src/dynamics/dynamics.sml somewhere close to the corresponding lines of code.

You need smlnj to build along with ml-lex and ml-yacc. Given that you have these installed, just make in the project directory. If all goes well you should find the executables bin/system-t and bin/repl. Here is an example repl session:

$ ./bin/repl
> (\(x:nat) s(x))(s(s(z)))
Step: s(s(s(z)))
s(s(s(z))) : nat
> \ (x:nat) s(s(x))
lam{nat}([email protected](s(x@2))) : arr(nat; nat)
> (\ (f : nat -> nat) \ (x : nat) f(x))(\ (x:nat) s(x))(s(z))
Step: ap(lam{nat}([email protected](lam{nat}([email protected](x@7)); x@6)); s(z))
Step: ap(lam{nat}([email protected](x@10)); s(z))
Step: s(s(z))
s(s(z)) : nat
> \ (f:nat->nat) s(f)
Type error: s can be only applied to a nat.
> rec s(s(s(z))) {z => z | s(u) with v => s(s(s(v)))}
Step: s(s(s(rec(z; [email protected]@8.s(s(s(x@8))); s(s(z))))))
Step: s(s(s(s(s(s(rec(z; [email protected]@12.s(s(s(x@12))); s(z))))))))
Step: s(s(s(s(s(s(s(s(s(rec(z; [email protected]@16.s(s(s(x@16))); z))))))))))
Step: s(s(s(s(s(s(s(s(s(z)))))))))
s(s(s(s(s(s(s(s(s(z))))))))) : nat

Using the bin/system-t executable you can execute the T program in a file. There is a sample program in examples/sample.t. Executing it yields the following result.

$ ./bin/system-t examples/sample.t
s(s(s(s(z))))

Note that instead of ↪ we use =>.

I have followed the homework solutions to CMU's 15-312. The ABT library is almost directly taken from the solutions that can be found on the course website as well as some of the other files (e.g. src/parser/parsestates.sml).