Changes between Version 14 and Version 15 of KindSystem


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

--

Legend:

Unmodified
Added
Removed
Modified
  • KindSystem

    v14 v15  
    242242 
    243243{{{ 
    244 data kind With (k :: * -> *) = WithStar (k *) | WithNat (k Nat) 
    245  
    246 data Blah :: * -> With Maybe -> * where 
    247   B1 :: Int -> Blah (WithStar (Just Int)) 
    248   B2 :: Int -> Blah (WithNat Nothing) -- type error! 
     244data kind With (k :: ** -> **) = WithStar (k *) | WithNat (k Nat) 
     245 
     246data Blah :: With MaybeK -> * where 
     247  B1 :: Int -> Blah (WithStar (JustK Int)) 
     248  B2 :: Int -> Blah (WithNat NothingK) -- type error! 
    249249}}} 
    250250 
    251251Alt formulation of With using GADK syntax.  Does this help? 
    252252{{{ 
    253 data kind With :: forall (k :: * -> *) . k -> * where 
    254   WithStar :: (k *) -> With k 
    255   WithNat :: (k Nat) -> With k 
     253data kind With :: (** -> **) -> ** where 
     254  WithStar :: forall (k :: ** -> **). (k *) -> With k 
     255  WithNat  :: forall (k :: ** -> **). (k Nat) -> With k 
    256256}}}  
    257257