## ~thon/thon

646b3dd8476232930872ac776c0a5a07d3472f32 — Evan Bergeron 3 months ago
```Update README
```
```1 files changed, 14 insertions(+), 18 deletions(-)

```
`M README.md => README.md +14 -18`
```@@ 1,25 1,21 @@
# thon

thon is a small programming language. Here's an example program that
-verifies the empty list is empty.
+verifies the singleton list is not empty.

```
-fun isempty : (data l = (unit | nat * l)) -> nat =
-  \ natlist : (data l = (unit | nat * l)) ->
-        (case (unfold natlist) of
+data list = Nil unit | Cons nat * list in
+fun isempty : list -> nat =
+  \ natlist : list ->
+        (case (exposelist natlist) of
empty -> S Z
| not -> Z)
-in let nil : (data l = (unit | nat * l)) =
-    fold data l = (unit | nat * l) with
-    left unit : (unit
-               | nat * (data l = (unit | nat * l)))
-in
-(isempty nil)
+in (isempty (Cons (Z, (Nil unit))))
```

thon has natural numbers, functions, recursion, binary product and sum
types, polymorphism, existential packages (a formalization of
-interfaces), and recursive types.
+interfaces), recursive types, and binary algebraic datatypes.

## natural numbers

@@ 162,19 158,19 @@ abstract, we can equivalently use the other implementation.

## recursive types

-`data nats = (unit | (nat * nats))` is the type of lists natural numbers.
+`u nats. (unit | (nat * nats))` is the type of lists natural numbers.

```
-fold data nats = (unit | (nat * nats))
-with left unit : (unit | (nat * (data nats = (unit | (nat * nats)))))
+fold u nats.  (unit | (nat * nats))
+with left unit : (unit | (nat * (u nats. (unit | (nat * nats)))))
```

is the empty list of natural numbers.

```
-\ (nat * (data nats = (unit | nat * nats))) ->
-   fold data nats = (unit | nat * nats) with
-   right 0 : (unit | nat * (data nats = (unit | nat * nats)))
+\ (nat * (u nats. (unit | nat * nats))) ->
+   fold u nats. (unit | nat * nats) with
+   right 0 : (unit | nat * (u nats. (unit | nat * nats)))
```

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

@@ 208,7 204,7 @@ A fun program I wrote after adding recursion. Pretty much all the code
I've written in thon is available through the git repo.

```
-let isone : nat -> nat =
+let isone : nat -> nat =
\ n : nat ->
ifz n of
Z -> Z (*false*)

```