== Variables and Constructors ==
{{{
Var ::= Lower | VarSym -- plain variable eg: length, map_, wibble23
Con ::= Upper | VarSym -- plain constructor eg: Int, Cons, Tuple2
VarSym ::= Lower | Upper | Digit | _ | '
TyVar ::= Var -- value or higher kinded type variable
| % Var -- region variable
| ! Var -- effect variable
| $ Var -- closure variable
RVar ::= % Var -- region variable eg: %r1, %const
ECon ::= ! Con -- effect constructor eg: !Read, !Write
}}}
[[br]]
== Name spaces ==
Each variable lies in a particular names space. Variables in the region, effect and closure type name spaces are prefixed with a qualifier. We use % for regions, ! for effects and $ for closures. These symbols are also used for the corresponding region, effect and closure kinds. Variables in the value and value type name spaces do not have qualifiers.
||'''Namespace'''||'''qualifier'''||'''associated kind'''||'''example'''||
||Values||none||not applicable||length, map, Cons, Nothing||
||Value types||none||*||List, Tuple, the m in (forall (m :: * -> *). Monad m => a -> m a)||
||Region types||%||%||%r1, %const||
||Effect types||!||!||!e1, !Read, !Write, !Console||
||Closure types||$||$||$c1, $c2||
The general rule is that a type variable exists in the name space of its resulting kind. For example:
||The a in ||forall a. a -> a|| has kind *|| and is in name space * (value types)||
||The m in ||forall (m :: * -> *). ... || has kind (* -> *) || and is in name space * (value types)||
||The constructor||!Read|| has kind (% -> !)|| and is in name space ! (effects)||
||The variable||%r1||has kind %||and is in name space % (regions)||
The exceptions are type class constructors such as Eq and Mutable. Eq has kind * -> + and Mutable has kind % -> +. Although the result kind of these constructors is + (witnesses), we put the constructors Eq and Mutable in the * (type) name space instead of making a new name space for +. We follow Haskell in this respect. Note that although Haskell98 doesn't assign kinds to type class constraints, you can't have a type constructor Eq as well as a type class Eq in the same scope.
There is also a name space associated with each type. Projection function are added to these name spaces by defining data constructors to have fields, and by explicitly declaring projection dictionaries. For example, if {{{xs}}} has type {{{List Int}}} then the expression {{{xs.length}}} calls the projection function {{{length}}} located in the name space for {{{List Int}}}. If there is no {{{length}}} projection in the {{{List Int}}} name space, but there is in a more general name space such as {{{List a}}}, then that is used instead.