[Haskell-cafe] Re: Small displeasure with associated type synonyms
Tom Schrijvers
Tom.Schrijvers at cs.kuleuven.be
Thu Mar 6 15:41:00 EST 2008
> 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 at cs.kuleuven.be
url: http://www.cs.kuleuven.be/~toms/
More information about the Haskell-Cafe
mailing list