Changes between Version 50 and Version 51 of TypeFunctions
 Timestamp:
 Aug 26, 2006 8:42:02 PM (10 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctions
v50 v51 23 23 }}} 24 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.''' 25 * Kind signatures of type function shave the form25 * Kind signatures of type function have the form 26 26 {{{ 27 type family [iso]T a1 .. an :: <kind>27 type family T a1 .. an :: <kind> 28 28 }}} 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.)29 and introduce `n`ary type functions (with `n` >= 1), which may be of higherkind. Again, the type variables can have kind signatures. Equations for an `n`ary type function must specify exactly `n` arguments, which serve as indexes. 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 already have on ordinary type synonyms.) 31 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.