Changes between Version 4 and Version 5 of IntermediateTypes


Ignore:
Timestamp:
Aug 4, 2006 12:59:12 PM (8 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 ===