Polymorphism and universes

Polymorphism lets one declaration work for many types. Universes ensure that types themselves have a checked classification without placing everything in one inconsistent Type : Type loop.

Implicit type parameters

function id[a:Type](item:a) : a = item;
function singleton[a:Type](item:a) : List(a) = Cons(item, Nil);

At a call, expected types and arguments infer a when possible. Square brackets mark the parameter implicit; it remains explicit in typed elaboration and is normally erased when used only at type level.

Universal types

value identity : forall a. a -> a = fn(item) = item;

forall a. T introduces an implicit Pi binder over Type. The Unicode ∀ spelling is equivalent. Use explicit binder annotations when the intended universe or value domain is not obvious.

Universe levels

Type
Type1
Type2

Type is universe U 0, containing ordinary value types. Type1 classifies type constructors at the next level, and so on. The hierarchy is cumulative: a term accepted at a lower universe may be lifted to a higher one when required.

Cumulativity is a directed lift, not definitional equality between all levels. The checker must not solve a downward universe demand by pretending distinct levels are identical.

Higher-kinded parameters

structure Mappable(f:Type1) = {
    function map[a:Type,b:Type](g:a -> b, item:f(a)) : f(b)
};

f constructs value types, so it belongs to Type1. The front end can check higher-kinded declarations; first-class runtime passage of arbitrary type constructors remains a named implementation gap in some compiled paths.

Inference and public APIs

Inference is a convenience, not an excuse to hide a library contract. State type parameters, effect rows, and constraints on exported functions when doing so makes callers and compatibility clearer.

Explicit universe-level variables are reserved for a later surface revision; the compiler may infer level-polymorphic binders internally, but documentation must not invent level syntax absent from the Language Reference.

Why universes matter

Dependent types allow values inside types, and polymorphism allows types as inputs. Universes keep these powerful combinations stratified, make normalization obligations visible, and prevent circular typing paradoxes.

Common mistakes

Do not write unapproved explicit level-variable syntax or treat cumulativity as symmetric equality. A parameter that constructs ordinary value types generally belongs in Type1, not Type.

Recap

Implicit parameters express reusable code; universes classify what those parameters may range over. Inference fills routine details without weakening the declared universe discipline.

Normative details: Language Reference §4.1–4.3.