Re: [Haskell-cafe] accessing a type variable in instance declaration

2013-05-22 Thread Roman Cheplyaka
* TP paratribulati...@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.

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

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] accessing a type variable in instance declaration

2013-05-22 Thread TP
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


Re: [Haskell-cafe] accessing a type variable in instance declaration

2013-05-22 Thread Roman Cheplyaka
* TP paratribulati...@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)
 -
 
 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

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe