Changes between Version 46 and Version 47 of TypeFunctions
 Timestamp:
 Aug 15, 2006 9:42:17 PM (8 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctions
v46 v47 18 18 19 19 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]. 20 * Kind signatures of indexed data type s have the form20 * Kind signatures of indexed data type families have the form 21 21 {{{ 22 data T a1 .. an :: <kind>22 data family T a1 .. an :: <kind> 23 23 }}} 24 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.24 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.''' 25 25 * Kind signatures of type functions have the form 26 26 {{{ 27 type [iso] T a1 .. an :: <kind>27 type family [iso] T a1 .. an :: <kind> 28 28 }}} 29 and introduce an `n`ary type functions, which may be of higherkind, 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.)30 * 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.'''31 * Instances of indexed data types/newtypes and equations of type functions have the same form as vanilladata types/newtypes and type synonyms, respectively, but can have nonvariable type indexes in index positions. Type indexes can include applications of indexed data types and newtypes, but no type functions.29 and introduce `n`ary type functions, which may be of higherkind, 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.''') 30 * 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.) 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 nonvariable type indexes in index positions. Type indexes can include applications of indexed data types and newtypes, but no type functions. 32 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 * 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.)34 33 * All type indexes of an associated indexed type or type function need to be class parameters. 35 34 * 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.)