(* [] and :: are syntactic sugar for Nil/Cons, respectively *)
type List a = [ Nil
              | Cons a (List a)]

val length : forall a. List a -> Int
let length =
  let aux n xs = match xs with
      | [] -> n
      | x::xs -> aux (n + 1) xs
    end in
  aux 0

val append : forall a. List a -> List a -> List a
let append xs ys = match xs with
  | [] -> ys
  | x::xs -> x::append xs ys

val map : forall a b. (a -> b) -> List a -> List b
let map f xs = match xs with
    | [] -> []
    | x::xs -> f x::map f xs
  end

val join : forall a. List (List a) -> List a
let join xs = match xs with
    | [] -> []
    | l::xs -> append l (join xs)