accessing a type variable in instance declaration
Hi all, I wonder if there is some means to get a type variable value in the body of a class instance definition. It seems it is not possible (a workaround has already been given on this list), but I would like a confirmation. For example, imagine that I have a Tensor type constructor, that takes a type-level integer (representing the Tensor order) to make a concrete type: --------- instance Show (Tensor order) where show TensorVar str = show "tensor " ++ str ++ " of order " ++ (show (c2num order)) ---------- where c2num transforms a type-level integer to an integer, through typeclasses (see http://www.haskell.org/haskellwiki/The_Monad.Reader/Issue5/Number_Param_Type...) I obtain a compilation error: order is not known in the body of the instance. Putting ScopedTypeVariable as extension does not change anything (http://www.haskell.org/ghc/docs/7.0-latest/html/users_guide/other-type-exten...). I have tried also using forall, without more success: ------------ instance forall order. Show (Tensor order) where show TensorVar str = show ”tensor ” ++ str ++ ” of order ” ++ (show (c2num order)) ------------ Thanks in advance, TP
* TP
Hi all,
I wonder if there is some means to get a type variable value in the body of a class instance definition. It seems it is not possible (a workaround has already been given on this list), but I would like a confirmation. For example, imagine that I have a Tensor type constructor, that takes a type-level integer (representing the Tensor order) to make a concrete type:
--------- instance Show (Tensor order) where show TensorVar str = show "tensor " ++ str ++ " of order " ++ (show (c2num order)) ----------
where c2num transforms a type-level integer to an integer, through typeclasses (see http://www.haskell.org/haskellwiki/The_Monad.Reader/Issue5/Number_Param_Type...)
I obtain a compilation error: order is not known in the body of the instance. Putting ScopedTypeVariable as extension does not change anything (http://www.haskell.org/ghc/docs/7.0-latest/html/users_guide/other-type-exten...).
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) Roman
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
* TP
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?
You seem to assume that Succ Zero will have type 'Succ 'Zero (i.e. the promoted type), but it's not the case — it still has type Nat, as always. On the other hand, the type 'Succ 'Zero has kind 'Nat and doesn't have any inhabitants — only types of kind * do. So, how to fix this depends on what you want. For example, you can change c2num to accept Proxy c instead of c. Or you can establish the connection between Succ Zero and 'Succ 'Zero — again, using a (slightly modified) Sing class. In the latter case, take a look at the 'singletons' package — it can do a lot of work for you. Roman
participants (2)
-
Roman Cheplyaka -
TP