Example programs¶

This page should give a lot of example programs to give some insight into how to use various features of the language. Note that the language isn't 100% settled, so some things (even syntactic things) may change very slightly over time.

Simple functions over natural numbers and lists¶

The identity function:

id = | x.x;

The predecessor function (over natural numbers):

pred = | x.peek x of {
  Zero.Zero;
  Succ(x).x };

The addition function:

add = x | y.fold f(x, y) as {
  Zero.y;
  Succ(_|z).f(z, Succ(y))
} in f(x, y);

The multiplication function:

mul = x, y | .fold f(x) as {
  Zero.Zero;
  Succ(_|z).add(y, f(z))
} in f(x);

Less-than-or-equal:

leq = x | y.fold f(x, y) as {
  Zero.True;
  Succ(_|z).case y of {
    Zero.False;
    Succ(w).f(z, w) }
} in f(x, y);

Determining the length of a list:

length = x | .fold f(x) as {
  Nil.Zero;
  Cons(_, _|z).Succ(f(z))
} in f(x);

Coinductive examples¶

First we introduce the type of functions, over domain a and codomain b. It only has one destructor, Eval:

data c -> Fn a b = Eval : c, a -> b;

We can define, for instance, the function which takes a natural number and adds 3 to it:

addThree = | .( Eval : x.add(3, x) );

Applying a function f to every element in a (inductive) list:

map = f | l.fold g(l) as {
  Nil.Nil;
  Cons(x, _|xs).Cons(Eval[f](x), g(xs))
} in g(l);

We can define the (lazy) infinite list:

data c -> InfList a
  = Head : c -> a
  | Tail : c -> c;

The list of all natural numbers:

allNats = | .unfold g(x) as (
  Head : x;
  Tail : g(Succ(x))
) in g(Zero);

Applying a function f to every element in a (coinductive) list:

mapLazy = f | l.unfold g(l) as (
  Head : Eval[f](Head[l]);
  Tail : g(Tail[l])
) in g(l);

More complex examples¶

Insertion sort:

insert = i, xs | ys.fold f(us, vs) as {
    Nil.[i];
    Cons(a, _|ws).peek vs of {
        Nil.[i];
        Cons(z, zs).case leq(i, z) of {
            True.Cons(i, Cons(z, zs));
            False.Cons(z, f(ws, zs)) } }
} in f(xs, ys);

insertSort = y | .fold f(z) as {
    Nil.Nil;
    Cons(x, xs' | xs).insert(x, xs', f(xs))
} in f(y);