... | ... | @@ -64,6 +64,8 @@ Restrictions: |
|
|
|
|
|
**Associated type**: An indexed type that is declared in a type class.
|
|
|
|
|
|
**Type family**: Indexed types can be regarded as families of types; especially in the case of indexed data types, we call each declaration at a particular type index as *member* or *element* of that family.
|
|
|
|
|
|
**Definitions vs. declarations**: We sometimes call the kind signature of an indexed constructor its *declaration* and the subsequent population of the type family by type equations or indexed data/newtype declarations the constructor's *definition*.
|
|
|
|
|
|
## How It Works
|
... | ... | @@ -104,7 +106,7 @@ The LALR parser allows arbitrary types as left-hand sides in **data**, **newtype |
|
|
### Representation of associated types
|
|
|
|
|
|
|
|
|
We add type declarations to class declarations and instance declarations by a new field (of type `[LTyClDecl]`) to both `TyClDecl.ClassDecl` (known by the field name `tcdATs`) and `TyClDecl.InstDecl`. For classes, this new field contains values constructed from `TyData`, `TyFunction`, and `TySynonym`, whereas for instances, we only have `TyData` and `TySynonym`. This is due to (a) `TyData` representing both signatures and definitions of associated data types (whereas the two are split into `TyFunction` and `TySynonym` for associated synonyms) and (b) associated synonyms having default definitions, which associated data types do not possess.
|
|
|
We add type declarations to class declarations and instance declarations by a new field, of type `[LTyClDecl]`, to both `TyClDecl.ClassDecl` (known by the field name `tcdATs`) and `TyClDecl.InstDecl`. For classes, this new field contains values constructed from `TyData`, `TyFunction`, and `TySynonym`, whereas for instances, we only have `TyData` and `TySynonym`. This is due to (a) `TyData` representing both signatures and definitions of associated data types (whereas the two are split into `TyFunction` and `TySynonym` for associated synonyms) and (b) associated synonyms having default definitions, which associated data types do not possess.
|
|
|
|
|
|
### Phasing
|
|
|
|
... | ... | @@ -153,24 +155,76 @@ NB: Lifted associated type declarations inherit the context of the instance head |
|
|
|
|
|
---
|
|
|
|
|
|
---
|
|
|
### Type checking indexed data types
|
|
|
|
|
|
`Revise from here!`
|
|
|
|
|
|
---
|
|
|
Type checking in the presence of only indexed data and newtypes is much simpler than in the presence of type functions as type equality remains purely syntactic (i.e., we do not need to change the unification procedure). However, we need to check that the alternatives of a case expression inspecting an indexed data type contains only constructors of one member of the family. (To relax this restriction, we would need a story for compiling open data types.)
|
|
|
|
|
|
#### Desugaring indexed data types
|
|
|
|
|
|
|
|
|
The kind signature of an indexed data type
|
|
|
|
|
|
```wiki
|
|
|
data T (a1::<kind1>) .. (an::<kindn>) :: <kind>
|
|
|
```
|
|
|
|
|
|
|
|
|
turns into an F<sub>C</sub> type function declaration
|
|
|
|
|
|
```wiki
|
|
|
type T_n : <kind1> -> .. -> <kindn> -> <kind>
|
|
|
```
|
|
|
|
|
|
|
|
|
A member of an indexed data type
|
|
|
|
|
|
```wiki
|
|
|
data T t1 .. tn b1 .. bm = <constructors>
|
|
|
```
|
|
|
|
|
|
|
|
|
### Type checking associated data types
|
|
|
turns into an equality axiom and a vanilla data declaration
|
|
|
|
|
|
```wiki
|
|
|
axiom cTinst : (forall c1..cr. T_n t1 .. tn) :=: (forall c1..cr. Tinst c1 .. cn)
|
|
|
data Tinst c1 .. cr b1 .. bm = <constructors>
|
|
|
```
|
|
|
|
|
|
Type checking in the presence of only associated data types is much simpler than in the presence of associated type synonyms (or general type functions) as type equality remains purely syntactic (i.e., we do not need to change the unification procedure). However, we need to check that the alternatives of a case expression inspecting an associated data type contains only constructors defined within the same instances. (To relax this restriction, we would need a story for compiling open data types.)
|
|
|
|
|
|
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`.
|
|
|
|
|
|
Class declarations:
|
|
|
#### Inserting coercions
|
|
|
|
|
|
- As part of the knot typing exercises in `TcTyClsDecls.tcTyAndClassDecls`, we extract all AT declarations from classes and add them to the list of class and data type declarations to be processed. This ensures that AT declarations participate in kind checking and that they are entered into the global type-checker environment.
|
|
|
|
|
|
To ensure that the F<sub>C</sub> code generated by the above desugaring still type checks, we need to introduce cast expressions using `cTinst` to move between the indexed type `T_n` and the representation types, such as `Tinst`, of its members. The simplicity of type checking and desugaring indexed data types - as opposed to general type functions - is due to the locations where these casts need to be added being well defined. More precisely, there are two different kinds of locations corresponding to the introduction and elimination of indexed data types:
|
|
|
|
|
|
1. Wrappers for data constructors introduce indexed types.
|
|
|
1. Case expressions scrutinising indexed types eliminate them.
|
|
|
|
|
|
#### Wrappers for indexed types
|
|
|
|
|
|
### Type checking associated types
|
|
|
|
|
|
#### Class declarations
|
|
|
|
|
|
- As part of the knot tying exercises in `TcTyClsDecls.tcTyAndClassDecls`, we extract all AT declarations from classes and add them to the list of class and data type declarations to be processed. This ensures that AT declarations participate in kind checking and that they are entered into the global type-checker environment.
|
|
|
- We do *not* update the data declarations within class declarations (field `tcdATs` within `ClassDecl`), as the `Class.Class` structure produced by the type checker only contains the `Id`s of a classes associated types.
|
|
|
- We check that we have -fglasgow-exts.
|
|
|
|
|
|
#### Instance declarations
|
|
|
|
|
|
|
|
|
We need to handle ATs in `TcInstDcls.tcInstDecls1`, which is where the type information in instances - i.e., in vanilla Haskell just the instance heads - are processed.
|
|
|
|
|
|
### Representation of type functions after type checking
|
|
|
|
|
|
|
|
|
Type functions have a number of properties in common with class instances; in particular, they require a machinery for matching type patterns against types, as instance heads do during context simplification. Hence, we probably want some structure similar to `InstEnv.Instance` for type functions - for instances this is maintained in the field `iSpec` of `TcEnv.InstInfo` (for type functions we don't need anything like `iBinds` as they are pure type-level entities). If possible, it would be ideal if we can reuse (or generalise) some of the matching machinery for instance heads.
|
|
|
|
|
|
|
|
|
The essentials of a module after type checking are in `HscTypes.ModGuts`; in particular, we have two fields `mg_insts :: [Instance]` and `mg_binds :: [CoreRule]` containing all instance heads and all rewrite rules respectively. Similarly, we now want something like `mg_tyequa :: [TyEqua]` to represent all type euqations.
|
|
|
|
|
|
## Possible Extensions
|
|
|
|
|
|
- Our type-indexed data types are open. However, we currently don't allow case expressions mixing constructors from different indexes. We could do that if we had a story for open function definitions outside of classes. |