|
|
# 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<sub>C</sub> 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](type-functions-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](type-functions-examples).
|
|
|
|
|
|
- Kind signatures of indexed data types have the form
|
|
|
|
|
|
```wiki
|
|
|
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
|
|
|
|
|
|
```wiki
|
|
|
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.) **We probably want the saturation constraint only for type functions, not for data/newtype families.**
|
|
|
- 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 F<sub>C</sub> 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:
|
|
|
|
|
|
- [syntax and representation,](type-functions-syntax)
|
|
|
- [renaming,](type-functions-renaming)
|
|
|
- [type checking,](type-functions-type-checking) and
|
|
|
- [representation in Core and in interfaces.](type-functions-core)
|
|
|
|
|
|
## 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. |
|
|
CONVERSION ERROR
|
|
|
|
|
|
Error: HttpError (HttpExceptionRequest Request {
|
|
|
host = "ghc.haskell.org"
|
|
|
port = 443
|
|
|
secure = True
|
|
|
requestHeaders = []
|
|
|
path = "/trac/ghc/wiki/TypeFunctions"
|
|
|
queryString = "?version=47"
|
|
|
method = "GET"
|
|
|
proxy = Nothing
|
|
|
rawBody = False
|
|
|
redirectCount = 10
|
|
|
responseTimeout = ResponseTimeoutDefault
|
|
|
requestVersion = HTTP/1.1
|
|
|
}
|
|
|
(StatusCodeException (Response {responseStatus = Status {statusCode = 403, statusMessage = "Forbidden"}, responseVersion = HTTP/1.1, responseHeaders = [("Date","Sun, 10 Mar 2019 06:53:48 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:
|
|
|
|
|
|
```trac
|
|
|
= 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.
|
|
|
|
|
|
== 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 [wiki:TypeFunctionsStatus 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 [wiki:TypeFunctionsExamples examples are on an extra page].
|
|
|
* Kind signatures of indexed data type families have the form
|
|
|
{{{
|
|
|
data family 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 initial keyword. '''Is it still necessary to know the number of type indexes (now that we don't require saturated applications for indexed data types)? We can now also admit the omission of the kind with * being the default.'''
|
|
|
* Kind signatures of type functions have the form
|
|
|
{{{
|
|
|
type family [iso] T a1 .. an :: <kind>
|
|
|
}}}
|
|
|
and introduce `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. '''Not true anymore.''')
|
|
|
* Applications of type functions need to supply all indexes after unfolding of all ordinary type synonyms. (This is the same saturation requirement that we walready 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 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.
|
|
|
* 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 F,,C,, 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:
|
|
|
* [wiki:TypeFunctionsSyntax syntax and representation,]
|
|
|
* [wiki:TypeFunctionsRenaming renaming,]
|
|
|
* [wiki:TypeFunctionsTypeChecking type checking,] and
|
|
|
* [wiki:TypeFunctionsCore representation in Core and in interfaces.]
|
|
|
|
|
|
|
|
|
== 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.
|
|
|
``` |