Changes between Version 1 and Version 2 of TypeFunctions/Ambiguity


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

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctions/Ambiguity

    v1 v2  
    33The 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. 
    44
    5 Please edit to improve. 
     5[Started Jan 2010.]  '''Please edit to improve.'''
    66
    7 [Started Jan 2010.]
     7== Terminology ==
     8
     9A type system is usually specified by
     10 * A '''specification''', in the form of some '''declarative typing rules'''.  These rules often involve "guessing types".  Here is a typical example, for variables:
     11{{{
     12  (f : forall a1,..,an. C => tau) \in G
     13  theta = [t1/a1, ..., tn/an]        -- Substitution, guessing ti
     14  Q |= theta( C )
     15  ------------------------- (VAR)
     16  Q, G |- f :: theta(tau)
     17}}}
     18  The preconditions say that f is in the environment G with a suitable polymorphic type.
     19  We "guess" types t1..tn, and use them to instantiate f's polymorphic type variables
     20  a1..an, via a substitution `theta`.  Under this substitution f's instantiated constraints
     21  `theta(C)` must be deducible (using `|=`) from the ambient constraints Q.
     22
     23 The point is that we "guess" the ai.
     24
     25 * 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
     26   * The "guessing" is replaced by generating fresh unification variables.
    827
    928== Coherence ==
     
    2645In ''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.
    2746
    28 But in terms of the type system ''specification'' it is harder.
     47But in terms of the type system ''specification'' it is harder.  Usually a
    2948
    3049'''Problem 1''': how can w