Small displeasure with associated type synonyms
Dear all, I was doing a little experimentation with associated type synonyms and ran into a small but unforeseen annoyance. The following, contrived, example snippets illustrate my pain: First, let us declare some of the simplest classes exhibiting associated type synonyms that I can think of, class C a where type T a val :: T a together with a trivial instance for nullary products: instance C () where type T () = () val = () But then, let us try an instance for binary products: instance (C a, C b) => C (a, b) where type T (a, b) = (T a, T b) val = (val, val) I really thought this would work out nicely, but GHC (version 6.8.2) gracefully gives me Couldn't match expected type `T a2' against inferred type `T a' Expected type: T (a2, b) Inferred type: (T a, T a1) In the expression: (val, val) In the definition of `val': val = (val, val) Couldn't match expected type `T b' against inferred type `T a1' Expected type: T (a2, b) Inferred type: (T a, T a1) In the expression: (val, val) In the definition of `val': val = (val, val) while I think I deserve better than that. Can someone (Tom?) please explain (a) why the required unifications fail, (b) whether or not it is reasonable to expect the unifications to succeed, and (c) how I can overcome problems like these? Surely, I can have val take a dummy argument, but I am hoping for something a bit more elegant here. I tried lexically scoped type variables, but to no avail: instance forall a b. (C a, C b) => C (a, b) where type T (a, b) = (T a, T b) val = (val :: T a, val :: T b) gives me Couldn't match expected type `T a2' against inferred type `T a' In the expression: val :: T a In the expression: (val :: T a, val :: T b) In the definition of `val': val = (val :: T a, val :: T b) etc. Cheers, Stefan
I don't know if this is exactly what you were expecting as a dummy argument, but I solve this kind of issues like this: _L = undefined class C a where type TT a val :: a -> TT a instance C () where type TT () = () val _ = () instance (C a, C b) => C (a, b) where type TT (a,b) = (TT a, TT b) val _ = (val (_L :: a),val (_L :: b)) Why normal unification (val :: TT a) does not work I can't say why, but this kind of behavior is not solely for type families. Cheers, hugo
Stefan,
I tried lexically scoped type variables, but to no avail:
instance forall a b. (C a, C b) => C (a, b) where type T (a, b) = (T a, T b) val = (val :: T a, val :: T b)
The problem is ambiguity. The type checker can't determine which val function to use, i.e. which dictionary to pass to val. Assume: instance C Int where type T Int = Int val = 0 instance C Bool where type T Bool = Int val = 1 Now, if you want some val :: Int, which one do you get? The one of C Int of C Bool? Depending on the choice you may get a different result. We can't have that in a deterministic functional language. Hence the error. Adding a type signature doesn't change the matter. Providing an additional argument, as you propose, resolves the ambiguity. I hope this helps. Cheers, Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/
Tom Schrijvers wrote:
Stefan,
I tried lexically scoped type variables, but to no avail:
instance forall a b. (C a, C b) => C (a, b) where type T (a, b) = (T a, T b) val = (val :: T a, val :: T b)
The problem is ambiguity. The type checker can't determine which val function to use, i.e. which dictionary to pass to val. Assume:
instance C Int where type T Int = Int val = 0
instance C Bool where type T Bool = Int val = 1
Now, if you want some val :: Int, which one do you get? The one of C Int of C Bool? Depending on the choice you may get a different result. We can't have that in a deterministic functional language. Hence the error. Adding a type signature doesn't change the matter.
I don't see how your example explains this particular error. I agree Int cannot be generalized to (T Int) or (T Bool). I see Stefan's local type signature is not (val :: a) like your (val ::Int) but (val :: T a) which is a whole different beast. And (T a) is the type that ghc should assign here. The C (a,b) instance wants val :: T (a,b), The T (a,b) is declared as "(T a, T b)". The annotated val returns "(T a, T b)". One never needs the sort of Int to (T Int) generalization. So what is a better explanation or example to clarify why GHC cannot accept the original code? -- Chris
I don't see how your example explains this particular error. I agree Int cannot be generalized to (T Int) or (T Bool).
Generalized is not the right word here. In my example T Int, T Bool and Int are all equivalent.
I see Stefan's local type signature is not (val :: a) like your (val ::Int) but (val :: T a) which is a whole different beast.
Not all that different. As in my example the types T Int, T Bool and Int are equivalent, whether one writes val :: Int, val :: T Int or val :: T Bool. My point is that writing val :: T Int or val :: T Bool does not help determining whether one should pick the val implementation of instance C Int or C Bool.
And (T a) is the type that ghc should assign here.
As my example tries to point out, there is not one single syntactic form to denote a type. Consider the val of in the first component. Because of val's signature in the type class the type checker infers that the val expression has a type equivalent to T a2 for some a2. The type checker also expects a type equivalent to T a, either because of the type annotation or because of the left hand side. So the type checker must solve the equation T a ~ T a2 for some as yet to determine type a2 (a unification variable). This is precisely where the ambiguity comes in. The type constructor T is not injective. That means that the equation may hold for more than one value of a2 (e.g. for T Int ~ T a2, a2 could be Int or Bool). Hence, the type checker complains: Couldn't match expected type `T a2' against inferred type `T a'. Maybe you don't care what type is chosen, if multiple ones are possible. My example tried to show that this can effect the values computed by your program. So it does matter. For this particular example, it seems that the type checker does not have have more than alternative for a2 in scope. However, it is not aware of that fact. It uniformly applies the same general strategy for solving equations in all contexts. This is a trade-off in type system complexity vs. expressivity. There is an opportunity for exploring another point in the design space here. Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/
Okay, I get the difference. The "T a" annotation in "val :: T a)"and "val :: T a" does not help choose the "C a" dictionary. But the "val :: a-> T a" and "val (undefined :: a)" allows "a" to successfully choose the "C a" dictionary. val :: T a fixes "T a" but does not imply "C a". (undefined :: a) fixes "a" and does imply "C a". I now see how the functional dependency works here (which I should have tried to do in the first place -- I should have thought more and relied on the mailing list less). "class C a b | a -> b" is here "class C a where type T a = b". So only knowing "T a" or "b" does not allow "a" to be determined. -- Chris Tom Schrijvers wrote:
I don't see how your example explains this particular error. I agree Int cannot be generalized to (T Int) or (T Bool).
Generalized is not the right word here. In my example T Int, T Bool and Int are all equivalent.
I see Stefan's local type signature is not (val :: a) like your (val ::Int) but (val :: T a) which is a whole different beast.
Not all that different. As in my example the types T Int, T Bool and Int are equivalent, whether one writes val :: Int, val :: T Int or val :: T Bool. My point is that writing val :: T Int or val :: T Bool does not help determining whether one should pick the val implementation of instance C Int or C Bool.
And (T a) is the type that ghc should assign here.
As my example tries to point out, there is not one single syntactic form to denote a type.
Consider the val of in the first component. Because of val's signature in the type class the type checker infers that the val expression has a type equivalent to T a2 for some a2. The type checker also expects a type equivalent to T a, either because of the type annotation or because of the left hand side. So the type checker must solve the equation T a ~ T a2 for some as yet to determine type a2 (a unification variable). This is precisely where the ambiguity comes in. The type constructor T is not injective. That means that the equation may hold for more than one value of a2 (e.g. for T Int ~ T a2, a2 could be Int or Bool). Hence, the type checker complains:
Couldn't match expected type `T a2' against inferred type `T a'.
Maybe you don't care what type is chosen, if multiple ones are possible. My example tried to show that this can effect the values computed by your program. So it does matter.
For this particular example, it seems that the type checker does not have have more than alternative for a2 in scope. However, it is not aware of that fact. It uniformly applies the same general strategy for solving equations in all contexts. This is a trade-off in type system complexity vs. expressivity.
There is an opportunity for exploring another point in the design space here.
Tom
-- Tom Schrijvers
Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium
tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/
On Thu, Mar 6, 2008 at 3:57 PM, ChrisK
Okay, I get the difference.
The "T a" annotation in "val :: T a)"and "val :: T a" does not help choose the "C a" dictionary. But the "val :: a-> T a" and "val (undefined :: a)" allows "a" to successfully choose the "C a" dictionary.
val :: T a fixes "T a" but does not imply "C a". (undefined :: a) fixes "a" and does imply "C a". I now see how the functional dependency works here (which I should have tried to do in the first place -- I should have thought more and relied on the mailing list less).
"class C a b | a -> b" is here "class C a where type T a = b". So only knowing "T a" or "b" does not allow "a" to be determined.
Am I correct in thinking this would have worked if it were an
associated type instead of an associated type synonym?
ie,
class C a where
data T a
val :: T a
--
Dave Menendez
Am I correct in thinking this would have worked if it were an associated type instead of an associated type synonym?
ie,
class C a where data T a val :: T a
Yes, you are. Associate data type constructors (as well as ordinary algebraic data constructors) are injective. So we have: forall a b . T a = T b <=> a = b Cheers, Tom -- Tom Schrijvers Department of Computer Science K.U. Leuven Celestijnenlaan 200A B-3001 Heverlee Belgium tel: +32 16 327544 e-mail: tom.schrijvers@cs.kuleuven.be url: http://www.cs.kuleuven.be/~toms/
On Fri, Mar 07, 2008 at 08:07:57AM +0100, Tom Schrijvers wrote:
Am I correct in thinking this would have worked if it were an associated type instead of an associated type synonym?
ie,
class C a where data T a val :: T a
Yes, you are. Associate data type constructors (as well as ordinary algebraic data constructors) are injective. So we have:
Yay, that's what I though! (but was hesitant to suggest anything, since I've never actually used associated anything...) It's nice to hear that I do understand some of this stuff. :) -- David Roundy Department of Physics Oregon State University
Tom, Thanks for your quick answer.
The problem is ambiguity. The type checker can't determine which val function to use, i.e. which dictionary to pass to val.
I see. Still, maybe a type-error message in terms of good old "unresolved top-level overloading" would be a bit more useful here... ;-) Cheers, Stefan
Stefan Holdermans:
The problem is ambiguity. The type checker can't determine which val function to use, i.e. which dictionary to pass to val.
I see. Still, maybe a type-error message in terms of good old "unresolved top-level overloading" would be a bit more useful here... ;-)
I agree the error message is appalling. Could you put this as a bug in the bug tracker? Thanks, Manuel
participants (7)
-
ChrisK -
David Menendez -
David Roundy -
Hugo Pacheco -
Manuel M T Chakravarty -
Stefan Holdermans -
Tom Schrijvers