Changes between Version 3 and Version 4 of IntermediateTypes


Ignore:
Timestamp:
Aug 4, 2006 12:44:59 PM (9 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