Changes between Version 32 and Version 33 of TypeFunctionsTypeChecking


Ignore:
Timestamp:
Aug 31, 2006 9:28:37 PM (8 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsTypeChecking

    v32 v33  
    8787=== Representation of newtype instances === 
    8888 
    89 We handle newtype instances similar to data instances.  However, newtypes have no separate worker and wrapper, but only a hybrid that is categorised as a worker (see `MkIds.mkDataConIds`).  In particular, this worker gets the wrapper signature as well as an unfolding.  The wrapper signature ensures that the result type of the constructor mentions the family constructor (and not the instance representation constructor).  The body of an ordinary newtype applies the newtype coercion to move from abstract to concrete type.  In the case of a family instance, we compose the newtype coercion with the family coercion to directly move from the abstract family instance to the concrete type. 
     89We handle newtype instances similar to data instances.  However, newtypes have no separate worker and wrapper, but only a hybrid that is categorised as a worker (see `MkIds.mkDataConIds`).  In particular, this worker gets the wrapper signature as well as an unfolding.  The wrapper signature ensures that the result type of the constructor mentions the family constructor (and not the instance representation constructor).  The body of an ordinary newtype applies the newtype coercion to move from abstract to concrete type.  In the case of a family instance, we compose the newtype coercion with the family coercion to directly move from the abstract family instance to the concrete type.  We apply the same idea in the opposite direction; cf. `MkIds.unwrapNewTypeBody`. 
    9090 
    9191=== Representation of equality axioms ===