Changes between Version 18 and Version 19 of KindSystem


Ignore:
Timestamp:
Oct 17, 2008 2:28:03 PM (5 years ago)
Author:
TristanAllwood
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • KindSystem

    v18 v19  
    9191 
    9292 
    93  
    94 == Interaction with normal functions == 
     93=== Interaction with normal functions === 
    9594 
    9695Functions cannot have arguments of a non * kind.  So the following would be disallowed: 
     
    116115In the above, {{{n}}} would be inferred to have kind {{{Nat}}} and {{{a}}} would have kind {{{*}}}. 
    117116 
    118 == Interaction with (G)ADTs == 
     117=== Interaction with (G)ADTs === 
    119118 
    120119(G)ADTs can already be annotated with a mixture of names with optional explicit kind signatures and just kind signatures. These kind signatures would now be able to refer to the newly declared, non-* kinds.  However the ultimate kind of a (G)ADT must still be {{{*}}}. i.e. 
     
    166165These are resolved by Haskell 98 with `(a :: *->*)` and `(b :: *)`.  We propose no change. 
    167166But see kind polymorphism below. 
     167 
     168 
     169=== Kind Namespace === 
     170 
     171Also see: TypeNaming 
     172 
     173Strictly, the new kinds that have been introduced using {{{data kind}}} syntax inhabit a new namespace.  Mostly it is unambiguous when you refer to a type and when you refer to a kind.  However there are some corner cases, particularly in module import/export lists. 
     174 
     175'''Option 1 : Collapse Type and Kind namespace''' 
     176 
     177''Pros:'' 
     178* Simple 
     179* Follows behaviour of type classes, type functions and data type functions. 
     180 
     181''Cons:'' 
     182* Inconsistent.  It would allow the user to create {{{True}}} and {{{False}}} as types, but not to be able to put them under kind {{{Bool}}}.  (You'd need to name your kind a {{{Bool'}}} or {{{Bool_k}}}) 
     183 
     184'''Option 2 : Fix ambiguities''' 
     185 
     186''Pros:'' 
     187* As more extensions are put into the language, it'll have to happen sooner or later 
     188 
     189''Cons:'' 
     190* Will involve creating a whole new namespace 
     191* Several corner cases 
     192 
     193 
    168194 
    169195 
     
    246272{{{ 
    247273data kind With (k :: ** -> **) = WithStar (k *) | WithNat (k Nat) 
    248  
    249 data Blah :: With MaybeK -> * where 
    250   B1 :: Int -> Blah (WithStar (JustK Int)) 
    251   B2 :: Int -> Blah (WithNat NothingK) -- type error! 
    252 }}} 
    253  
    254 Alt formulation of With using GADK syntax.  Does this help? 
     274}}} 
     275 
     276or 
     277 
     278Alternate formulation of With using GADK syntax. 
     279 
    255280{{{ 
    256281data kind With :: (** -> **) -> ** where 
     
    259284}}}  
    260285 
    261 == GADK Syntax == 
    262  
    263286 
    264287 
     
    319342Of course, if we are going to worry about {{{*}}} at different levels, the same could apply to other machinary that is applied at different levels (I'm looking at you (->)). 
    320343 
    321  
    322 == Kind Namespace == 
    323  
    324 With reference to: TypeNaming 
    325  
    326 Strictly, the new kinds that have been introduced using {{{data kind}}} syntax inhabit a new namespace.  Mostly it is unambiguous when you refer to a type and when you refer to a kind.  However there are some corner cases, particularly in module import/export lists. 
    327  
    328 === Option 1 : Collapse Type and Kind namespace === 
    329  
    330 '''Pros:''' 
    331 * Simple 
    332 * Follows behaviour of type classes, type functions and data type functions. 
    333  
    334 '''Cons:''' 
    335 * Inconsistent.  It would allow the user to create {{{True}}} and {{{False}}} as types, but not to be able to put them under kind {{{Bool}}}.  (You'd need to name your kind a {{{Bool'}}} or {{{Bool_k}}}) 
    336  
    337 === Option 2 : Fix ambiguities === 
    338  
    339 '''Pros:''' 
    340 * As more extensions are put into the language, it'll have to happen sooner or later 
    341  
    342 '''Cons:''' 
    343 * Will involve creating a whole new namespace 
    344 * Several corner cases 
    345344 
    346345