[Haskell-cafe] Re: Small displeasure with associated type synonyms

[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.

-- 
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 at cs.kuleuven.be
> url: http://www.cs.kuleuven.be/~toms/