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

- 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";