Type families versus functional dependencies question

[Alexey Rodriguez Yakushev-2]

Hi guys,

We are having trouble with the following program that uses type families:

> class Blah f a where
>   blah :: a -> T f f a
 
> class A f where
>   type T f :: (* -> *) -> * -> *

the following function does not type:

> wrapper :: forall a f . Blah f a => a -> T f f a
> wrapper x = blah x

GHC gives the error:

    Couldn't match expected type `T f1 f1 a'
           against inferred type `T f f a'
    In the expression: blah x
    In the definition of `wrapper': wrapper x = blah x

Maybe it is a problem with ambiguous types, namely "f" appears only in applications of "T". But that is not the case, there is a "naked" f appearing as the argument of "T f". But perhaps the type checker does not want to unify those two f's precisely because they are the arguments of "T f".

I have tried to encode the above program using FunDeps, because this procedure helps me understand type errors. But in this case I get no type error!

> class A' (f :: * -> *) (g :: (* -> *) -> * -> *) | f -> g where

> class Blah' f a where
>   blah' :: A' f g => a -> g f a

> wrapper' :: forall a f g . (Blah' f a,A' f g) => a -> g f a
> wrapper' x = blah' x

So my question is whether my encoding is correct. And if it is, why isn't the type families version working?

Thanks!

Alexey


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

[Claus Reinke]

> GHC gives the error:
>
>    Couldn't match expected type `T f1 f1 a'
>           against inferred type `T f f a'
>    In the expression: blah x
>    In the definition of `wrapper': wrapper x = blah x

actually, GHC gives me "could not deduce Blah f a from Blah f1 a"
first. It seems that desugaring type function notation into an additional
constraint helps, so there's something odd going on:

    class Blah f a where blah :: a -> T f f a
    class A f where type T f :: (* -> *) -> * -> *

    wrapper :: forall a f tf . (Blah f a,T f~tf) => a -> tf f a
    wrapper x = blah x

You're relying on that second f to determine the first, which
then allows T f to determine tf f a. Looks a bit like cyclic
programming at the type level?-) Whereas the desugared
view is that we may not know the type constructor tf yet,
but whatever it is, its first parameter fixes f.

Yet another take on it: tf, the result of T f f a, needs to be
determined by the context, rather than the type function,
and type functions are traditionally bad at reasoning
backwards. The extra indirection separates determining
f from applying T f.

I think I'd prefer if that naive desugaring of type function
always worked, without such differences.

Worth a ticket?
Claus


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

[Alexey Rodriguez Yakushev-2]

On Thu, Jul 3, 2008 at 7:31 PM, Claus Reinke <claus.reinke@...> wrote:

GHC gives the error:

  Couldn't match expected type `T f1 f1 a'
         against inferred type `T f f a'
  In the expression: blah x
  In the definition of `wrapper': wrapper x = blah x

actually, GHC gives me "could not deduce Blah f a from Blah f1 a"
first. It seems that desugaring type function notation into an additional
constraint helps, so there's something odd going on:

Silly me, I didn't paste the whole type error. Yes, GHC gives both. I should add that I tested this under GHC 6.8.2. But this is known not to work with a (one/two months old) GHC head.

Cheers,

Alexey
 

  class Blah f a where blah :: a -> T f f a
  class A f where type T f :: (* -> *) -> * -> *

  wrapper :: forall a f tf . (Blah f a,T f~tf) => a -> tf f a
  wrapper x = blah x

You're relying on that second f to determine the first, which
then allows T f to determine tf f a. Looks a bit like cyclic
programming at the type level?-) Whereas the desugared
view is that we may not know the type constructor tf yet,
but whatever it is, its first parameter fixes f.

Yet another take on it: tf, the result of T f f a, needs to be
determined by the context, rather than the type function,
and type functions are traditionally bad at reasoning backwards. The extra indirection separates determining
f from applying T f.

I think I'd prefer if that naive desugaring of type function
always worked, without such differences.

Worth a ticket?
Claus

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

[Claus Reinke]

>> actually, GHC gives me "could not deduce Blah f a from Blah f1 a"
>> first. It seems that desugaring type function notation into an additional
>> constraint helps, so there's something odd going on:
>
> Silly me, I didn't paste the whole type error. Yes, GHC gives both. I should
> add that I tested this under GHC 6.8.2. But this is known not to work with a
> (one/two months old) GHC head.

