[Haskell-cafe] Re: type families and type signatures
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Tue Apr 8 00:48:28 EDT 2008
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
More information about the Haskell-Cafe
mailing list