TP | 22 May 16:18 2013
Picon

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_Types)

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-extensions.html#scoped-type-variables).

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))
------------

(Continue reading)

Roman Cheplyaka | 22 May 16:40 2013

Re: accessing a type variable in instance declaration

* TP <paratribulations <at> free.fr> [2013-05-22 16:18:55+0200]
> 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_Types)
> 
> 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-extensions.html#scoped-type-variables).

You are confusing type and value variables.

  c2num order

means apply the function 'c2num' to the value variable 'order', which is
not defined.

(Continue reading)

TP | 22 May 18:45 2013
Picon

Re: accessing a type variable in instance declaration

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 #-}
(Continue reading)

Roman Cheplyaka | 22 May 19:40 2013

Re: accessing a type variable in instance declaration

* TP <paratribulations <at> free.fr> [2013-05-22 18:45:06+0200]
> 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)
> -----------------
> 
(Continue reading)


Gmane