Re: [Haskell-cafe] Type families versus functional dependencies question
Alexey Rodriguez: On Fri, Jul 4, 2008 at 5:03 AM, Manuel M T Chakravarty [EMAIL PROTECTED] 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type families versus functional dependencies question
On Fri, Jul 4, 2008 at 5:03 AM, Manuel M T Chakravarty [EMAIL PROTECTED] 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Type families versus functional dependencies question
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type families versus functional dependencies question
On Thu, Jul 3, 2008 at 7:31 PM, Claus Reinke [EMAIL PROTECTED] 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
