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;


Ross Paterson <ross@soi.city.ac.uk>