Changes between Version 4 and Version 5 of IntermediateTypes
 Timestamp:
 Aug 4, 2006 12:59:12 PM (10 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

IntermediateTypes
v4 v5 20 20 * 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. 21 21 22 * Kinds are now Types  The type Kind is just a synonym for Type. There are specialPrimitiveTyCons that represent kinds.22 * Kinds are now Types  The type `Kind` is just a synonym for `Type`. There are special !PrimitiveTyCons that represent kinds. 23 23 24 24 * Newtypes are implemented with coercions  The previous adhoc mechanism has been replaced with one that uses coercions. … … 35 35 probably not be used outside the few places it is already used. Type 36 36 reexports everything useful from !TypeRep, but exports the 37 representation abstractly. The datatype Typereally represents a37 representation abstractly. The datatype `Type` really represents a 38 38 single syntactic category that includes types, coercions, kinds, and 39 39 superkinds. … … 42 42 === Type Variables === 43 43 44 Type variables, of type Var, and associated construction and44 Type variables, of type `Var`, and associated construction and 45 45 manipulation 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 type48 checking. After typechecking, all !TcTyVars are turned to !TyVars.49 !TyVars carry a Bool field, isCoercionVar which is Trueif the type50 variable is a coercion variable and Falseotherwise. The function51 TyVar.isCoVarshould be used to test if a type variable is a coercion46 data constructors that make type variables, `TyVar` and `TcTyVar`. 47 `TcTyVar`s can be mutable tyvars that are instantiated during type 48 checking. After typechecking, all `TcTyVar`s are turned to `TyVar`s. 49 `TyVar`s carry a `Bool` field, `isCoercionVar`, which is `True` if the type 50 variable is a coercion variable and `False` otherwise. The function 51 `isCoVar` should be used to test if a type variable is a coercion 52 52 variable. 53 53 54 54 === Type Constructors === 55 55 56 Type constructors, of datatype !TyCon, are defined in the !TyCon module56 Type constructors, of datatype `TyCon`, are defined in the !TyCon module 57 57 and exported abstractly. There are several different sorts of type 58 58 constructors; the most important for understanding the overall 59 59 intermediate language type system are: 60 60 61 * !AlgTyCon, which are for tycons for datatypes and newtypes and have a field of type !AlgTyConRhswhich specified whether it is a datatype or newtype and contains further information for each;62 * !PrimTyCon, which are for builtin 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 superkinds, 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 !CoercionKindTyConcarry their kind67 in a field called tyConKind, and !CoercionKindTyConscarry their68 kinding rule (a function with type [Type] > Kind) in a field called69 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 builtin 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 superkinds, 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 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`. 70 70 71 71 === Kinds are Types === 72 72 73 73 We 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 now75 represented using type constructors, e.g. the kind *is represented as74 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 76 76 77 77 {{{star = TyConApp liftedTypeKindTyCon []}}} 78 78 79 where liftedTypeKindTyCon is a builtin !PrimTyCon. The arrow type80 constructor is used as the arrow kind constructor, e.g. the kind * >81 * is represented internally as79 where `liftedTypeKindTyCon` is a builtin `PrimTyCon`. The arrow type 80 constructor is used as the arrow kind constructor, e.g. the kind `* > 81 *` is represented internally as 82 82 83 83 {{{FunTy star star}}} … … 86 86 the typeKind function. The "Kind" of a kind is always one of the 87 87 sorts TY (for kinds that classify normal types) or CO (for kinds that 88 classify coercion evidence). The coercion kind, T1 :=: T2, is89 represented by !PredTy (!EqPred T1 T2).88 classify coercion evidence). The coercion kind, `T1 :=: T2`, is 89 represented by `PredTy (EqPred T1 T2)`. 90 90 91 91 GHC has a relatively complicated kind structure... … … 93 93 There's a little subtyping at the kind level. Here is the picture for 94 94 typekinds (kinds of sort TY). 95 95 96 {{{ 97 96 98 ? 97 99 / \ … … 112 114 (>) :: ?? > ? > * 113 115 (\(x::t) > ...) Here t::?? (i.e. not unboxed tuple) 116 114 117 }}} 115 118 … … 117 120 118 121 Coercions are typelevel terms which act as evidence for type 119 equalities and are classified by a new sort of kind (with the form T1120 :=: T2 ). Most of the coercion construction and manipulation functions122 equalities and are classified by a new sort of kind (with the form `T1 123 :=: T2`). Most of the coercion construction and manipulation functions 121 124 are found in the Coercion module. 122 125 123 126 The syntax of coercions extends the syntax of types (and the type 124 Coercion is just a synonym for Type). By representing coercion127 `Coercion` is just a synonym for `Type`). By representing coercion 125 128 evidence on the type level, we can take advantage of the existing 126 129 erasure mechanism and keep nontermination out of coercion proofs 127 130 (which is necessary to keep the system sound). The syntax of 128 131 coercions and types also overlaps a lot. A normal type is evidence 129 for the reflexive coercion, i.e. 132 for the reflexive coercion, i.e., 130 133 131 134 {{{Int :: Int :=: Int}}} 132 135 133 There are also coercion variables, which are represented as TyVar's 134 for which the isCoercionVar field is True. Coercion variables are 136 Coercion variables are 135 137 used to abstract over evidence of type equality, as in 136 138 … … 140 142 to implement some source language features (newtypes for now, 141 143 associated types soon and probably more in the future). Coercion 142 constants are represented as TyCons made with the constructor143 CoercionTyCon.144 constants are represented as `TyCon`s made with the constructor 145 `CoercionTyCon`. 144 146 145 147 Coercions are type level terms and can have normal type constructors applied 146 148 to them. The action of type constructors on coercions is much like in 147 a logical relation. So if c1 :: T1 :=: T2then149 a logical relation. So if `c1 :: T1 :=: T2` then 148 150 149 [c1] :: [T1] :=: [T2]150 151 and if c2 :: S1 :=: S2then152 153 c1 > c2 :: (T1 > S1 :=: T2 > S2)151 `[c1] :: [T1] :=: [T2]` 152 153 and if `c2 :: S1 :=: S2` then 154 155 `c1 > c2 :: (T1 > S1 :=: T2 > S2)` 154 156 155 157 The sharing of syntax means that a normal type can be looked at as 156 158 either a type or as coercion evidence, so we use two different kinding 157 relations, one to find typekinds (implemented as Type.typeKind ::158 Type > Kind ) and one to find coercionkinds (implementedas159 Coercion.coercionKind :: Coercion > Kind).159 relations, one to find typekinds (implemented in Type as `typeKind :: 160 Type > Kind`) and one to find coercionkinds (implemented in Coercion as 161 `coercionKind :: Coercion > Kind`). 160 162 161 163 Coercion variables are distinguished from type variables, and … … 174 176 175 177 In most of the compiler, as in the FC paper, coercions are abstracted 176 using !ForAllTy cv ty where cvis a coercion variable, with a kind of177 the form !PredTy (!EqPred T1 T2). However, during type inference it is178 using `ForAllTy cv ty` where `cv` is a coercion variable, with a kind of 179 the form `PredTy (EqPred T1 T2)`. However, during type inference it is 178 180 convenient to treat such coercion qualifiers in the same way other 179 181 class 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)) ty182 (where !PredTy (!EqPred T1 T2) is the kind of cv). Also, several of the dataConXXX functions treat equality182 functions like `tcSplitForAllTy` and `tcSplitPhiTy` and `tcSplitSigmaTy`, 183 treat `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 183 185 184 186 === Newtypes are coerced types ===