Changes between Version 52 and Version 53 of TypeFunctions


Ignore:
Timestamp:
Aug 26, 2006 9:35:57 PM (9 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctions

    v52 v53  
    2020 * Kind signatures of indexed data type families have the form
    2121 {{{
    22 data family T a1 .. an :: <kind>
     22data family T a1 .. an [:: <kind>]
    2323}}}
    24  and introduce a type family whose kind is determined by the kinds of the `ai` (which can have kind annotations) and the explicit signature `<kind>`.  Newtypes families have the same form, except for the initial keyword.  '''We can now also admit the omission of the kind with * being the default.'''
     24 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 can now also admit the omission of the kind with * being the default.'''
    2525 * Kind signatures of type function have the form
    2626 {{{
     
    2929 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.
    3030 * 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.)
    31  * 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.
    32  * 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.
    33  * All type indexes of an associated indexed type or type function need to be class parameters.
     31 * 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.
     32 * 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.
     33 * 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.
     34 * 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.
     35 * ??
    3436 * 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.)
    3537