wiki:TypeFunctionsSyntax

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

--

Type Functions: Syntax and Representation

Syntax of kind signatures and definitions of indexed types

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

Representation of indexed types

Kind signatures

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.

Signatures for indexed data and newtypes are represented as a special case of TyData, namely when TyData has a kind signature, but no constructors.

We recognise both forms of kind signatures by the predicate HsDecls.isKindSigDecl.

Definitions of indexed types

We 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:

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

In both cases (and as before we had type functions), tcdVars collects all variables we need to quantify over.

Parsing and AST construction

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

Representation of associated types

We add type declarations to class declarations and instance declarations by a new field, of type [LTyClDecl], to both TyClDecl.ClassDecl (known by the field name tcdATs) and TyClDecl.InstDecl. For classes, this new field contains values constructed from TyData, TyFunction, and TySynonym, whereas for instances, we only have TyData and TySynonym. This is due to (a) TyData representing both signatures and definitions of associated data types (whereas the two are split into TyFunction and TySynonym for associated synonyms) and (b) associated synonyms having default definitions, which associated data types do not possess.