== 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.