Re: [Haskell-cafe] Re: Small displeasure with associated type synonyms
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Small displeasure with associated type synonyms
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: [EMAIL PROTECTED] url: http://www.cs.kuleuven.be/~toms/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Small displeasure with associated type synonyms
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Small displeasure with associated type synonyms
On Thu, Mar 6, 2008 at 3:57 PM, ChrisK [EMAIL PROTECTED] wrote: 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 [EMAIL PROTECTED] http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Small displeasure with associated type synonyms
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: [EMAIL PROTECTED] url: http://www.cs.kuleuven.be/~toms/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
