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