Hi Mark,
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.)
You are of course spot on, but this is a difference in how GHC handles
functional dependencies compared to Hugs. Hugs does reject bar as
being ambiguous, but GHC does not! In other words, it also uses
"delayed" ambiguity checking for the FD version, and so raises an
error only when seeing bar'. The implementation of type families just
mirrors GHC's behaviour for FDs. (This is why I presented the FD
example, but I should have mentioned that the equivalence is
restricted to GHC.)
The rational for the decision to use delayed ambiguity checking in GHC
is that it is, in general, not possible to spot and report all
ambiguous signatures and *only* those. So, there are three possible
choices:
(1) Reject all signatures that *may* be ambiguous (and hence reject
some perfectly good programs).
(2) Reject all signatures that are *guaranteed* to be ambiguous
(and accept some programs with functions that can never be applied).
(3) Don't check for ambiguity (or "delayed" ambiguity checking).
As you wrote, all three choices are perfectly safe - we will never
accept a type-incorrect program, but they vary in terms of the range
of accepted programs and quality of error messages.
Please correct me if I am wrong, but as I understand the situation,
Hugs uses Choice (1) and GHC uses Choice (3). As an example, consider
this contrived program:
class F a b | a -> b where
f1 :: a -> b
f2 :: b -> a
instance F Int Int where
f1 = id
f2 = id
class G x a b where
g :: x -> a -> b
instance F a b => G Bool a b where
g c v = f1 v
instance F b a => G Int a b where
g c v = f2 v
foo1 :: (G Int a b) => a -> a
foo1 v = v
foo2 :: (G Bool a b) => a -> a
foo2 v = v
bar = foo2 (42::Int)
Here foo1 is actually ambiguous, but foo2 is fine due to the FD in the
instance context of the (G Bool a b) instance. GHC accepts this
program (not checking for ambiguity) and allows you to evaluate bar.
In contrast, Hugs rejects both the signature of foo1 and of foo2,
arguably being overly restrictive with foo2.
Cheers,
Manuel
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
