[Haskell-cafe] Lightweight type-level dependent programming in Haskell

Miguel Mitrofanov miguelimo38 at yandex.ru
Thu Jun 11 00:45:02 EDT 2009


> I recently discovered an interesting way of closing typeclasses while
> playing with type-level peano naturals:

>> class Nat n where
>>   caseNat :: forall r. n -> (n ~ Z => r) -> (forall p. (n ~ S p,  
>> Nat p) => p -> r) -> r

I usually use this one:

class Nat n where
   caseNat :: p Z -> (forall m. Nat m => p (S m)) -> p n
instance Nat Z where
   caseNat pz _ = pz
instance Nat n => Nat (S n) where
   caseNat _ psm = psm


More information about the Haskell-Cafe mailing list