example.in

# Natural numbers
cons Z
cons S(n)

# Erasure and Duplication
# def erase(_)
# def dup(_) = (a, b)
#   | dup(_) = (c, d) => (c, d)

# Addition
def _ + y = r
  | Z    => y
  | S(x) => x + S(y)

# Multiplication
def _ * y = r
  | Z    => erase(y); Z
  | S(x) => (y1, y2) = dup(y); x * y1 + y2

# Example: Computations on natural numbers
let y = 5n
    x = 3n
    example_3_plus_5 = x + y

let example_3_times_2 = 3n * 2n

# Lists
cons Nil
cons head :: tail = l

def length(list) = r
  | Nil => Z
  | x :: xs => erase(x); S(length(xs))

def map(list, fi, fo) = r
  | Nil => erase(fi); erase(fo); Nil
  | x :: xs => (x, fi2) = dup(fi)
               (fo1, fo2) = dup(fo)
               fo1 :: map(xs, fi2, fo2)

# Example: List operations
let l0 = 1n :: 2n :: 3n :: Nil
    (l0a, l0b) = dup(l0)
    l0_length = length(l0a)
    l0_mapped = map(l0b, x, x + 2n)

# Explicit lambdas
cons in |> out
def apply(l, in) = out
  | i |> o => in = i; o

# Example: List mapping with lambdas
def map2(l, f) = r
  | Nil     => erase(f); Nil
  | x :: xs => (f1, f2) = dup(f)
               apply(f1, x) :: map2(xs, f2)

let l0 = 1n :: 2n :: 3n :: Nil
    l0_mapped_lambda = map2(l0, x |> x + 2n)