Changes between Version 12 and Version 13 of KindSystem


Ignore:
Timestamp:
Oct 17, 2008 8:25:30 AM (7 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • KindSystem

    v12 v13  
    131131In the above example, there is the question of what kind we should assign to {{{a}}} in {{{Ok}}}.  Currently it would be inferred to be {{{*}}}.  That inference engine would need to be improved to include inference of other kinds.
    132132
    133 GADT constructors must only accept arguments of kind {{{*}}} (as per the restrictions on (->) described below), but may also collect constraints for the kind inference system.
    134 
    135 === Ambiguous cases ===
    136 
    137 TODO: are there real ambiguous cases?  _Assuming_ data types have their kind signatures inferred before functions are type checked and must be monomorphic in their kinds, I don't see how there could be unless a variable is totally unconstrained (i.e. not mentioned)
    138 
    139 {{{
    140 foo :: forall a . Int
    141 }}}
    142 
    143 However this is accepted (6.8.3), although ghci drops the 'a'.  Even if it was used in a scoped setting (TODO example of where that makes sense without a type class grounding it), the moment it is used it'll get a kind constraint.  Do PolymorphicKinds break this assumption?
     133GADT constructors must only accept arguments of kind {{{*}}} (as per the restrictions on (->) described above), but may also collect constraints for the kind inference system.
     134
     135=== Kind inference ===
     136
     137Kind inference figures out the kind of each type variable.   There are often ambiguous cases:
     138{{{
     139  data T a b = MkT (a b)
     140}}}
     141These are resolved by Haskell 98 with `(a :: *->*)` and `(b :: *)`.  We propose no change.
     142But see kind polymorphism below.
    144143
    145144