Changes between Version 36 and Version 37 of TypeFunctions


Ignore:
Timestamp:
Aug 3, 2006 5:03:48 PM (9 years ago)
Author:
chak
Comment:

Align implementation description with actual code plus add terminology section

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctions

    v36 v37  
    3838 * 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.)
    3939
     40== Terminology ==
     41
     42'''Parametric type constructors''': Type constructors in vanilla Haskell.
     43
     44'''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''.
     45
     46'''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.
     47
     48'''Type function''': An indexed type synonym.
     49
     50'''Indexed data type''': An indexed type constructor declared with `data` or `newtype`.
     51
     52'''Associated type''': An indexed type that is declared in a type class.
     53
     54'''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''.
     55
    4056== How It Works ==
    4157
    42 === Syntax of type functions ===
     58=== Syntax of kind signatures and definitions of indexed types ===
    4359
    44 Type function (kind) signatures are represented by the new declaration form `TyFunction` (of `HsDecls.TyClDecl`).  Syntactically, we recognise kind signatures by either not having an RHS at all (in which the result kind implicitly is *) or having a result kind separated from the head by {{{::}}}.  We require that every type equation has a kind signature in scope.  However, the degenerate case of a type equation where all type arguments are variables is valid without a kind signature (in fact, it may not have any) and coincides with the type synonyms of vanilla Haskell.
     60All kind signature consists of a type declaration head followed by a `::` and a kind.  In the case of  a data declaration, we addititonally require that there is no `where` clause.   We require for every definition of an indexed type (i.e., type equations or indexed data/newtype declaration) that a matching kind signature is in scope.  Vanilla type synonym definitions and data/newtype declarations fall out as special cases of type function equations and indexed type declarations that have variable-only patterns, for which we require no kind signatures.  The vanilla forms are also closed (further definitions would be useless, as they are bound to overlap).
    4561
    4662=== Representation of indexed types ===
    4763
    48 ==== Type function signatures ====
     64==== Kind signatures ====
    4965
    50 `HsDecls.TyClDecl` has a new variant `TyFunction` to represent signatures of type functions.  These consist of the name, type parameters, an iso flag, and optionally an explicit result kind.  The type parameters can have kind signatures as usual.
     66`HsDecls.TyClDecl` has a new variant `TyFunction` to represent signatures of type functions.  These consist of the name, type parameters, an iso flag, and optionally an explicit result kind.  The type parameters can have kind signatures as usual. 
    5167
    52 ==== Type function equations and associated data types ====
     68Signatures for indexed data and newtypes are represented as a special case of `TyData`, namely when `TyData` has a kind signature, but no constructors.
    5369
    54 To represent type functions and associated data types, we need to generalise data type declarations `TyData` and type synonym declarations `TySynonym` to allow type patterns instead of just type variables as parameters.  We do so by way of the field `tcdPats` of type `Maybe [LHsType name]`, used as follows:
     70We recognise both forms of kind signatures by the predicate `HsDecls.isKindSigDecl`.
     71
     72==== Definitions of indexed types ====
     73
     74We represent type functions and indexed data and newtypes by generalising type synonym declarations `TySynonym` and data type declarations `TyData` to allow patterns ofr type indexes instead of just type variables as parameters.  In both variants, we do so by way of the field `tcdPats` of type `Maybe [LHsType name]`, used as follows:
    5575 * If it is `Nothing`, we have a ''vanilla'' data type declaration or type synonym declaration and `tcdVars` contains the type parameters of the type constructor.
    56  * If it is `Just pats`, we have the definition of an associated data type or a type function equations (toplevel or nested in an instance declarations).  Then, 'pats' are type patterns for the type-indexes of the type constructor and `tcdVars` are the variables in those patterns.  Hence, the arity of the type constructor is `length tcdPats` and ''not'' `length tcdVars`.
    57 In both cases (and as before type functions), `tcdVars` collects all variables we need to quantify over.
     76 * If it is `Just pats`, we have the definition of an a indexed type (toplevel or nested in an instance declarations).  Then, 'pats' are type patterns for the type-indexes of the type constructor and `tcdVars` are the variables in those patterns.  Hence, the arity of the type constructor is `length tcdPats` and ''not'' `length tcdVars`.
     77In both cases (and as before we had type functions), `tcdVars` collects all variables we need to quantify over.
    5878
    5979==== Parsing and AST construction ====
    6080
    61 The LALR parser allows arbitrary types as left-hand sides in '''data''' and '''type''' declarations.  The parsed type is, then, passed to {{{RdHsSyn.checkTyClHdr}}} for closer analysis (possibly via `RdHsSyn.checkSynHdr`).  It decomposes the type and, among other things, yields the type arguments in their original form plus all type variables they contain.  Subsequently, {{{RdrHsSyn.checkTyVars}}} is used to either enforce that all type arguments are variables (second argument is `False`) or to simply check whether the type arguments are variables (second argument `True`).  If in enforcing mode, `checkTyVars` will raise an error if it encounters a non-variable (e.g., required for class declarations).  If in checking mode, it yields the value placed in the `tcdPats` field described above; i.e., returns `Nothing` instead of the type arguments if these arguments are all only variables.
    62 
    63 NB: Some well-formedness checks are left for the renamer to do.  For example, we don't enforce at this point that toplevel data declarations use variable-only heads (as this requires context information not available during parsing).
     81The LALR parser allows arbitrary types as left-hand sides in '''data''', '''newtype''', and '''type''' declarations.  The parsed type is, then, passed to {{{RdHsSyn.checkTyClHdr}}} for closer analysis (possibly via `RdHsSyn.checkSynHdr`).  It decomposes the type and, among other things, yields the type arguments in their original form plus all type variables they contain.  Subsequently, {{{RdrHsSyn.checkTyVars}}} is used to either enforce that all type arguments are variables (second argument is `False`) or to simply check whether the type arguments are variables (second argument `True`).  If in enforcing mode, `checkTyVars` will raise an error if it encounters a non-variable (e.g., required for class declarations).  If in checking mode, it yields the value placed in the `tcdPats` field described above; i.e., returns `Nothing` instead of the type arguments if these arguments are all only variables.
    6482
    6583=== Representation of associated types ===