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

[Miguel Mitrofanov]

> 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