~ejb/thon

a small functional language
Add singleton bst and start bst insert
Add empty binary tree example
typCtx is a list of 'a options now, not a list of ints

refs

master
browse  log 

clone

read-only
https://git.sr.ht/~ejb/thon
read/write
git@git.sr.ht:~ejb/thon

You can also use your local clone with git send-email.

 _   _
| | | |
| |_| |__   ___  _ __
| __| '_ \ / _ \| '_ \
| |_| | | | (_) | | | |
 \__|_| |_|\___/|_| |_|


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.

 _  _      _                 _   _  _            _
| \| |__ _| |_ _  _ _ _ __ _| | | \| |_  _ _ __ | |__  ___ _ _ ___
| .` / _` |  _| || | '_/ _` | | | .` | || | '  \| '_ \/ -_) '_(_-<
|_|\_\__,_|\__|\_,_|_| \__,_|_| |_|\_|\_,_|_|_|_|_.__/\___|_| /__/


- Z is the natural number 0.

- S Z is 1.

 ___             _   _
| __|  _ _ _  __| |_(_)___ _ _  ___
| _| || | ' \/ _|  _| / _ \ ' \(_-<
|_| \_,_|_||_\__|\__|_\___/_||_/__/


- \ 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.

 ___                   _        _   ___                    _
| _ ) ___ _  _ _ _  __| |___ __| | | _ \___ __ _  _ _ _ __(_)___ _ _
| _ \/ _ \ || | ' \/ _` / -_) _` | |   / -_) _| || | '_(_-< / _ \ ' \
|___/\___/\_,_|_||_\__,_\___\__,_| |_|_\___\__|\_,_|_| /__/_\___/_||_|


- \ 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).

 ___     _                         _    _
| _ \___| |_  _ _ __  ___ _ _ _ __| |_ (_)____ __
|  _/ _ \ | || | '  \/ _ \ '_| '_ \ ' \| (_-< '  \
|_| \___/_|\_, |_|_|_\___/_| | .__/_||_|_/__/_|_|_|
           |__/              |_|

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

 ___     _    _           _   _      _   ___         _
| __|_ _(_)__| |_ ___ _ _| |_(_)__ _| | | _ \__ _ __| |____ _ __ _ ___ ___
| _|\ \ / (_-<  _/ -_) ' \  _| / _` | | |  _/ _` / _| / / _` / _` / -_|_-<
|___/_\_\_/__/\__\___|_||_\__|_\__,_|_| |_| \__,_\__|_\_\__,_\__, \___/__/
                                                             |___/

- Pack 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.

 ___                    _           _____
| _ \___ __ _  _ _ _ __(_)_ _____  |_   _|  _ _ __  ___ ___
|   / -_) _| || | '_(_-< \ V / -_)   | || || | '_ \/ -_|_-<
|_|_\___\__|\_,_|_| /__/_|\_/\___|   |_| \_, | .__/\___/__/
                                         |__/|_|

- u.(unit | (nat * 0)) is the type of lists natural numbers.

- 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.

 ___         _        _ _
|_ _|_ _  __| |_ __ _| | |
 | || ' \(_-<  _/ _` | | |
|___|_||_/__/\__\__,_|_|_|

This works for me on ubuntu 20:

    $ git clone https://github.com/evanbergeron/thon.git
    $ 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";