wiki:TypeFunctions

Version 45 (modified by chak, 8 years ago) (diff)

--

Type Functions 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 FC intermediate code generation.

Aims

New features:

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

Revised features

  • We may want to re-implement functional dependencies using associated type synonyms.

We keep track of the current implementation status.

Specification and Restrictions

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.

  • Kind signatures of indexed data types have the form
    data T a1 .. an :: <kind>
    
    and introduce a data type whose first n argument are indexes, with n >= 1. The <kind> can specify additional parametric parameters. Index variables can have a kind annotation. Indexed newtypes have the same form, except for the keyword.
  • Kind signatures of type functions have the form
    type [iso] T a1 .. an :: <kind>
    
    and introduce an n-ary type functions, which may be of higher-kind, with n >= 1. Again, the type variables can have kind signatures. The modifier iso is optional and requires the type function to be injective. (In principle, we could make the <kind> optional, with * being the default, but we don't do that for uniformity with signatures of indexed types - the form data T a1 .. an is already used for empty data types.)
  • Applications of indexed types need to supply all indexes; i.e., partial application to indexes is not admitted. (Arguments beyond the indexes can be partially supplied as usual.)
  • Instances of indexed data types/newtypes and equations of type functions have the same form as vanilla data types/newtypes and type synonyms, respectively, but can have non-variable type indexes in index positions. Type indexes can include applications of indexed data types and newtypes, but no type functions.
  • Instances of indexed types 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, they must have the same number of type indexes.
  • The degenerate case of a data type/newtype declaration or type equation where all type parameters are variables is valid without a kind signature and coincides with the data types and type synonyms of vanilla Haskell. In fact, for the moment, we do not allow the degenerate case to have a kind signature. The latter constraint could be dropped if it proves to be inconvenient. (Rationale: Multiple type equations are useless when one is degenerate - as the whole system needs to be confluent and we don't have sequential matching on type equations. So, we get backwards compatibility for free.)
  • All type indexes of an associated indexed type or type function need to be class parameters.
  • Instances of indexed types may not overlap. Instances of type equations may only overlap if the equations coincide at critical pairs. (Rational: We cannot be more lazy about checking overlap, as we otherwise cannot guarantee that we generate an FC program that fulfils the formal consistency criterion.)

Restrictions:

  • We currently don't allow associated 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.)

Terminology

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

Type function: An indexed type synonym.

Indexed data type: An indexed type constructor declared with data or newtype.

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

The details of the implementation are split over a couple of subpages, due to the amount of the material:

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.