[Haskell-cafe] Re: Small displeasure with associated type synonyms
haskell at list.mightyreason.com
Thu Mar 6 15:57:21 EST 2008
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
"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.
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
> Tom Schrijvers
> Department of Computer Science
> K.U. Leuven
> Celestijnenlaan 200A
> B-3001 Heverlee
> tel: +32 16 327544
> e-mail: tom.schrijvers at cs.kuleuven.be
> url: http://www.cs.kuleuven.be/~toms/
More information about the Haskell-Cafe