Changes between Version 2 and Version 3 of TypeFunctions/Ambiguity


Ignore:
Timestamp:
Jan 20, 2010 9:05:57 PM (6 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctions/Ambiguity

    v2 v3  
    1919  We "guess" types t1..tn, and use them to instantiate f's polymorphic type variables
    2020  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.
     21  `theta(C)` must be ''satisfiable'' (using `|=`) from the ambient constraints Q.
    2222
    2323 The point is that we "guess" the ai.
     
    2525 * 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
    2626   * The "guessing" is replaced by generating fresh unification variables.
     27   * The algorithm carries an ever-growing substitution that instantiates these unification variables.
     28
     29We want the inference algorithm to be
     30 * '''sound''' (if it succeeds, then the program is well typed according to the specification) and
     31 * '''complete''' (if the program is well typed according to the specification, the algorithm succeeds).
     32
    2733
    2834== Coherence ==
     
    4551In ''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.
    4652
    47 But in terms of the type system ''specification'' it is harder.  Usually a
     53But 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.
    4854
    49 '''Problem 1''': how can w
     55'''Problem 1''': How can we write the specification so as to reject programs such as that above.
     56
     57== Digression: open and closed world ==
     58
     59Suppose there was precisely one instance for `Text`:
     60{{{
     61instance Text Char where ...
     62}}}
     63Then you might argue that there is only one way for the algorithm to succeed, namely by instantiating `read` and `show` at `Char`.
     64
     65It's pretty clear that this is a Bad Idea:
     66 * In general it is hard to say whether there is a unique substitution that would make a collection of constraints satisfiable.
     67 * If you add just one more instance, the program would become untypeable, which seems fragile.
     68
     69To 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.
     70
     71
     72== Early detection of errors ==
     73
     74Suppose, with the above class `Text` I write
     75{{{
     76f x = show (read x)
     77}}}
     78What 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. 
     79
     80In this example we'd get
     81{{{
     82f :: (Text a) => String -> String
     83}}}
     84And indeed this is a perfectly fine type for