Changes between Version 2 and Version 3 of TypeFunctions/Ambiguity
 Timestamp:
 Jan 20, 2010 9:05:57 PM (10 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctions/Ambiguity
v2 v3 19 19 We "guess" types t1..tn, and use them to instantiate f's polymorphic type variables 20 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.21 `theta(C)` must be ''satisfiable'' (using `=`) from the ambient constraints Q. 22 22 23 23 The point is that we "guess" the ai. … … 25 25 * An '''inference algorithm''', often also presented using similarlooking rules, but in a form that can be read as an algorithm with no "guessing". Typically 26 26 * The "guessing" is replaced by generating fresh unification variables. 27 * The algorithm carries an evergrowing substitution that instantiates these unification variables. 28 29 We 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 27 33 28 34 == Coherence == … … 45 51 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. 46 52 47 But in terms of the type system ''specification'' it is harder. Usually a53 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 welltyped. 48 54 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 59 Suppose there was precisely one instance for `Text`: 60 {{{ 61 instance Text Char where ... 62 }}} 63 Then you might argue that there is only one way for the algorithm to succeed, namely by instantiating `read` and `show` at `Char`. 64 65 It'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 69 To avoid this nasty corner we use the '''openworld assumption'''; that is, we assume that the programmer may add new instances at any time, and that doing so should not make a welltyped program become illtyped. (We ignore overlapping instances for now. 70 71 72 == Early detection of errors == 73 74 Suppose, with the above class `Text` I write 75 {{{ 76 f x = show (read x) 77 }}} 78 What type should we infer for `f`? Well, a simpleminded inference algorithm works as follows for a letdefinition `f=e`: typecheck `e`, collecting whatever constraints it generates. Now simply abstract over them. 79 80 In this example we'd get 81 {{{ 82 f :: (Text a) => String > String 83 }}} 84 And indeed this is a perfectly fine type for