Types

A type is specified by a type expression. Type expressions may contain type variables. A type expression with no free type variables is called a closed type expression. A closed type expression can be interpreted as containing a set of values, and so can be used to define a type. Non-closed types can also be given a meaning by supplying a type for each free type variable.

A type expression has one of the following forms:

• The type Symbol, containing the string values.
• The type Bool, containing the Boolean values.
• The type Int, containing the integer values.

• The tuple type expression <n_0 : t_0, ..., n_m : t_m> where each n_i is an lident and t_i is a type expression. It contains all tuple values of the form <n_0 : v_0, ..., n_m : v_m> where value v_i is contained in t_i.

• The anonymous tuple type <t_0, ..., t_m> where each t_i is a type expression. It contains all anonymous tuple values <v_0, ..., v_m> where value v_i is contained in t_i.

• a, where a is an lident, representing a type variable, which is a placeholder for any type.

• forall a.t where a is an lident representing a type variable, and t is a type expression. If t contains no free variables besides a, then forall a.t is closed. The meaning of forall a.t can be understood as follows. Let t[u/a] be the same as t except that every unshadowed occurence of a is replaced by type expression u. (Unshadowed means that if t contains a subexpression forall a.v, that subexpression is unchanged.) Then forall a.t is equal to the intersection of t[u/a] over all type expressions u.

• (t), where t is a type expression, is equivalent to the type expression t.

• args -> t, where args has a form described below, and t is a type expression, defines an arrow type. An arrow type contains functions from a number of argument types, described by args, to a result type described by t. args may contain one of the following forms:
  • (), in which case the arrow type contains functions taking zero arguments.
  • The type expression t, in which case the arrow type contains functions taking a single argument of type t.
  • (t_1,...,t_m) where the t_i are type expressions, in which case the arrow type contains functions taking m arguments, where the i-th argument has type t_i.

• U args where U identifies a defined type, and args are the arguments to the type. As we will see below, it is possible to define a new type, and it may take type arguments. Such a defined type can be referred to in future type expressions. The name of a defined types is a uident. U is a ulongvar and accesses a defined type as follows. If it is simply a uident, it refers to a type defined in the same block or a containing block. Otherwise it has the form x.y where y is a ulongvar, and it refers to the type accessed by y in the nested block defining variable x. The defined type may take zero or more arguments. The arguments are type expressions separated by commas. The list of arguments may optionally be enclosed in square braces. This notation reinforces the idea that the defined type is being applied to a set of arguments.