| 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`. |
| | 150 | where 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 | |
| | 152 | Neverthless, 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. |
| 160 | | |
| | 162 | The 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 | {{{ |
| | 164 | data T t1 .. tn b1 .. bm = C s1 .. sk |
| | 165 | }}} |
| | 166 | then we generate a wrapper |
| | 167 | {{{ |
| | 168 | C = /\c1..cr b1..bm -> |
| | 169 | \x1..xk -> |
| | 170 | Con C [c1,..,cr,b1,..,bm] [x1,..,xk] |> sym (cTinst@c1..@cr b1 .. bm) |
| | 171 | }}} |
| | 172 | The generation of constructor wrappers is performed by `MkId.mkDataConIds`. |
