Standard type constructors

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;