Rustpie is a Rust implementation of the Pie, a dependently typed language with a Lisp-like syntax. The language is formally specified in the book The Little Typer.
Rustpie is currently in very early development.
There are some differences between the Pie language in Rustpie and the canonical Pie implementation.
Rustpie adds the command (exit)
to exit the REPL.
It can only be used in the repl and cannot be used in source files.
In the canonical implementation, you must claim
and define
in a file.
Rustpie does not have this restriction, and you can add definitions directly in the REPL.
In the canonical implementation, constructing pairs using cons
directly in the REPL results in the “Can’t determine a type” error.
Rustpie repl does not have this restriction, and it will happily infer the type:
>>> (cons 1 'a)
(the (Pair Nat Atom) (cons 1 'a))