Version 7 (modified by benl, 6 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. 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.