= 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