[Haskell-cafe] Re: type families and type signatures
Martin Sulzmann
martin.sulzmann at gmail.com
Tue Apr 8 04:51:31 EDT 2008
The point is that Mark proposes a *pessimistic* ambiguity check whereas
Tom (as well as GHC) favors
an *optimistic* ambiguity check.
By pessimistic I mean that we immediately reject a program/type if
there's a potential
unambiguity. For example,
class Foo a b
forall a b. Foo a b => b -> b
is potentially ambiguous assuming we encounter
instance Foo Int Char
instance Foo Bool Char
But such instances might never arise. See Tom's example below which applies
an optimistic ambiguity check. In the extreme case, the optimistic
ambiguity check
only checks for ambiguity when calling the ground top-level function main.
At this point (latest), we must provide (unambiguously) evidence
for type classes and type equations.
In summary:
- The pessimistic ambiguity check is more in line with Haskell's open
world view
(of type classes and type families/functions being open/extensible).
Anything can
happen in the future (we might add an new type instances). So let's
assume the
worst and immediately report any potential ambiguity.
- The optimistic ambiguity check takes into account the set of available
instance.
Depending on the set of instances there may not be any ambiguity
after all.
Both strategies are backed up by theoretical results. See the Coherence
Theorems
in Mark's thesis and "A Theory of Overloading" (I'm happy to provide
more concrete
pointers if necessary).
Martin
Tom Schrijvers wrote:
>> 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).
>
> [...]
>
>> 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.)
>
> Thanks for explaining the ambiguity issue, Mark. I wasn't thinking
> about that. We have thought about ambiguity. See Section 7.3 in our paper
>
> http://www.cs.kuleuven.be/~toms/Research/papers/draft_type_functions_2008.pdf
>
>
> Note that neither Definition 3 nor Definition 4 demands that all
> unification variables are substituted with ground types during type
> checking. So we do allow for a form of ambiguity: when any type is
> valid (this has no impact on the semantics). Consider the initial program
>
> type family F a
>
> foo :: F a -> F a
> foo = id
>
> You propose to reject function Foo because it cannot be used
> unambiguously. We propose to accept foo, because the program could be
> extended with
>
> type instance F x = Int
>
> and, for instance, this would be valid:
>
> foo2 :: F Char -> F Bool
> foo2 = foo
>
> If you look at the level of the equality constraints:
>
> (F Char -> F Bool) ~ (F alpha -> F alpha)
>
> we normalise first wrt the instance F x = Int, and get
>
> (Int -> Int) ~ (Int -> Int)
>
> which is trivially true. In this process we do not substitute alpha.
> So alpha is ambiguous, but any solution will do and not have an impact
> on program execution. GHC already did this before type functions, for
> this kind of ambiguity, it substitutes alpha for an arbitrary type.
> That's not unreasonable, is it?
>
> Cheers,
>
> 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/
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
More information about the Haskell-Cafe
mailing list