|
|
# Type Functions and Associated Types in GHC - The Master Plan
|
|
|
# Type Functions, Type Families, and Associated Types in GHC - The Master Plan
|
|
|
|
|
|
|
|
|
This page serves as a collection of notes concerning the implementation of type functions and associated types, especially about the implications for type checking, interface files, and F<sub>C</sub> intermediate code generation.
|
|
|
This page serves as a collection of notes concerning the implementation of type families (aka type functions) and associated types, especially about the implications for type checking, interface files, and F<sub>C</sub> intermediate code generation.
|
|
|
|
|
|
## Aims
|
|
|
## Status
|
|
|
|
|
|
|
|
|
New features:
|
|
|
Detailed information about implemented and unimplemented features as well as bugs and plans for further improvements is at [implementation status](type-functions-status). The following provides a summary:
|
|
|
|
|
|
- Open type-indexed data types and type functions
|
|
|
- Associated data types and type synonyms, which are type-indexed data types and type functions associated with a class - i.e., associated types are syntactic sugar for type-indexed types and type functions.
|
|
|
|
|
|
Implemented features:
|
|
|
|
|
|
Revised features
|
|
|
- All basic functionality of open data type families, open type synonym families, and equality constraints has been implemented.
|
|
|
- Type checking is fully integrated with GADTs.
|
|
|
|
|
|
- We may want to re-implement functional dependencies using associated type synonyms.
|
|
|
|
|
|
Missing features:
|
|
|
|
|
|
We keep track of the current [implementation status](type-functions-status).
|
|
|
- Superclass equalities.
|
|
|
- Data family instances in GADT form.
|
|
|
- [Total type families.](type-functions/total-families)
|
|
|
- Closed synonym families.
|
|
|
- Re-implement functional dependencies using type families.
|
|
|
|
|
|
|
|
|
We also have notes on [type checking with indexed synonyms.](type-functions-syn-tc)
|
|
|
Speculative ideas:
|
|
|
|
|
|
|
|
|
A related extension are [class families.](type-functions/class-families)
|
|
|
- [Class families.](type-functions/class-families)
|
|
|
- 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. Class instances of entire data families (including `deriving` clauses at family declarations to derive for all instances) requires the same sort of capabilities as case expressions mixing data constructors from different indexes. This is, as they require to build a dictionary that applies to all family instances (as opposed to a distinct dictionary per instance, which is what we have now).
|
|
|
|
|
|
## Terminology
|
|
|
|
... | ... | @@ -48,48 +52,6 @@ A related extension are [class families.](type-functions/class-families) |
|
|
|
|
|
Note: we previously used the term "indexed type", but have now switched to using "type family". Please change any uses of the former into the latter as you come across them.
|
|
|
|
|
|
## Specification and Restrictions
|
|
|
|
|
|
|
|
|
The user-level definition of the type-family extensions is given here [ http://haskell.org/haskellwiki/GHC/Indexed_types](http://haskell.org/haskellwiki/GHC/Indexed_types). Section 4, "Definition of the type system extension" constitues the specification.
|
|
|
|
|
|
|
|
|
Refinement of the specification in the *Beyond Associated Types* paper. (I'll actually link this paper here once it is a bit more coherent.) Some [examples are on an extra page](type-functions-examples).
|
|
|
|
|
|
- Kind signatures of indexed data type families have the form
|
|
|
|
|
|
```wiki
|
|
|
data family T a1 .. an [:: <kind>]
|
|
|
```
|
|
|
|
|
|
and introduce a type family whose kind is determined by the kinds of the `ai` (which can have kind annotations) and the optional signature `<kind>` (which defaulys to `*`).
|
|
|
- Kind signatures of type function have the form
|
|
|
|
|
|
```wiki
|
|
|
type family T a1 .. an [:: <kind>]
|
|
|
```
|
|
|
|
|
|
and introduce `n`-ary type functions (with `n` \>= 1), which may be of higher-kind. Again, the type variables can have kind signatures and the result kind signature is optional, with `*` being the default. Type instances for an `n`-ary type function must specify exactly `n` arguments, which serve as indexes.
|
|
|
- Applications of type synonym families need to supply all indexes after unfolding of all ordinary type synonyms. (This is the same saturation requirement that we already have on ordinary type synonyms.)
|
|
|
- Instances of data and type families have the keyword `instance` after the first keyword. They otherwise have the same form as ordinary data type and type synonym declarations, respectively, but can have non-variable type indexes as arguments. Type indexes can include applications of data families, but no type synonym families.
|
|
|
- Instances of type families are only valid if a kind signature for the type constructor is in scope. The kind of an indexed type is solely determined from the kind signature. Instances must conform to this kind. In particular, the argument count of data and newtype instances must match the arity indicated by the kind. The number of arguments of a type synonym instance must be equal to the number of type indexes (i.e., type variables in the head) of the family declaration. Instances of data families can be both data types or newtypes (or a mix of the two).
|
|
|
- Data family instances can have deriving clauses as usual (but they do not support the non-standard deriving of `Typeable`).
|
|
|
- Associated types are type families declared as part of a type class. The syntax of family declarations in class declarations and of type instance declarations in instance declarations is as for toplevel declarations, but without the `family` and `instance` keywords.
|
|
|
- Instances of an associated type can only be defined in instances of its class. However, it is admissible to omit the type definition in instances of the class (similar to how methods may be omitted). Then, the only inhabitant of the corresponding type is `undefined`.
|
|
|
- All argument variables of an associated type family declaration need to be class parameters. There may not be any repetitions, but the order of the variables can differ from that in the class head and the type family can be defined over a subset of the class parameters.
|
|
|
- In instances, the type indexes of a type declaration must be identical to the corresponding class parameters (i.e., those that share the same variable name in the class declaration). And all arguments that where not connected to a class parameter in the family declaration must be variables; i.e., cannot be used as type indexes.
|
|
|
- Type contexts (including super class and instance contexts) can have equational constraints of the form `t1 ~ t2`, where the two types `t1` and `t2` need to be rank 0 types.
|
|
|
- In an export and import list, associated types are treated as subcomponents of their type class, just like the class methods. In particular, `C(..)` denotes class `C` with all its methods and all its associated types. If the associated types of a class are explicitly listed in the parenthesis, each type name needs to be prefixed with the keyword `type`; i.e., to denote class `C` with associated type `T` and method `foo`, we write `C(type T, foo)`.
|
|
|
- In export and import lists, all data constructors of newtype and data families defined in any newtype or data instance is regarded to be a subcomponent of the family type constructor, and hence specified by `F(..)` if `F` is the family type constructor. Instead of specifying them all with "`..`", they can also be explicitly listed, just as with vanilla data types.
|
|
|
- Instances data families may not overlap (as such instances correspond to indeterminate type functions). Type synonym instances may overlap if the right-hand sides are syntactically equal under the overlap substitution. (Rational: We cannot be more lazy about checking overlap, as we otherwise cannot guarantee that we generate an F<sub>C</sub> program that fulfils the formal consistency criterion.)
|
|
|
- FFI signatures do not look through indexed newtypes nor through indexed synonyms. (The main reason for not looking through indexed synonyms is as they may occur in the rhs of a vanilla newtype.)
|
|
|
- To enable indexed type families, the switch `-ftype-families` needs to be used (which is implied by `-fglasgow-exts`).
|
|
|
|
|
|
|
|
|
Restrictions:
|
|
|
|
|
|
- We currently don't allow indexed GADTs. I cannot see any fundamental problem in supporting them, but I want to keep it simple for the moment. (When allowing this, a constructor signature in an associated GADT can of course only refine the instantiation of the type arguments specific to the instance in which the constructor is defined.)
|
|
|
|
|
|
## How It Works
|
|
|
|
|
|
|
... | ... | @@ -101,7 +63,10 @@ The details of the implementation are split over a couple of subpages, due to th |
|
|
- [desugaring,](type-functions-core) and
|
|
|
- [interfaces.](type-functions-iface)
|
|
|
|
|
|
## Possible Extensions
|
|
|
## References
|
|
|
|
|
|
- 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.
|
|
|
- Class instances of entire data families (including `deriving` clauses at family declarations to derive for all instances) requires the same sort of capabilities as case expressions mixing data constructors from different indexes. This is, as they require to build a dictionary that applies to all family instances (as opposed to a distinct dictionary per instance, which is what we have now). |
|
|
- [ Associated Types with Class.](http://www.cse.unsw.edu.au/~chak/papers/CKPM05.html) Manuel M. T. Chakravarty, Gabriele Keller, Simon Peyton Jones, and Simon Marlow. In Proceedings of The 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05), ACM Press, pages 1-13, 2005.
|
|
|
- [ Associated Type Synonyms.](http://www.cse.unsw.edu.au/~chak/papers/CKP05.html) Manuel M. T. Chakravarty, Gabriele Keller, and Simon Peyton Jones. In Proceedings of The Tenth ACM SIGPLAN International Conference on Functional Programming, ACM Press, pages 241-253, 2005.
|
|
|
- [ Towards Open Type Functions for Haskell.](http://www.cse.unsw.edu.au/~chak/papers/SSPC07.html) Tom Schrijvers, Martin Sulzmann, Simon Peyton-Jones, and Manuel M. T. Chakravarty. Presented at IFL 2007.
|
|
|
- [ Type Checking with Open Type Functions.](http://www.cse.unsw.edu.au/~chak/papers/SPCS08.html) Tom Schrijvers, Simon Peyton-Jones, Manuel M. T. Chakravarty, and Martin Sulzmann. Unpublished draft.
|
|
|
- Old and outdated wiki material on [type checking with indexed synonyms.](type-functions-syn-tc) |
|
|
\ No newline at end of file |