let map f = function (* 1 *)
| [] -> []
| Cons (x, xs) -> Cons (f x, map f xs) (* 2 *)

let filter p xs = [ x | with x <- xs, p x ] (* 3 *)

1. Minimalist syntax: semicolons, in and other noise is entirely optional.
2. Pattern matching and guards make writing code more intuitive.
3. List comprehensions are a short and sweet way of expressing complex computations on lists.

type vect 'n 'a =    (* 1 *)
  | Nil  : vect Z 'a (* 2 *)
  | Cons : forall 'a. 'a * vect 'n 'a -> vect (S 'n) 'a

(* 3 *)
let rec map (f : 'a -> 'b) (xs : vect 'n 'a) : vect 'n 'b =
  match xs with
  | Nil -> Nil
  | Cons (x, xs) -> Cons (f x, map f xs)

1. Types can be parametrised by not only other types, but all manners of data types: type constructors, naturals, integers…
2. Indexed types let constructors vary their return types, enforcing invariants statically.
3. Polymorphic type annotations enforce strict contracts on implementations, more often than not forbidding incorrect implementations entirely.

type function 'n :+ 'k begin  (* 1 *)
  Z      :+ 'n = 'n           (* 2 *)
  (S 'n) :+ 'k = S ('n :+ 'k) (* 3 *)
end

let rec append (xs : vect 'n 'a) (ys : vect 'k 'a) : vect ('n :+ 'k) 'b =
  match xs with
  | Nil -> ys
  | Cons (x, xs) -> Cons (x, append xs ys)

1. Type functions let the programmer express complex invariants in a functional language rather than trying to wrangle type-level prolog.
2. Functions at the type level are defined by pattern matching and compute by β-reduction, much like at the value level.
3. A powerful termination checker ensures that your type-level functions won't send the type checker into a tailspin. Even then, the type checker has resource limits to ensure it does not run away.