Changes between Version 21 and Version 22 of IntermediateTypes


Ignore:
Timestamp:
Aug 4, 2006 4:06:58 PM (9 years ago)
Author:
guest
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • IntermediateTypes

    v21 v22  
    202202=== Newtypes are coerced types ===
    203203
    204 The implementation of newtypes has changed to include explicit type coercions in the place of the previously used ad-hoc mechanism.  When a newtype
    205 
    206 {{{newtype T a = MkT (T a -> T a)}}}
    207 
    208 is declared, a new !TyCon called CoT is created, and is stored in the
    209 type constructor.  The new TyCon has the ame arity as the newtype type
    210 constructor, in this case one.  The TyCon does not have a kind on its
    211 own, only when fully applied to its arguments.  In this case we have
    212 
    213 {{{CoT Int ::  T Int :=: (T Int -> T Int)}}}
    214 
    215 This coercion is used to wrap and unwrap newtypes whenever the constructor or case is used in the Haskell source code.
    216 
    217 Such coercions are always used when the newtype is recursive and are optional for non-recursive newtypes.  This can be easily changed by altering the function mkNewTyConRhs in iface/BuildTyCl.lhs.
     204The implementation of newtypes has changed to include explicit type coercions in the place of the previously used ad-hoc mechanism. 
     205For a newtype declared by
     206{{{
     207newtype T a = MkT (a -> a)
     208}}}
     209the `NewTyCon` for `T` will contain n`t_co = CoT` where `CoT t : T t :=: t ->
     210t`.  This `TyCon` is a `CoercionTyCon`, so it does not have a kind on its
     211own; it basically has its own typing rule for the fully-applied
     212version.  If the newtype `T` has k type variables hen `CoT` has arity at
     213most k.  In the case that the right hand side is a type application
     214ending with the same type variables as the left hand side, we
     215"eta-contract" the coercion.  So if we had
     216{{{
     217newtype S a = MkT [a]
     218}}}
     219then we would generate the arity 0 coercion `CoS : S :=: []`.  The
     220primary reason we do this is to make newtype deriving cleaner.  If the coercion
     221cannot be reduced in this fashion, then it has the same arity as the tycon.
     222
     223In the paper we'd write
     224{{{
     225        axiom CoT : (forall t. T t) :=: (forall t. [t])
     226}}}
     227and then when we used `CoT` at a particular type, `s`, we'd say
     228{{{
     229        CoT @ s
     230}}}
     231which encodes as `(TyConApp instCoercionTyCon [TyConApp CoT [], s])`
     232
     233But in GHC we instead make `CoT` into a new piece of type syntax
     234(like `instCoercionTyCon`, `symCoercionTyCon` etc), which must always
     235be saturated, but which encodes as
     236{{{
     237TyConApp CoT [s]
     238}}}
     239In the vocabulary of the paper it's as if we had axiom declarations
     240like
     241{{{
     242axiom CoT t :  T t :=: [t]
     243}}}
     244The newtype coercion is used to wrap and unwrap newtypes whenever the constructor or case is used in the Haskell source code.
     245
     246Such coercions are always used when the newtype is recursive and are optional for non-recursive newtypes.  Whether or not they are used can be easily changed by altering the function mkNewTyConRhs in iface/BuildTyCl.lhs.
    218247
    219248== Core (the intermediate language) ==