Typing the Y combinator in Links.

y.links

# Typing the Y combinator in Links.
# links> examples();
# 720
# Succ(Succ(Succ(Succ(Succ(Succ(Zero))))))
# () : ()

sig y : (((a) ~e~> b) ~e~> (a) ~e~> b) -> (a) ~e~> b
fun y(f) {
  fun g(x : (mu f . (((f) ~e~> (a) ~e~> b))))(a) {
    f(x(x))(a)
  }
  g(g)
}

# The factorial function.
sig fact : ((Int) ~e~> Int) -> (Int) ~e~> Int
fun fact(self)(n) {
  if (n == 0) 1 else n * self(n-1)
}

# A representation of natural numbers.
typename Nat = [|Zero|Succ:Nat|];

sig int2nat : ((Int) ~e~> Nat) -> (Int) ~e~> Nat
fun int2nat(self)(n) {
  if (n == 0) Zero
  else Succ(self(n-1))
}

sig natToString : (Nat) ~> String
fun natToString(n) {
  switch (n) {
    case Zero     -> "Zero"
    case Succ(n') -> "Succ(" ^^ natToString(n') ^^ ")"
  }
}

fun examples() {
  var result = y(fact)(6);
  println(intToString(result));
  var result = y(int2nat)(6);
  println(natToString(result))
}