Re: [Haskell-cafe] Scope of type variables in associated types

21 May 2007

      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/