Changes between Version 9 and Version 10 of KindSystem


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

--

Legend:

Unmodified
Added
Removed
Modified
  • KindSystem

    v9 v10  
    8787}}}
    8888
     89
     90
     91== Interaction with normal functions ==
     92
     93Functions cannot have arguments of a non * kind.  So the following would be disallowed:
     94
     95{{{
     96bad :: Zero -> Bool   -- Zero has kind Nat
     97}}}
     98
     99This follows straighforwardly from the kind of (->) in GHC already: {{{?? -> ? -> *}}}, see IntermediateTypes
     100
     101Type variables may however be inferred to have non-* kinds.  E.g.
     102
     103{{{
     104#!text/x-haskell
     105data NatRep :: Nat -> * where
     106  ZeroRep :: NatRep Zero
     107  SuccRep :: (NatRep n) -> NatRep (Succ n)
     108
     109tReplicate :: forall n a . NatRep n -> a -> List a n
     110...
     111}}}
     112
     113In the above, {{{n}}} would be inferred to have kind {{{Nat}}} and {{{a}}} would have kind {{{*}}}.
     114
    89115== Interaction with GADTs ==
    90116
     
    105131GADT constructors must only accept arguments of kind {{{*}}} (as per the restrictions on (->) described below), but may also collect constraints for the kind inference system.
    106132
    107 == Interaction with normal functions ==
    108 
    109 Functions cannot have arguments of a non * kind.  So the following would be disallowed:
    110 
    111 {{{
    112 bad :: Zero -> Bool   -- Zero has kind Nat
    113 }}}
    114 
    115 This follows straighforwardly from the kind of (->) in GHC already: {{{?? -> ? -> *}}}, see IntermediateTypes
    116 
    117 Type variables may however be inferred to have non-* kinds.  E.g.
    118 
    119 {{{
    120 #!text/x-haskell
    121 data NatRep :: Nat -> * where
    122   ZeroRep :: NatRep Zero
    123   SuccRep :: (NatRep n) -> NatRep (Succ n)
    124 
    125 tReplicate :: forall n a . NatRep n -> a -> List a n
    126 ...
    127 }}}
    128 
    129 In the above, {{{n}}} would be inferred to have kind {{{Nat}}} and {{{a}}} would have kind {{{*}}}.
    130 
    131133=== Ambiguous cases ===
    132134
     
    149151instance LessThanOrEqual Zero Zero
    150152instance LessThanOrEqual n m => LessThanOrEqual n (Succ m)
    151 
    152 class Bad x y            -- \
    153 instance Bad True Int    --  |
    154 instance Bad Int String  --   > Together this would require argument x :: forall kind k . k,
    155                          --  |  see PolymorphicKinds
    156                          -- /
     153}}}
     154This example is ill-kinded though:
     155{{{
     156class Bad x           -- Defaults to x::*
     157instance Bad Int   -- OK
     158instance Bad Zero  -- BAD: ill-kinded
    157159}}}
    158160