|
# Type Functions and Associated Types in GHC - The Master Plan
|
|
CONVERSION ERROR
|
|
|
|
|
|
|
|
Error: HttpError (HttpExceptionRequest Request {
|
|
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.
|
|
host = "ghc.haskell.org"
|
|
|
|
port = 443
|
|
## Aims
|
|
secure = True
|
|
|
|
requestHeaders = []
|
|
|
|
path = "/trac/ghc/wiki/TypeFunctions"
|
|
New features:
|
|
queryString = "?version=62"
|
|
|
|
method = "GET"
|
|
- Open type-indexed data types and type functions
|
|
proxy = Nothing
|
|
- 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.
|
|
rawBody = False
|
|
|
|
redirectCount = 10
|
|
|
|
responseTimeout = ResponseTimeoutDefault
|
|
Revised features
|
|
requestVersion = HTTP/1.1
|
|
|
|
}
|
|
- We may want to re-implement functional dependencies using associated type synonyms.
|
|
(StatusCodeException (Response {responseStatus = Status {statusCode = 403, statusMessage = "Forbidden"}, responseVersion = HTTP/1.1, responseHeaders = [("Date","Sun, 10 Mar 2019 06:59:38 GMT"),("Server","Apache/2.2.22 (Debian)"),("Strict-Transport-Security","max-age=63072000; includeSubDomains"),("Vary","Accept-Encoding"),("Content-Encoding","gzip"),("Content-Length","252"),("Content-Type","text/html; charset=iso-8859-1")], responseBody = (), responseCookieJar = CJ {expose = []}, responseClose' = ResponseClose}) "<!DOCTYPE HTML PUBLIC \"-//IETF//DTD HTML 2.0//EN\">\n<html><head>\n<title>403 Forbidden</title>\n</head><body>\n<h1>Forbidden</h1>\n<p>You don't have permission to access /trac/ghc/wiki/TypeFunctions\non this server.</p>\n<hr>\n<address>Apache/2.2.22 (Debian) Server at ghc.haskell.org Port 443</address>\n</body></html>\n"))
|
|
|
|
|
|
|
|
Original source:
|
|
We keep track of the current [implementation status](type-functions-status).
|
|
|
|
|
|
```trac
|
|
## Specification and Restrictions
|
|
= 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 F,,C,, intermediate code generation.
|
|
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).
|
|
|
|
|
|
== Aims ==
|
|
- Kind signatures of indexed data type families have the form
|
|
|
|
|
|
New features:
|
|
```wiki
|
|
* Open type-indexed data types and type functions
|
|
data family T a1 .. an [:: <kind>]
|
|
* 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
|
|
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 `*`). Newtypes families have the same form, except for the initial keyword.
|
|
* We may want to re-implement functional dependencies using associated type synonyms.
|
|
- Kind signatures of type function have the form
|
|
|
|
|
|
We keep track of the current [wiki:TypeFunctionsStatus implementation status].
|
|
```wiki
|
|
|
|
type family T a1 .. an [:: <kind>]
|
|
|
|
```
|
|
== Specification and Restrictions ==
|
|
|
|
|
|
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. Equations for an `n`-ary type function must specify exactly `n` arguments, which serve as indexes.
|
|
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 [wiki:TypeFunctionsExamples examples are on an extra page].
|
|
- Applications of type functions 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.)
|
|
* Kind signatures of indexed data type families have the form
|
|
- Instances of indexed data types/newtypes and equations of type functions have the keyword `instance` after the first keyword. They otherwise have the same form as ordinary data type/newtype and type synonym declarations, respectively, but can have non-variable type indexes as arguments. 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, the argument count of data and newtype instances must match the arity indicated by the kind. The number of arguments of a type equation must be equal to the number of type indexes (i.e., type variables in the head) of the family declaration.
|
|
data family T a1 .. an [:: <kind>]
|
|
- 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 and with the kind signature being compulsory.
|
|
}}}
|
|
- Instances of an assoicated 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`.
|
|
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 `*`). Newtypes families have the same form, except for the initial keyword.
|
|
- 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.
|
|
* Kind signatures of type function have the form
|
|
- 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.
|
|
{{{
|
|
- 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)`.
|
|
type family T a1 .. an [:: <kind>]
|
|
- 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 of indexed data and new types may not overlap (as such instances correspond to indeterminate type functions). 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 F<sub>C</sub> program that fulfils the formal consistency criterion.)
|
|
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. Equations for an `n`-ary type function must specify exactly `n` arguments, which serve as indexes.
|
|
- To enable indexed type families, the switch `-findexed-types` needs to be used (which is implied by `-fglasgow-exts`).
|
|
* Applications of type functions 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 indexed data types/newtypes and equations of type functions have the keyword `instance` after the first keyword. They otherwise have the same form as ordinary data type/newtype and type synonym declarations, respectively, but can have non-variable type indexes as arguments. 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, the argument count of data and newtype instances must match the arity indicated by the kind. The number of arguments of a type equation must be equal to the number of type indexes (i.e., type variables in the head) of the family declaration.
|
|
Restrictions:
|
|
* 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 assoicated 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`.
|
|
- 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.)
|
|
* 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.
|
|
## Terminology
|
|
* 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.
|
|
**Parametric type constructors**: Type constructors in vanilla Haskell.
|
|
* Instances of indexed data and new types may not overlap (as such instances correspond to indeterminate type functions). 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 F,,C,, program that fulfils the formal consistency criterion.)
|
|
|
|
* To enable indexed type families, the switch `-findexed-types` needs to be used (which is implied by `-fglasgow-exts`).
|
|
**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.
|
|
|
|
|
|
Restrictions:
|
|
**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.
|
|
* 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.)
|
|
|
|
|
|
**Type function**: An indexed type synonym.
|
|
|
|
|
|
== Terminology ==
|
|
**Indexed data type**: An indexed type constructor declared with `data` or `newtype`.
|
|
|
|
|
|
'''Parametric type constructors''': Type constructors in vanilla Haskell.
|
|
**Associated type**: An indexed type that is declared in a type class.
|
|
|
|
|
|
'''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.
|
|
**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.
|
|
|
|
|
|
'''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*.
|
|
|
|
|
|
'''Type function''': An indexed type synonym.
|
|
## How It Works
|
|
|
|
|
|
'''Indexed data type''': An indexed type constructor declared with `data` or `newtype`.
|
|
|
|
|
|
The details of the implementation are split over a couple of subpages, due to the amount of the material:
|
|
'''Associated type''': An indexed type that is declared in a type class.
|
|
|
|
|
|
- [syntax and representation,](type-functions-syntax)
|
|
'''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.
|
|
- [renaming,](type-functions-renaming)
|
|
|
|
- [type checking,](type-functions-type-checking)
|
|
'''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''.
|
|
- [desugaring,](type-functions-core) and
|
|
|
|
- [interfaces.](type-functions-iface)
|
|
|
|
|
|
== How It Works ==
|
|
|
|
|
|
We also have notes on [type checking with indexed synonyms.](type-functions-syn-tc)
|
|
The details of the implementation are split over a couple of subpages, due to the amount of the material:
|
|
|
|
* [wiki:TypeFunctionsSyntax syntax and representation,]
|
|
## Possible Extensions
|
|
* [wiki:TypeFunctionsRenaming renaming,]
|
|
|
|
* [wiki:TypeFunctionsTypeChecking type checking,]
|
|
- 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. |
|
* [wiki:TypeFunctionsCore desugaring,] and
|
|
|
|
* [wiki:TypeFunctionsIface interfaces.]
|
|
|
|
We also have notes on [wiki:TypeFunctionsSynTC type checking with indexed synonyms.]
|
|
|
|
|
|
|
|
== 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.
|
|
|
|
``` |