Changes between Version 17 and Version 18 of IntermediateTypes
 Timestamp:
 Aug 4, 2006 3:08:52 PM (10 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

IntermediateTypes
v17 v18 74 74 datatype `Type`. `Kind` is just a synonym for `Type`. Basic kinds are now 75 75 represented using type constructors, e.g. the kind `*` is represented as 76 77 {{{star = TyConApp liftedTypeKindTyCon []}}} 78 76 {{{ 77 star = TyConApp liftedTypeKindTyCon [] 78 }}} 79 79 where `liftedTypeKindTyCon` is a builtin `PrimTyCon`. The arrow type 80 80 constructor is used as the arrow kind constructor, e.g. the kind `* > 81 81 *` is represented internally as 82 83 {{{FunTy star star}}} 84 82 {{{ 83 FunTy star star 84 }}} 85 85 Kinds and types may be distinguished by looking at their "Kind" using 86 86 the typeKind function. The "Kind" of a kind is always one of the … … 93 93 There's a little subtyping at the kind level. Here is the picture for 94 94 typekinds (kinds of sort TY). 95 96 95 {{{ 97 96 ? … … 147 146 to them. The action of type constructors on coercions is much like in 148 147 a logical relation. So if `c1 :: T1 :=: T2` then 149 150 `[c1] :: [T1] :=: [T2]` 151 148 {{{ 149 [c1] :: [T1] :=: [T2] 150 }}} 152 151 and if `c2 :: S1 :=: S2` then 153 154 `c1 > c2 :: (T1 > S1 :=: T2 > S2)` 155 152 {{{ 153 c1 > c2 :: (T1 > S1 :=: T2 > S2) 154 }}} 156 155 The sharing of syntax means that a normal type can be looked at as 157 156 either a type or as coercion evidence, so we use two different kinding