Version 3 (modified by 7 years ago) (diff) | ,
---|

# Ambiguity

The question of *ambiguity* in Haskell is a tricky one. This wiki page is a summary of thoughts and definitions, in the hope of gaining clarity. I'm using a wiki because it's easy to edit, and many people can contribute, even though you can't typeset nice rules.

[Started Jan 2010.] **Please edit to improve.**

## Terminology

A type system is usually specified by

- A
**specification**, in the form of some**declarative typing rules**. These rules often involve "guessing types". Here is a typical example, for variables:(f : forall a1,..,an. C => tau) \in G theta = [t1/a1, ..., tn/an] -- Substitution, guessing ti Q |= theta( C ) ------------------------- (VAR) Q, G |- f :: theta(tau)

The preconditions say that f is in the environment G with a suitable polymorphic type. We "guess" types t1..tn, and use them to instantiate f's polymorphic type variables a1..an, via a substitution`theta`

. Under this substitution f's instantiated constraints`theta(C)`

must be*satisfiable*(using`|=`

) from the ambient constraints Q.

The point is that we "guess" the ai.

- An
**inference algorithm**, often also presented using similar-looking rules, but in a form that can be read as an algorithm with no "guessing". Typically- The "guessing" is replaced by generating fresh unification variables.
- The algorithm carries an ever-growing substitution that instantiates these unification variables.

We want the inference algorithm to be

**sound**(if it succeeds, then the program is well typed according to the specification) and**complete**(if the program is well typed according to the specification, the algorithm succeeds).

## Coherence

Suppose we have (I conflate classes `Read`

and `Show`

into one class `Text`

for brevity):

class Text a where read :: String -> a show :: a -> String x :: String x = show (read "3.7")

The trouble is that there is a constraint `(Text t)`

, where `t`

is a type variable that is otherwise unconstrained. Moreover, the type that we choose for `t`

affects the semantics of the program. For example, if we chose `t = Int`

then we might get `x = "3"`

, but if we choose `t = Float`

we might get `x = "3.7"`

. This is bad: we want our type system to be **coherent** in the sense that every well-typed program has but a single value.

In practice, the Haskell Report, and every Haskell implementation, rejects such a program saying something like

Cannot deduce (Text t) from ()

In *algorithmic* terms this is very natural: we indeed have a constraint `(Text t)`

for some unification variable `t`

, and no way to solve it, except by searching for possible instantiations of `t`

. So we simply refrain from trying such a search.

But in terms of the type system *specification* it is harder. We can simply guess `a=Int`

when we instantiate `read`

and `show`

and lo, the program is well typed. But we do not *want* this program to be well-typed.

**Problem 1**: How can we write the specification so as to reject programs such as that above.

## Digression: open and closed world

Suppose there was precisely one instance for `Text`

:

instance Text Char where ...

Then you might argue that there is only one way for the algorithm to succeed, namely by instantiating `read`

and `show`

at `Char`

.

It's pretty clear that this is a Bad Idea:

- In general it is hard to say whether there is a unique substitution that would make a collection of constraints satisfiable.
- If you add just one more instance, the program would become untypeable, which seems fragile.

To avoid this nasty corner we use the **open-world assumption**; that is, we assume that the programmer may add new instances at any time, and that doing so should not make a well-typed program become ill-typed. (We ignore overlapping instances for now.

## Early detection of errors

Suppose, with the above class `Text`

I write

f x = show (read x)

What type should we infer for `f`

? Well, a simple-minded inference algorithm works as follows for a let-definition `f=e`

: typecheck `e`

, collecting whatever constraints it generates. Now simply abstract over them.

In this example we'd get

f :: (Text a) => String -> String

And indeed this is a perfectly fine type for