Changes between Version 3 and Version 4 of IntermediateTypes


Ignore:
Timestamp:
Aug 4, 2006 12:44:59 PM (8 years ago)
Author:
guest
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • IntermediateTypes

    v3 v4  
    88 
    99Most of the system is fairly standard, with the exception of 
    10 coercions.  A coercion c, is a type-level term, with a kind of the 
    11 form T1 :=: T2. (c :: T1 :=: T2) is a proof that a term of type T1 
    12 can be coerced to type T2.  It is used as argument of a cast 
    13 expression; if t :: T1 then (t `cast` c) :: T2. 
    14  
     10coercions.  A coercion `c`, is a type-level term, with a kind of the 
     11form `T1 :=: T2`. (`c :: T1 :=: T2`) is a proof that a term of type `T1` 
     12can be coerced to type `T2`.  It is used as argument of a cast 
     13expression; if `t :: T1` then {{{(t `cast` c) :: T2}}}.   
     14 
     15= What's New? = 
     16 
     17If you are already familiar with the intermediate language and its type system as it existed in 6.4.2 (and probably before) then 
     18the key aspects that have changed are (and are further described in several sections below): 
     19 
     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 
     22 * Kinds are now Types - The type Kind is just a synonym for Type.  There are special PrimitiveTyCons that represent kinds. 
     23 
     24 * Newtypes are implemented with coercions - The previous ad-hoc mechanism has been replaced with one that uses coercions. 
     25 
     26 * GADTs are implemented with coercions - The complex typing rules for case expressions on GADTs have been removed and instead the data constructors of GADTs carry coercions inside them.  Consequently, typechecking Core is simpler (though type inference is just as hard as ever). 
     27 
     28For anyone not familiar with the system as it existed previously, the rest of this note attempts to describe most of the type system of the intermediate language. 
    1529 
    1630== Types == 
    1731 
    18 The representation of types is defined (as the datatype Type) in 
     32The representation of types is defined (as the datatype `Type`) in 
    1933!TypeRep, and most of the useful functions on types are defined in 
    2034Type.  TypeRep exports the representation concretely, and should