Changes between Version 9 and Version 10 of KindSystem


Ignore:
Timestamp:
Oct 17, 2008 8:08:17 AM (6 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