wiki:TypeFunctions

Version 83 (modified by chak, 6 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.

Status

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:

Implemented 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.

Missing features:

  • Superclass equalities.
  • Data family instances in GADT form.
  • Total type families.
  • Closed synonym families.
  • Re-implement functional dependencies using type families.

Speculative ideas:

  • 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

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:

References