Changes between Version 17 and Version 18 of IntermediateTypes


Ignore:
Timestamp:
Aug 4, 2006 3:08:52 PM (9 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