Changes between Version 4 and Version 5 of IntermediateTypes


Ignore:
Timestamp:
Aug 4, 2006 12:59:12 PM (9 years ago)
Author:
guest
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • IntermediateTypes

    v4 v5  
    2020 * Coercions have been added - The syntax of types now includes coercions which are evidence for type equalities.  There are distinguished coercion variables and a new variant of `TyCon`, with constructor `CoercionTyCon`.  There is also a new `Expr` variant, with constructor `Cast`, which performs a cast given an expression and evidence of the safety of the cast.
    2121
    22  * Kinds are now Types - The type Kind is just a synonym for Type.  There are special PrimitiveTyCons that represent kinds.
     22 * Kinds are now Types - The type `Kind` is just a synonym for `Type`.  There are special !PrimitiveTyCons that represent kinds.
    2323
    2424 * Newtypes are implemented with coercions - The previous ad-hoc mechanism has been replaced with one that uses coercions.
     
    3535probably not be used outside the few places it is already used.  Type
    3636re-exports everything useful from !TypeRep, but exports the
    37 representation abstractly.  The datatype Type really represents a
     37representation abstractly.  The datatype `Type` really represents a
    3838single syntactic category that includes types, coercions, kinds, and
    3939super-kinds.
     
    4242=== Type Variables ===
    4343
    44 Type variables, of type Var, and associated construction and
     44Type variables, of type `Var`, and associated construction and
    4545manipulation functions are defined in the Var module.  There are two
    46 data constructors that make type variables, !TyVar and !TcTyVar.
    47 !TcTyVars can be mutable tyvars that are instantiated during type
    48 checking.  After typechecking, all !TcTyVars are turned to !TyVars.
    49 !TyVars carry a Bool field, isCoercionVar which is True if the type
    50 variable is a coercion variable and False otherwise.  The function
    51 TyVar.isCoVar should be used to test if a type variable is a coercion
     46data constructors that make type variables, `TyVar` and `TcTyVar`.
     47`TcTyVar`s can be mutable tyvars that are instantiated during type
     48checking.  After typechecking, all `TcTyVar`s are turned to `TyVar`s.
     49`TyVar`s carry a `Bool` field, `isCoercionVar`, which is `True` if the type
     50variable is a coercion variable and `False` otherwise.  The function
     51`isCoVar` should be used to test if a type variable is a coercion
    5252variable.
    5353
    5454=== Type Constructors ===
    5555
    56 Type constructors, of datatype !TyCon, are defined in the !TyCon module
     56Type constructors, of datatype `TyCon`, are defined in the !TyCon module
    5757and exported abstractly.  There are several different sorts of type
    5858constructors; the most important for understanding the overall
    5959intermediate language type system are:
    6060 
    61  * !AlgTyCon, which are for tycons for datatypes and newtypes and have a field of type !AlgTyConRhs which specified whether it is a datatype or newtype and contains further information for each;
    62  * !PrimTyCon, which are for built-in primitive tycons, and are also used to represent base kinds; 
    63  * !CoercionTyCon, which are for special tycons which are meant to represent syntactic forms (and not really type constructors), so they must be saturated to have a kind;
    64  * !SuperKindTyCon, which are tycons that are used to represent super-kinds, also called sorts (which classify kinds as either coercion kinds, CO, or type kinds, TY), !SuperKindTyCons are unique in never having a kind. 
    65 
    66 All !TyCon's but !SuperKindTyCon and !CoercionKindTyCon carry their kind
    67 in a field called tyConKind, and !CoercionKindTyCons carry their
    68 kinding rule (a function with type [Type] -> Kind) in a field called
    69 coKindFun.
     61 * `AlgTyCon`, which are for tycons for datatypes and newtypes and have a field of type `AlgTyConRhs` which specified whether it is a datatype or newtype and contains further information for each;
     62 * `PrimTyCon`, which are for built-in primitive tycons, and are also used to represent base kinds; 
     63 * `CoercionTyCon`, which are for special tycons which are meant to represent syntactic forms (and not really type constructors), so they must be saturated to have a kind;
     64 * `SuperKindTyCon`, which are tycons that are used to represent super-kinds, also called sorts (which classify kinds as either coercion kinds, CO, or type kinds, TY), `SuperKindTyCon`s are unique in never having a kind. 
     65
     66All `TyCon`s but `SuperKindTyCon` and `CoercionKindTyCon` carry their kind
     67in a field called `tyConKind`, and `CoercionKindTyCons` carry their
     68kinding rule (a function with type `[Type] -> Kind`) in a field called
     69`coKindFun`.
    7070
    7171=== Kinds are Types ===
    7272
    7373We have (as of August 2006) unified types and kinds as members of the
    74 datatype Type.  Kind is just a synonym for Type.  Basic kinds are now
    75 represented using type constructors, e.g. the kind * is represented as
     74datatype `Type`.  `Kind` is just a synonym for `Type`.  Basic kinds are now
     75represented using type constructors, e.g. the kind `*` is represented as
    7676     
    7777      {{{star = TyConApp liftedTypeKindTyCon []}}}
    7878
    79 where liftedTypeKindTyCon is a built-in !PrimTyCon.  The arrow type
    80 constructor is used as the arrow kind constructor, e.g. the kind * ->
    81 * is represented internally as
     79where `liftedTypeKindTyCon` is a built-in `PrimTyCon`.  The arrow type
     80constructor is used as the arrow kind constructor, e.g. the kind `* ->
     81*` is represented internally as
    8282
    8383      {{{FunTy star star}}}
     
    8686the typeKind function.  The "Kind" of a kind is always one of the
    8787sorts TY (for kinds that classify normal types) or CO (for kinds that
    88 classify coercion evidence).  The coercion kind, T1 :=: T2, is
    89 represented by !PredTy (!EqPred T1 T2).
     88classify coercion evidence).  The coercion kind, `T1 :=: T2`, is
     89represented by `PredTy (EqPred T1 T2)`.
    9090
    9191GHC has a relatively complicated kind structure...
     
    9393There's a little subtyping at the kind level.  Here is the picture for
    9494type-kinds (kinds of sort TY).
     95
    9596{{{
     97
    9698                 ?
    9799                / \
     
    112114        (->)  :: ?? -> ? -> *
    113115        (\(x::t) -> ...)        Here t::?? (i.e. not unboxed tuple)
     116
    114117}}}
    115118
     
    117120
    118121Coercions are type-level terms which act as evidence for type
    119 equalities and are classified by a new sort of kind (with the form T1
    120 :=: T2).  Most of the coercion construction and manipulation functions
     122equalities and are classified by a new sort of kind (with the form `T1
     123:=: T2`).  Most of the coercion construction and manipulation functions
    121124are found in the Coercion module.
    122125
    123126The syntax of coercions extends the syntax of types (and the type
    124 Coercion is just a synonym for Type).  By representing coercion
     127`Coercion` is just a synonym for `Type`).  By representing coercion
    125128evidence on the type level, we can take advantage of the existing
    126129erasure mechanism and keep non-termination out of coercion proofs
    127130(which is necessary to keep the system sound).  The syntax of
    128131coercions and types also overlaps a lot.  A normal type is evidence
    129 for the reflexive coercion, i.e.
     132for the reflexive coercion, i.e.,
    130133
    131134    {{{Int :: Int :=: Int}}}
    132135
    133 There are also coercion variables, which are represented as TyVar's
    134 for which the isCoercionVar field is True.  Coercion variables are
     136Coercion variables are
    135137used to abstract over evidence of type equality, as in
    136138
     
    140142to implement some source language features (newtypes for now,
    141143associated types soon and probably more in the future).  Coercion
    142 constants are represented as TyCons made with the constructor
    143 CoercionTyCon.
     144constants are represented as `TyCon`s made with the constructor
     145`CoercionTyCon`.
    144146
    145147Coercions are type level terms and can have normal type constructors applied
    146148to them.  The action of type constructors on coercions is much like in
    147 a logical relation.  So if c1 :: T1 :=: T2 then
     149a logical relation.  So if `c1 :: T1 :=: T2` then
    148150 
    149     [c1] :: [T1] :=: [T2]
    150 
    151 and if c2 :: S1 :=: S2 then
    152 
    153     c1 -> c2 :: (T1 -> S1 :=: T2 -> S2)
     151    `[c1] :: [T1] :=: [T2]`
     152
     153and if `c2 :: S1 :=: S2` then
     154
     155    `c1 -> c2 :: (T1 -> S1 :=: T2 -> S2)`
    154156
    155157The sharing of syntax means that a normal type can be looked at as
    156158either a type or as coercion evidence, so we use two different kinding
    157 relations, one to find type-kinds (implemented as Type.typeKind ::
    158 Type -> Kind) and one to find coercion-kinds (implemented as
    159 Coercion.coercionKind :: Coercion -> Kind).
     159relations, one to find type-kinds (implemented in Type as `typeKind ::
     160Type -> Kind`) and one to find coercion-kinds (implemented in Coercion as
     161`coercionKind :: Coercion -> Kind`).
    160162
    161163Coercion variables are distinguished from type variables, and
     
    174176
    175177In most of the compiler, as in the FC paper, coercions are abstracted
    176 using !ForAllTy cv ty where cv is a coercion variable, with a kind of
    177 the form !PredTy (!EqPred T1 T2).  However, during type inference it is
     178using `ForAllTy cv ty` where `cv` is a coercion variable, with a kind of
     179the form `PredTy (EqPred T1 T2)`.  However, during type inference it is
    178180convenient to treat such coercion qualifiers in the same way other
    179181class membership or implicit parameter qualifiers are treated.  So
    180 functions like tcSplitForAllTy and tcSplitPhiTy and tcSplitSigmaTy,
    181 treat !ForAllTy cv ty as if it were !FunTy (!PredTy (!EqPred T1 T2)) ty
    182 (where !PredTy (!EqPred T1 T2) is the kind of cv).  Also, several of the dataConXXX functions treat equality
     182functions like `tcSplitForAllTy` and `tcSplitPhiTy` and `tcSplitSigmaTy`,
     183treat `ForAllTy cv ty` as if it were `FunTy (PredTy (EqPred T1 T2)) ty`
     184(where `PredTy (EqPred T1 T2)` is the kind of `cv`).  Also, several of the dataConXXX functions treat equality
    183185
    184186=== Newtypes are coerced types ===