# Changes between Version 1 and Version 2 of TypeFunctions/Ambiguity

Ignore:
Timestamp:
Jan 20, 2010 8:48:06 PM (8 years ago)
Comment:

--

### Legend:

Unmodified
 v1 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. Please edit to improve. [Started Jan 2010.]  '''Please edit to improve.''' [Started Jan 2010.] == 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 deducible (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. == Coherence == 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. But in terms of the type system ''specification'' it is harder.  Usually a '''Problem 1''': how can w