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

[Matthew Sackman]

Andres Loeh <loeh at iai.uni-bonn.de> 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/