Changes between Version 14 and Version 15 of KindSystem


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