Version 2 (modified by benl, 8 years ago)


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               -- variable in the region namespace     eg: %r1, %const
ECon   ::=   !  Con               -- constructor in the effect namespace  eg: !Read, !Write

Name spaces

Each variable lies in a particular names space. There are several name spaces, and the five basic ones are:

Namespacequalifierassociated kindexample
Valuesnonenot applicablelength, map, Cons, Nothing
Value typesnone*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

All variables in the region, effect and closure name spaces are prefixed with a qualifier, which is also the symbol for that kind.

The general rule is that a 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%r1has kind %and is in name space % (regions)

The exception to this rule is the kinds given to type class constraints such as Eq and Mutable. Eq has kind * -> + and Mutable has kind % -> +, but 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 a kind to type class constraints, constrains and type constructors are still in the same name space, so 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 types 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.