second-order abstract syntax
This is an implementation of Abstract Binding Trees from Robert Harper's book, Practical Foundations for Programming Languages.
In particular, this differs from many implementations of ABTs in the following respects:
You need either SML/NJ or MLton. Either download the binary SML/NJ installer or, on OS X, use homebrew:
brew update && brew install smlnj
Recursively clone the repo:
git clone --recursive https://github.com/jonsterling/sml-typed-abts.git
Note: whenever you pull anew from this repository, be sure to refresh the submodules:
git submodule update --init --recursive
To run the example with MLton, use the included script, and then run the resulting executable:
./scripts/mlton.sh
./example.out
Eventually, a prompt should appear at which you can parse and sort-check/infer ABT expressions. Here's an example session:
Type an expression at the prompt
> \x. x
lam([x@10].x@10)
> (\f. f 3) (\x. x)
Error: Fail: expected exp == nat
> (\f. f #3) (\x. x)
ap(lam([f@31].ap(f@31; num(3))); lam([x@32].x@32))
The printer is in "debug mode", which means that all variables are annotated with a unique index; this is useful for convincing oneself that variables are being bound properly.
Start the SML REPL:
cd sml-typed-abts
rlwrap sml
Standard ML of New Jersey v110.78 [built: Sun Apr 26 01:06:11 2015]
-
At the -
prompt, type:
- CM.make "example.cm";
You should see a lot of compilation messages and then, the prompt should appear:
Type an expression at the prompt
>