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

21 May 2007

      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/