thon

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)))))
in
(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.

functions

• \ x : nat -> x is the identity function on natural numbers.

  We could also have \ x : nat -> (\ y : nat -> y). This function returns a function that returns whatever was fed to the top-level function.

• ((\ x : nat -> x) Z) applies the identity function to the natural number Zero.

bounded recursion

• \ nat -> rec 0 ( Z -> Z | S -> S S 0 ) is a function that multiplies its input by 2. Let’s break it down:

  rec i ( Z -> b | S -> r) evaluates to b if i is Zero. This is the base case.

  The recursive case (r) binds a new variable that represents the value of the previous recursion.

  rec (S i) ( Z -> b | S -> r ) plugs its previous recusive value rec i ( Z -> b' -> S - > r') in for this “previous recursion” variable in the recursive case r.

  e.g.

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

• poly \ 0 -> 0 is the polymorphic identity function.

existential packages

• impl makes a type private to an implementation. Here’s a simple example:

  ((*set*) \ x : nat -> (x, Z),
  (*get*) \ tup : (nat * nat) -> fst tup)
  
  ((*set*) \ x : nat -> x,
   (*get*) \ x : nat -> x)

  These tuples are two different implementations of a (set, get) interface.

  The left function in each takes in a natural number and converts it to something. The right function of each retrieves that natural number.

  The first implementation stores its arg in the tuple (arg, 0). The second stores arg by itself. Of course, these implementations have different types.

  These internal storage types are implementation details; let’s pack them away.

  impl (nat -> 0, 0 -> nat) with nat as
  (
      ((*set*) \ x : nat -> x,
      (*get*) \ x : nat -> x)
  )
  
  impl (nat -> 0, 0 -> nat) with (nat * nat) as
  (
      ((*set*) \ x : nat -> (x, Z),
      (*get*) \ tup : (nat * nat) -> fst tup)
  )

  Both of these expression have type ((nat -> T) * (T -> nat)) for some type T. They’ve abstracted away their implementation type into an abstract type variable.

  Now we can use these two implementations interchangably. I’ll write up an example of how to do this later.

recursive types

• u.(unit | (nat * 0)) is the type of lists natural numbers. The u is an approximation of the fancy type theory lower case mu. Eventually this will be more reasonable.

• fold u . (unit | (nat * 0)) with left unit : (unit | (nat * (u . (unit | (nat * 0)))))

  is the empty list of natural numbers. Haha I will add more sugar over time for this…

• \ (nat * (u. (unit | (nat * 0)))) -> fold u.(unit | (nat * 0)) with right 0 : (unit | (nat * (u. (unit | (nat * 0)))))

  is a function that takes a pair (nat, natlist) and prepends nat to natlist.

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/thon.cm";
- Thon.run "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 bergeronej@gmail.com. I would love to hear from you!