yes, I tested with 6.9.20080514. And just in case my phrasing
was unclear: desugaring the type function application makes the
error go away, so you have a workaround.

It is just confusing that this example shows that the "desugaring"
is not a desugaring, in the current implementation..

Claus


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

[Manuel M T Chakravarty]

Alexey Rodriguez:

> We are having trouble with the following program that uses type  
> families:
>
> > class Blah f a where
> >   blah :: a -> T f f a
>
> > class A f where
> >   type T f :: (* -> *) -> * -> *
>
> the following function does not type:
>
> > wrapper :: forall a f . Blah f a => a -> T f f a
> > wrapper x = blah x
>
> GHC gives the error:
>
>     Couldn't match expected type `T f1 f1 a'
>            against inferred type `T f f a'
>     In the expression: blah x
>     In the definition of `wrapper': wrapper x = blah x
>
> Maybe it is a problem with ambiguous types, namely "f" appears only  
> in applications of "T". But that is not the case, there is a "naked"  
> f appearing as the argument of "T f". But perhaps the type checker  
> does not want to unify those two f's precisely because they are the  
> arguments of "T f".

The problem is that blah's type is ambiguous, as f does only occur as  
an argument to the type family.  If you'd define

   class Blah f a where
     blah :: a -> f -> T f f a

(and change the rest of the program accordingly) then all will be  
fine.  See this thread for a more in-depth discussion of the problem:

   http://www.haskell.org/pipermail/haskell-cafe/2008-April/041385.html

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

[Alexey Rodriguez Yakushev-2]

On Thu, Jul 3, 2008 at 10:14 PM, Claus Reinke <claus.reinke@...> wrote:

actually, GHC gives me "could not deduce Blah f a from Blah f1 a"
first. It seems that desugaring type function notation into an additional
constraint helps, so there's something odd going on:

Silly me, I didn't paste the whole type error. Yes, GHC gives both. I should
add that I tested this under GHC 6.8.2. But this is known not to work with a
(one/two months old) GHC head.

yes, I tested with 6.9.20080514. And just in case my phrasing
was unclear: desugaring the type function application makes the
error go away, so you have a workaround.

Thanks for highlighting this. Indeed I missed it, and it makes my example work.

Cheers,

Alexey
 

It is just confusing that this example shows that the "desugaring"
is not a desugaring, in the current implementation..

Claus

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

[Alexey Rodriguez Yakushev-2]

On Fri, Jul 4, 2008 at 5:03 AM, Manuel M T Chakravarty <chak@...> wrote:

The problem is that blah's type is ambiguous, as f does only occur as an argument to the type family.  If you'd define

 class Blah f a where

   blah :: a -> f -> T f f a

(and change the rest of the program accordingly) then all will be fine.  See this thread for a more in-depth discussion of the problem:

 http://www.haskell.org/pipermail/haskell-cafe/2008-April/041385.html

Yes, I was afraid that this was the case. However, the question remains on whether my functional dependencies encoding is correct. A correct encoding would help me understand this typing problem a bit more. Especially, now that Claus showed that adding an equality constraint makes this program work!

Cheers,

Alexey

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

[Manuel M T Chakravarty]

Alexey Rodriguez:

>
>
> On Fri, Jul 4, 2008 at 5:03 AM, Manuel M T Chakravarty <chak@...
> > wrote:
> The problem is that blah's type is ambiguous, as f does only occur  
> as an argument to the type family.  If you'd define
>
>
>  class Blah f a where
>    blah :: a -> f -> T f f a
>
> (and change the rest of the program accordingly) then all will be  
> fine.  See this thread for a more in-depth discussion of the problem:
>
>  http://www.haskell.org/pipermail/haskell-cafe/2008-April/041385.html
>
> Yes, I was afraid that this was the case. However, the question  
> remains on whether my functional dependencies encoding is correct. A  
> correct encoding would help me understand this typing problem a bit  
> more. Especially, now that Claus showed that adding an equality  
> constraint makes this program work!

For this particular program, you could argue that the signature is not  
ambiguous as T is unary; hence, in (T f f a) only the (T f) is really  
a type family application and so the second occurrence of 'f' should  
make the signature unambiguous.  This is the reason why Claus'  
encoding works and why your FD translation works.  I will have a look  
at whether I can improve the implementation in GHC to be smarter about  
handling such higher kinded TFs.

Thanks for the example program!

Manuel

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