[Haskell-cafe] Re: type families and type signatures

[Mark P Jones]

Hi Tom,

It seems we are thinking of different things.  I was referring to
the characterization of a type of the form P => t as being "ambiguous"
if there is a type variable in P that is not determined by the
variables in t; this condition is used in Haskell to establish
coherence (i.e., to show that a program has a well-defined semantics).

I don't know if you have defined/studied corresponding notions of
ambiguity/coherence in your framework.  Instead, I was referring to
what Manuel described as "the equivalent problem using FDs":

   class IdC a b | a -> b
   instance IdC Int Int

   bar :: IdC a b => b -> b
   bar = id

   bar' :: IdC a b => b -> b
   bar' = bar

In this program, both bar and bar' have ambiguous types (the
variable 'a' in each of the contexts is not uniquely determined
by the variable 'b' appearing on the right), and so *neither*
one of these definitions is valid.  This behavior differs from
what has been described for your approach, so perhaps Manuel's
example isn't really "equivalent" after all.

Technically, one could ignore the ambiguous type signature for
bar, because the *principal* type of bar (as opposed to the
*declared type*) is not ambiguous.  However, in practice, there
is little reason to allow the definition of a function with an
ambiguous type because such functions cannot be used in practice:
the ambiguity that is introduced in the type of bar will propagate
to any other function that calls it, either directly or indirectly.
For this reason, it makes sense to report the ambiguity at the
point where bar is defined, instead of deferring that error to
places where it is used, like the definition of bar'.  (The latter
is what I mean by "delayed" ambiguity checking.)

Hope that helps,
Mark


Tom Schrijvers wrote:
> On Mon, 7 Apr 2008, Mark P Jones wrote:
> 
>> The surprising thing about this example is the fact that
>> the definition of foo is accepted, and not the fact that
>> the definition of foo' is rejected.  At least in Manuel's
>> "equivalent" program using functional dependencies, both
>> functions have ambiguous types, and hence both would be
>> rejected.  It sounds like your implementation may be using
>> a relaxed approach to ambiguity checking that delays
>> ambiguity checking from the point of definition to the
>> point of use.  Although this is probably still sound, it
>> can lead to puzzling error diagnostics ...
> 
> On the algorithmic level I don't see a relaxed approach to ambiguity 
> checking.
> 
> If alpha is a unifiction variable, you get for the first body
> 
>     (Id a -> Id a)  ~ (alpha ~ alpha)
> 
> where there is no ambiguity: the unique solution (modulo equality 
> theory) is alpha := Id a.
> 
> For the second body you get
> 
>     (Id a -> Id a) ~ (Id alpha -> Id alhpa)
> 
> This equation reduces to Id a ~ Id alpha. Our algorithm stops here. 
> There is in general no single solution for alpha (*) in such an 
> equation, as opposed to the above case.
> 
> I hope this clarifies our algorithm.
> 
> Cheers,
> 
> Tom