Universal types

extend with #universal-types;

Similar to generics in some object-oriented languages, universal type quantifiers allow you to implement parametric polymorphism in your functions. This means that you can write functions that can be used with different types of arguments.

With universal types, you can write generic functions that accept type parameters. These type parameters can be used in the type annotations for the function's arguments and return type. When calling the function, you must provide a concrete type, and the type parameter in the function definition is replaced with the actual type for that call.

To declare a generic function, simply add the generic keyword before fn and declare the type parameters between [] (comma-seprated) after the function name like so:

language core;

extend with #universal-types;

generic fn identity[T](x : T) -> T {
  return x
}

fn main(x : Nat) -> Nat {
  return identity[Nat](x)
}

It is also possible to write generic type abstractions for any expression. For example, the expression generic [X] inl(0) as Nat + X can be used anywhere where a sum type with the first type being Nat is expected. It can also be used with anonymous function expressions (abstractions):

language core;

extend with #universal-types;

generic fn const[X](x : X) -> forall Y. fn(Y) -> X {
  return generic [Y] fn(y : Y) { return x }
}

fn main(x : Nat) -> Nat {
  return const[Nat](x)[Bool](false)
}

The above example can also be written without the universal quantifier forall:

language core;

extend with #universal-types;

generic fn const[X, Y](x : X) -> fn(Y) -> X {
  return fn(y : Y) { return x }
}

fn main(x : Nat) -> Nat {
  return const[Nat, Bool](x)(false)
}

but then both type parameters have to be provided when calling the const function, whereas in the earlier example only one type parameter belonged to const and the other belonged to the function it returned and only needs to be provided when that function is called. The forall quantifier is used to represent the type of a generic expression.

As one last example demonstrating impredicativity, consider the self-application function from System F:

generic fn self_app[X](f : forall X . fn(X) -> X) -> forall X . fn(X) -> X {
  return f[forall X . fn(X) -> X](f)
}