Changes between Version 18 and Version 19 of KindSystem


Ignore:
Timestamp:
Oct 17, 2008 2:28:03 PM (7 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