Changes between Version 17 and Version 18 of IntermediateTypes


Ignore:
Timestamp:
Aug 4, 2006 3:08:52 PM (8 years ago)
Author:
guest
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • IntermediateTypes

    v17 v18  
    7474datatype `Type`.  `Kind` is just a synonym for `Type`.  Basic kinds are now 
    7575represented using type constructors, e.g. the kind `*` is represented as 
    76        
    77       {{{star = TyConApp liftedTypeKindTyCon []}}} 
    78  
     76{{{ 
     77star = TyConApp liftedTypeKindTyCon [] 
     78}}} 
    7979where `liftedTypeKindTyCon` is a built-in `PrimTyCon`.  The arrow type 
    8080constructor is used as the arrow kind constructor, e.g. the kind `* -> 
    8181*` is represented internally as 
    82  
    83       {{{FunTy star star}}} 
    84  
     82{{{ 
     83FunTy star star 
     84}}} 
    8585Kinds and types may be distinguished by looking at their "Kind" using 
    8686the typeKind function.  The "Kind" of a kind is always one of the 
     
    9393There's a little subtyping at the kind level.  Here is the picture for 
    9494type-kinds (kinds of sort TY). 
    95  
    9695{{{ 
    9796                 ? 
     
    147146to them.  The action of type constructors on coercions is much like in 
    148147a logical relation.  So if `c1 :: T1 :=: T2` then 
    149   
    150     `[c1] :: [T1] :=: [T2]` 
    151  
     148 {{{ 
     149[c1] :: [T1] :=: [T2] 
     150}}} 
    152151and if `c2 :: S1 :=: S2` then 
    153  
    154     `c1 -> c2 :: (T1 -> S1 :=: T2 -> S2)` 
    155  
     152{{{ 
     153c1 -> c2 :: (T1 -> S1 :=: T2 -> S2) 
     154}}} 
    156155The sharing of syntax means that a normal type can be looked at as 
    157156either a type or as coercion evidence, so we use two different kinding