Changes between Version 1 and Version 2 of TypeFunctions/Ambiguity


Ignore:
Timestamp:
Jan 20, 2010 8:48:06 PM (4 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