thon is a small programming language. Here’s an example program that verifies the empty list is empty.

let isempty : (u. (unit |  (nat * 0))) -> nat =
    \ natlist : (u. (unit |  (nat * 0))) ->
        (case (unfold natlist) of
          empty -> S Z
        | hdAndTl -> Z)
in let nil : (u. (unit |  (nat * 0))) =
    fold u . (unit | (nat * 0))
    with left unit : (unit |  (nat * (u . (unit | (nat * 0)))))
(isempty nil)

thon has natural numbers, functions, bounded recursion, binary product and sum types, parametric polymorphism, existential packages (a formalization of interfaces), and recursive types.

All that stuff is sanity tested and seems to work. The parser is not done yet.

natural numbers

Z is the natural number 0, S Z is 1.


bounded recursion

rec (S Z) (Z -> Z | S -> S S 0) (*steps to*)
S S (rec (Z) (Z -> Z | S -> S S 0)) (*steps to*)
S S (Z).

parametric polymorphism

existential packages

recursive types

I’ve mostly been working out of Bob Harper’s “Practical Foundations for Programming Languages,” though Pierce’s “Types and Programming Languages” has been a useful source of examples and exposition as well. I am also grateful to Rob Simmons and every other contributor to the SML starter code for CMU’s Fall 2016 compilers course.

install (ubuntu 20)

Wow, you read this far! If you’d like to program in thon, clone the git repo, then

$ sudo apt install smlnj ml-yaxx ml-lex ml-lpt
$ sml
- CM.make "path/to/your/git/clone/";
- "some thon program here";

If you figure out install instructions on mac or windows or have any other questions or comments, please email me at I would love to hear from you!