|Version 82 (modified by chak, 7 years ago) (diff)|
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 families (aka type functions) and associated types, especially about the implications for type checking, interface files, and FC intermediate code generation.
Detailed information about implemented and unimplemented features as well as bugs and plans for further improvements is at implementation status. The following provides a summary:
- 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.
- Superclass equalities.
- Data family instances in GADT form.
- Closed or exhaustive synonym families.
- Re-implement functional dependencies using type families.
- 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).
Data-type family: a data type declared with a data family declaration.
Type-synonym family, or type function: a type synonym declared with a type family declaration.
Type family: a data-type family or type-synonym family.
Parametric type constructors: the type constructor of a vanilla Haskell type.
Family type constructor or Family TyCon: the type constructor for a type family.
Instance TyCon: the TyCon arising from a data/newtype/type instance declaration. Sometimes called the representation TyCon. The instance TyCon is invisible to the programmer; it is only used internally inside GHC.
Associated type: A type family that is declared in a type class.
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.
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.
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.
How It Works
The details of the implementation are split over a couple of subpages, due to the amount of the material:
- Associated Types with Class. 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. 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. Tom Schrijvers, Martin Sulzmann, Simon Peyton-Jones, and Manuel M. T. Chakravarty. Presented at IFL 2007.
- Type Checking with Open Type Functions. 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.