Type families versus functional dependencies question

newer
Santana on my evil ways

older
not for me, guv!

Alexey Rodriguez

3 Jul 2008 3 Jul '08

9:20 a.m.

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

Attachments:

attachment.html (text/html — 1.7 KB)

Show replies by date

Claus Reinke

3 Jul 3 Jul

1:31 p.m.

New subject: Type families versus functional dependencies question

...

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

Alexey Rodriguez

2:56 p.m.

New subject: Type families versus functional dependencies question

On Thu, Jul 3, 2008 at 7:31 PM, 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

Claus Reinke

4:14 p.m.

New subject: Type families versus functional dependenciesquestion

...

...
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

Alexey Rodriguez

4 Jul 4 Jul

4:39 a.m.

New subject: Type families versus functional dependenciesquestion

On Thu, Jul 3, 2008 at 10:14 PM, 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

Manuel M T Chakravarty

3 Jul 3 Jul

11:03 p.m.

New subject: Type families versus functional dependencies question

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

Alexey Rodriguez

4 Jul 4 Jul

4:42 a.m.

New subject: Type families versus functional dependencies question

On Fri, Jul 4, 2008 at 5:03 AM, Manuel M T Chakravarty 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

Manuel M T Chakravarty

7 Jul 7 Jul

2:21 a.m.

New subject: Type families versus functional dependencies question

Alexey Rodriguez:

...

On Fri, Jul 4, 2008 at 5:03 AM, Manuel M T Chakravarty
...
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

6164

Age (days ago)

6168

Last active (days ago)

List overview

Download

7 comments

3 participants

participants (3)

Alexey Rodriguez
Claus Reinke
Manuel M T Chakravarty

Type families versus functional dependencies question

tags

participants (3)