Changes between Version 38 and Version 39 of TypeFunctions


Ignore:
Timestamp:
Aug 3, 2006 7:02:35 PM (9 years ago)
Author:
chak
Comment:

Type checking indexed types (II)

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctions

    v38 v39  
    4343'''Parametric type constructors''': Type constructors in vanilla Haskell.
    4444
    45 '''Indexed type constructors''': Type constructors that are defined via one or more type declarations that have non-variable parameters.  We often call them sloppily just ''indexed types''.
     45'''Indexed type constructors''': Type constructors that are defined via one or more type declarations that have non-variable parameters.  We often call them sloppily just ''indexed types''.  We informally call constructors that are not indexed ''vanilla'' constructors.
    4646
    4747'''Kind signature''': Declaration of the name, kind, and arity of an indexed type constructor.  The ''arity'' is the number of type indexes - ''not'' the overall number of parameters - of an indexed type constructor.
     
    145145turns into an equality axiom and a vanilla data declaration
    146146{{{
    147 axiom cTinst : (forall c1..cr. T_n t1 .. tn) :=: (forall c1..cr. Tinst c1 .. cn)
     147axiom cTinst : (forall c1..cr. T_n t1 .. tn) :=: (forall c1..cr. Tinst c1 .. cr)
    148148data Tinst c1 .. cr b1 .. bm = <constructors>
    149149}}}
    150 where the `ci` are the free variables of the `tj`.  Moreover, we replace all occurences of `T` in the rest of the program by `T_n`.
     150where the `ci` are the free variables of the `tj`.  Moreover, we morally replace all occurences of `T` in the rest of the program by `T_n`.  No such replacement is required in the actual implementation as the arity index at F,,C,, type functions is just a formal device used in the formal development.  In the implementation, it is perfectly fine to retain the original name and maintain the arity information separately.
     151
     152Neverthless, we need to generate a new name for the vanilla data types representing family members (i.e., `Tinst` above).  We use a similar mechanism as for the generation of the dictionary type constructors of type classes.  In particular, we generalise the field `algTcClass` of the internal representation for datatypes, `TyCon.AlgTyCon`, to be three valued: none, `Class` for data types representing dictionaries, and <which structure?> for data types representing members of a family.
    151153
    152154==== Inserting coercions ====
     
    158160==== Wrappers for indexed types ====
    159161
    160 
     162The wrapper of a data constructor acts as an impedance matcher between the source-level signatures of the constructor and its actual representation; in particular, it evaluates strict arguments and unboxes flattened arguments.  In the case of a constructor for an indexed data type, it additionally has to apply the coercion between the type function representing the source type and its representation as a vanilla data type.  So, for example, if we have (continuing the example from above)
     163{{{
     164data T t1 .. tn b1 .. bm = C s1 .. sk
     165}}}
     166then we generate a wrapper
     167{{{
     168C = /\c1..cr b1..bm ->
     169    \x1..xk ->
     170      Con C [c1,..,cr,b1,..,bm] [x1,..,xk] |> sym (cTinst@c1..@cr b1 .. bm)
     171}}}
     172The generation of constructor wrappers is performed by `MkId.mkDataConIds`.
    161173
    162174=== Type checking associated types ===