Changes between Version 21 and Version 22 of IntermediateTypes


Ignore:
Timestamp:
Aug 4, 2006 4:06:58 PM (8 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) ==