Changes between Version 16 and Version 17 of Commentary/Compiler/TypeType


Ignore:
Timestamp:
Jun 8, 2012 8:25:07 AM (3 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Compiler/TypeType

    v16 v17  
    8282A similar invariant applies to {{{FunTy}}}; {{{TyConApp}}} is never used with an arrow type.
    8383
    84 == Kinds ==
    85 
    86 Kinds are represented as types:
    87 {{{
    88 type Kind = Type
    89 }}}
    90 Basic kinds are now
    91 represented using type constructors, e.g. the kind `*` is represented as
    92 {{{
    93 liftedTypeKind :: Kind
    94 liftedTypeKind = TyConApp liftedTypeKindTyCon []
    95 }}}
    96 where `liftedTypeKindTyCon` is a built-in `PrimTyCon`.  The arrow type
    97 constructor is used as the arrow kind constructor, e.g. the kind `* -> *`
    98 is represented internally as
    99 {{{
    100 FunTy liftedTypeKind liftedTypeKind
    101 }}}
    102 It's easy to extract the kind of a type, or the sort of a kind:
    103 {{{
    104 typeKind :: Type -> Kind
    105 }}}
    106 The "sort" of a kind is always one of the
    107 sorts: `TY` (for kinds that classify normal types) or `CO` (for kinds that
    108 classify coercion evidence).  The coercion kind, `T1 :=: T2`, is
    109 represented by `PredTy (EqPred T1 T2)`.
    110 
    111 === Kind subtyping ===
    112 
    113 [[Image(https://docs.google.com/drawings/pub?id=1M5yBP8iAWTgqdI3oG1UNnYihVlipnvvk2vLInAFxtNM&w=359&h=229)]]
    114 
    115 (You can edit this picture [https://docs.google.com/drawings/d/1M5yBP8iAWTgqdI3oG1UNnYihVlipnvvk2vLInAFxtNM/edit?hl=en_GB here].)
    116 
    117 `*` is the kind of boxed values. Things like `Int` and `Maybe Float` have kind `*`.
    118 
    119 `#` is the kind of unboxed values. Things like `Int#` have kind `#`.
    120 
    121 `(#)` is the kind of unboxed tuples. Things like `(# Int, Int #)` have kind `(#)`.
    122 
    123 `ArgKind` is the kind of things that can appear as arguments to functions.
    124 
    125 `OpenKind` is the kind of things that can appear as results of functions.
    126 
    12784== Type variables ==
    12885