... | @@ -54,7 +54,7 @@ Restrictions: |
... | @@ -54,7 +54,7 @@ Restrictions: |
|
|
|
|
|
**Parametric type constructors**: Type constructors in vanilla Haskell.
|
|
**Parametric type constructors**: Type constructors in vanilla Haskell.
|
|
|
|
|
|
**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*.
|
|
**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.
|
|
|
|
|
|
**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.
|
|
**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.
|
|
|
|
|
... | @@ -187,12 +187,15 @@ data T t1 .. tn b1 .. bm = <constructors> |
... | @@ -187,12 +187,15 @@ data T t1 .. tn b1 .. bm = <constructors> |
|
turns into an equality axiom and a vanilla data declaration
|
|
turns into an equality axiom and a vanilla data declaration
|
|
|
|
|
|
```wiki
|
|
```wiki
|
|
axiom cTinst : (forall c1..cr. T_n t1 .. tn) :=: (forall c1..cr. Tinst c1 .. cn)
|
|
axiom cTinst : (forall c1..cr. T_n t1 .. tn) :=: (forall c1..cr. Tinst c1 .. cr)
|
|
data Tinst c1 .. cr b1 .. bm = <constructors>
|
|
data Tinst c1 .. cr b1 .. bm = <constructors>
|
|
```
|
|
```
|
|
|
|
|
|
|
|
|
|
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`.
|
|
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<sub>C</sub> 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.
|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
|
#### Inserting coercions
|
|
#### Inserting coercions
|
|
|
|
|
... | @@ -204,6 +207,25 @@ To ensure that the F<sub>C</sub> code generated by the above desugaring still ty |
... | @@ -204,6 +207,25 @@ To ensure that the F<sub>C</sub> code generated by the above desugaring still ty |
|
|
|
|
|
#### Wrappers for indexed types
|
|
#### Wrappers for indexed types
|
|
|
|
|
|
|
|
|
|
|
|
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)
|
|
|
|
|
|
|
|
```wiki
|
|
|
|
data T t1 .. tn b1 .. bm = C s1 .. sk
|
|
|
|
```
|
|
|
|
|
|
|
|
|
|
|
|
then we generate a wrapper
|
|
|
|
|
|
|
|
```wiki
|
|
|
|
C = /\c1..cr b1..bm ->
|
|
|
|
\x1..xk ->
|
|
|
|
Con C [c1,..,cr,b1,..,bm] [x1,..,xk] |> sym (cTinst@c1..@cr b1 .. bm)
|
|
|
|
```
|
|
|
|
|
|
|
|
|
|
|
|
The generation of constructor wrappers is performed by `MkId.mkDataConIds`.
|
|
|
|
|
|
### Type checking associated types
|
|
### Type checking associated types
|
|
|
|
|
|
#### Class declarations
|
|
#### Class declarations
|
... | | ... | |