Standard type variables.
typevar alpha, beta, gamma;Function and product types.
infixr -> : 2; abstype neg -> pos; infixr # : 4; abstype pos # pos; --- (a # b) (x, y) <= (a x, b y); infixr X : 4; type alpha X beta == alpha # beta;Normal right-to-left composition of f and g.
infix o : 2; dec o : (beta -> gamma) # (alpha -> beta) -> alpha -> gamma; --- (f o g) x <= f(g x); --- (a -> b) f <= b o f o a;The identity function.
dec id : alpha -> alpha; --- id x <= x;Booleans with the standard operations.
data bool == false ++ true; type truval == bool; infix or : 1; infix and : 2; dec not : bool -> bool; --- not true <= false; --- not false <= true; dec and : bool # bool -> bool; --- false and p <= false; --- true and p <= p; dec or : bool # bool -> bool; --- true or p <= true; --- false or p <= p; dec if_then_else : bool -> alpha -> alpha -> alpha; --- if true then x else y <= x; --- if false then x else y <= y;Lists.
infixr :: : 5; data list alpha == nil ++ alpha :: list alpha;List concatenation.
infixr <> : 5; dec <> : list alpha # list alpha -> list alpha; --- [] <> ys <= ys; --- (x::xs) <> ys <= x::(xs <> ys);The type num behaves as if it were defined by:
! data num == 0 ++ succ num;but is actually implemented a little more efficiently. The type also contains negative numbers (and reals in some implementations).
data num == succ num;Similarly, the type char behaves as if it were defined as an enumeration (in the normal order) of all the ASCII character constants.
abstype char; --- char x <= x;