Roman Cheplyaka wrote: > You are confusing type and value variables. > > c2num order > > means apply the function 'c2num' to the value variable 'order', which is > not defined. > > To get from a type to a value you can use a type class 'Sing' (for > 'singleton') > > class Sing a where > sing :: a > > instance Sing Zero where > sing = Zero > > instance Sing a => Sing (Succ a) where > sing = Succ sing > > After adding the appropriate constraint to the instance, you can write > > show $ c2num $ (sing :: order)
Ok, thanks, I understand. Now, I'm stuck to compile this code (independent from my previous post, but related to it): --------------- {-# LANGUAGE DataKinds #-} {-# LANGUAGE KindSignatures #-} data Nat = Zero | Succ Nat type One = Succ Zero type Two = Succ One -- class Cardinal c where -- line 1 class Cardinal (c::Nat) where -- line 2 c2num :: c -> Integer cpred :: (Succ c) -> c cpred = undefined instance Cardinal Zero where c2num _ = 0 instance (Cardinal c) => Cardinal (Succ c) where c2num x = 1 + c2num (cpred x) main = do print $ show $ c2num (undefined::Succ (Succ Zero)) print $ show $ c2num (undefined::Two) ----------------- With line 2, I get: test_nat.hs:11:14: Kind mis-match Expected kind `OpenKind', but `c' has kind `Nat' In the type `c -> Integer' In the class declaration for `Cardinal' With line 1 instead, I get: Kind mis-match The first argument of `Succ' should have kind `Nat', but `c' has kind `*' In the type `(Succ c) -> c' In the class declaration for `Cardinal' So, in the first case, c has a too restricted kind, and in the second one, it has a too broad kind in the definition of cpred. I have tried several things without any success. How to compile that code? Thanks, TP _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe