On Mon, May 21, 2007 at 10:36:00AM +0100, Simon Peyton-Jones wrote:

| The following doesn't seem to work. Is this a limitation of the current | implementation or will it never work? Are there any work arounds without | introducing extra type params into the data type E? | | > class G a b | a -> b where | > data E a :: * | > wrap :: b -> E a | > unwrap :: E a -> b | | > instance G a b where | > data E a = EC b -- this line - the b is not in scope. | > wrap = EC | > unwrap (EC b) = b | | I get "Not in scope: type variable `b'".

That's a bug. b should be in scope

Ahh, cool. I which case I wonder if this too is a bug? : data Nil = Nil data Cons :: * -> * -> * where Cons :: val -> tail -> Cons val tail class F c v t | c -> v t where data FD c t :: * instance F (Cons v t) v t where -- this blows up with "conflicting definitions for `t'" data FD (Cons v t) t = FDC v

However, your program is very suspicious! Associated data types *replace* functional dependencies, so you should not use both. Your probably want something like

class G a where data E a :: * wrap :: a -> E a unwrap :: E a -> a

I'm afraid not. I really need wrap to take a 'b' and unwrap to return a 'b'. Talking on #haskell to sjanssen last night, he came up with: class F a b where data F a :: * instance F a b where data F a = F b cast :: (F a b, F a c) => b -> c cast x = case F x of (F y) -> y as evidence as to why it's unsafe. But with the fundep, I would have thought it would have been safe. The associated type "way" would be to drop the b and then have data F a :: * -> * - just like in the papers. But I really need the b to be part of the class in order to match the b against other class constraints in other functions. In particular I need to be able to write something like: instance (G a b) => F a b where ... Somehow I doubt it, but is the following any less suspicious? class F a b where type BThing a :: * data FD a :: * wrap :: b -> FD a unwrap :: FD a -> b instance F a b where type BThing a = b data FD a = FDC (BThing a) wrap b = FDC b unwrap (FDC b) = b Incidentally, that "type BThing a = b" line also blows up with "Not in scope: type variable `b'". Thanks, Matthew -- Matthew Sackman http://www.wellquite.org/

On Mon, May 21, 2007 at 12:39:20PM +0100, Simon Peyton-Jones wrote:

| > | > instance G a b where | > | > data E a = EC b -- this line - the b is not in scope. | > | > wrap = EC | > | > unwrap (EC b) = b | > | | > | I get "Not in scope: type variable `b'". | > | > That's a bug. b should be in scope

I was wrong. It's not a bug. E is supposed to be a type *function*, so it can't mention anything on the RHS that is not bound on the LHS. We'll improve the documentation.

Ok, thanks for the clarification. One final question then, how could I rewrite the following in associated types: class OneStep a b | a -> b instance OneStep (Cons v t) t class TwoStep a b | a -> b instance (OneStep a b, OneStep b c) => TwoStep a c If the fundep and b is dropped then I get: class OneStep a data OS a :: * instance OneStep (Cons v t) data OS (Cons v t) = t class TwoStep a data TS a :: * instance (OneStep a, OneStep b) => TwoStep a This last one can't be right, as I can't express the fact that the OS in "OneStep a" provides the link with "OneStep b". So is there a way to achieve this sort of chaining with associated types? Sure, the fundep version requires undecidable instances, but I've been writing quite a lot of code lately that requires that! Many thanks, Matthew -- Matthew Sackman http://www.wellquite.org/

Andres Loeh wrote:

...

class OneStep a data OS a :: * instance OneStep (Cons v t) data OS (Cons v t) = t

class TwoStep a data TS a :: * instance (OneStep a, OneStep b) => TwoStep a

instance (OneStep a, OneStep (OS a)) => TwoStep a ?

Doesn't seem to work. Ok, my original was wrong as I had no constructor on the associated type. So below are 2 versions, one with fundeps, which works, one with associated type synonynms which doesn't work, which made me remember the warnings about how type synonynms aren't fully implemented yet, and so I wrote a third version with indexed types, but whilst I can make it work, wrapping up values in indexed types gets really really messy.

{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-}

module TestProb where

data Nil = Nil data Cons v t = Cons v t

class OneStep a b | a -> b instance OneStep (Cons v t) t

class TwoStep a b | a -> b instance (OneStep a b, OneStep b c) => TwoStep a c

class OneStep' a where type OS' a :: *

instance OneStep' (Cons v t) where type OS' (Cons v t) = t

class TwoStep' a where type TS' a :: *

instance (OneStep' a, OneStep' (OS' a)) => TwoStep' a where type TS' a = (OS' (OS' a))

foo :: (TwoStep a b) => a -> b -> Bool foo _ _ = True

foo' :: (TwoStep' a) => a -> TS' a -> Bool foo' _ _ = True

*TestProb> foo (Cons True (Cons 'b' (Cons "hello" Nil))) (Cons "boo" Nil) True *TestProb> :t foo (Cons True (Cons 'b' (Cons "hello" Nil))) foo (Cons True (Cons 'b' (Cons "hello" Nil))) :: Cons [Char] Nil -> Bool *TestProb> :t foo' (Cons True (Cons 'b' (Cons "hello" Nil))) <interactive>:1:0: No instance for (OneStep' (OS' (Cons Bool (Cons Char (Cons [Char] Nil))))) arising from a use of `foo'' at <interactive>:1:0-45 Possible fix: add an instance declaration for (OneStep' (OS' (Cons Bool (Cons Char (Cons [Char] Nil))))) Mmm. This is as a result of the instance (OneStep' a, OneStep' (OS' a)) constraint. Is it just me or does this look like the type synonynm isn't being applied? So how about adding:

instance (OneStep' a) => OneStep' (OS' a) where type OS' (OS' a) = a

*TestProb> :t foo' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) foo' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) :: (Fractional t) => TS' (Cons Bool (Cons Char (Cons t (Cons [Char] Nil)))) -> Bool Okay, but how do I inhabit that type? *TestProb> :t foo' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) (Cons 5.3 (Cons "hello" Nil)) <interactive>:1:59: Couldn't match expected type `TS' (Cons Bool (Cons Char (Cons t (Cons [Char] Nil))))' against inferred type `Cons t1 (Cons [Char] Nil)' In the second argument of `foo'', namely `(Cons 5.3 (Cons "hello" Nil))' So now, the third (and final!) version using indexed types:

class OneStep'' a where data OS'' a :: * mkOS'' :: a -> OS'' a

instance OneStep'' (Cons v t) where data OS'' (Cons v t) = OSC'' t mkOS'' (Cons v t) = OSC'' t

instance (OneStep'' a) => OneStep'' (OS'' a) where data OS'' (OS'' a) = OSC''w a

class TwoStep'' a where data TS'' a :: * mkTS'' :: a -> TS'' a

instance (OneStep'' a, OneStep'' (OS'' a)) => TwoStep'' a where data TS'' a = TSC'' (OS'' (OS'' a)) mkTS'' = TSC'' . mkOS'' . mkOS''

foo'' :: (TwoStep'' a) => a -> TS'' a -> Bool foo'' _ _ = True

This, sort of works: *TestProb> let ts = mkTS'' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) in foo'' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) ts True But of course, the wrapping into the indexed type demands the use of mkTS''. You can't even write: *TestProb> let ts = mkOS'' (Cons 'c' (Cons 5.3 (Cons "hello" Nil))) in foo'' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) ts <interactive>:1:119: Couldn't match expected type `TS'' (Cons Bool (Cons Char (Cons t (Cons [Char] Nil))))' against inferred type `OS'' (Cons Char (Cons t1 (Cons [Char] Nil)))' In the second argument of `foo''', namely `ts' In the expression: let ts = mkOS'' (Cons 'c' (Cons 5.3 (Cons "hello" Nil))) in foo'' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) ts In the definition of `it': it = let ts = mkOS'' (Cons 'c' (Cons 5.3 (Cons "hello" Nil))) in foo'' (Cons True (Cons 'c' (Cons 5.3 (Cons "hello" Nil)))) ts Further, it is *impossible* to define mkTS'' for the extra instance "instance (OneStep'' a) => OneStep'' (OS'' a) where" as to do so would demand unwrapping the supplied (OS'' a) which can't be done - if you try to add unwrop :: OS'' a -> a to the class OneStep'' then try to define it for the Cons instance - I've thrown away v so how are you going to get it back? undefined? Matthew -- Matthew Sackman http://www.wellquite.org/

Matthew Sackman wrote:

Andres Loeh wrote:

...

...

class OneStep a data OS a :: * instance OneStep (Cons v t) data OS (Cons v t) = t

class TwoStep a data TS a :: * instance (OneStep a, OneStep b) => TwoStep a instance (OneStep a, OneStep (OS a)) => TwoStep a ?

Doesn't seem to work. Ok, my original was wrong as I had no constructor on the associated type. So below are 2 versions, one with fundeps, which works, one with associated type synonynms which doesn't work, which made me remember the warnings about how type synonynms aren't fully implemented yet, and so I wrote a third version with indexed types, but whilst I can make it work, wrapping up values in indexed types gets really really messy.

Yes, it's messy with indexed data families as they force you to introduce all these new constructors and the corresponding wrapping and unwrapping code. As Tom wrote in another message in this thread, you really do want to use indexed synonyms families (aka associated type synonyms) here. They will do what you want. We are currently working on completing the implementation of synonym families.[1] Manuel [1] For those who wonder why this is taking so long, we are working on a system that is actually significantly more general than what we described in the ICFP05 paper. In particular, we want synonym families to play nice with GADTs.

Matthew Sackman wrote:

...

class G a where data E a :: * wrap :: a -> E a unwrap :: E a -> a

I'm afraid not. I really need wrap to take a 'b' and unwrap to return a 'b'. Talking on #haskell to sjanssen last night, he came up with:

How does class F a where data B a :: * data E a :: * wrap :: B a -> E a unwrap :: E a -> B a sound? 'B a' would represent the 'b' in your previous attempt, class F a b | a -> b where ... Bertram

Matthew Brecknell wrote:

Bertram Felgenhauer:

...

How does

class F a where data B a :: * data E a :: * wrap :: B a -> E a unwrap :: E a -> B a

sound? 'B a' would represent the 'b' in your previous attempt,

class F a b | a -> b where ...

I'm with Simon in thinking that this code is suspicious.

It wasn't my code Simon was replying to.

For any given call to "wrap" or "unwrap", how is the compiler supposed to determine which instance to use, given that "a" cannot be uniquely determined from the type of the function?

As far as my limited understanding goes this should work, because we are using an associated *data* type here. This means we can't have instances saying 'type B a = Int', we have to use either a newtype or a data declaration for that. As a side effect, the compiler can determine 'a' from 'B a'. This wouldn't be possible for associated type synonyms, but those aren't completely implemented yet anyway (again, as far as I know). Bertram