63 | | == Simple type resolution == |
| 63 | == Type resolution == |
| 64 | |
| 65 | Here's a complex example: |
| 66 | |
| 67 | type family F a b |
| 68 | data instance F Int [a] = Mk { f :: Int } |
| 69 | |
| 70 | g :: F Int b -> () |
| 71 | h :: F a [Bool] -> () |
| 72 | |
| 73 | k x = (g x, x.f, h x) |
| 74 | |
| 75 | Consider type inference on k. Initially we know nothing about the |
| 76 | type of x. |
| 77 | * From the application (g x) we learn that x's type has |
| 78 | shape (F Int <something>). |
| 79 | * From the application (h x) we learn that x's type has |
| 80 | shape (F <something else> [Bool]) |
| 81 | * Hence x's type must be (F Int [Bool]) |
| 82 | * And hence, using the data family we can see which field |
| 83 | f is intended. |
| 84 | |
| 85 | Notice that |
| 86 | a) Neither left to right nor right to left would suffice |
| 87 | b) There is significant interaction with type/data families |
| 88 | (and I can give you more examples with classes and GADTs) |
| 89 | c) In passing we note that it is totally unclear how (Plan A) |
| 90 | would deal with data families |
| 91 | |
| 92 | This looks like a swamp. In a simple Hindley-Milner typed language |
| 93 | you might get away with some informal heuristics, but Haskell is far |
| 94 | too complicated. |
| 95 | |
| 96 | Fortunately we know exactly what to do; it is described in some detail |
| 97 | in our paper "Modular type inference with local assumptions" |
| 98 | http://www.haskell.org/haskellwiki/Simonpj/Talk:OutsideIn |
| 99 | |
| 100 | The trick is to *defer* all these decisions by generating *type constraints* |
| 101 | and solving them later. We express it like this: |
| 102 | |
| 103 | G, r:t1 |- r.f : t2, (Has t1 "f" t2) |
| 104 | |
| 105 | This says that if r is in scope with type t1, then (r.f) has type t2, |
| 106 | plus the constraint (Has t1 "f" t2), which we read as saying |
| 107 | |
| 108 | Type t1 must have a field "f" of type t2 |
| 109 | |
| 110 | We gather up all the constraints and solve them. In solving them |
| 111 | we may figure out t1 from some *other* constraint (to the left or |
| 112 | right, it's immaterial. That allow us to solve *this* constraint. |
| 113 | |
| 114 | So it's all quite simple, uniform, and beautiful. It'll fit right |
| 115 | into GHC's type-constraint solver. |
| 116 | |
| 117 | But note what has happened: we have simply re-invented SORF. So the |
| 118 | conclusion is this: the only sensible way to implement FDR is using SORF. |
| 119 | |
| 120 | === Frege solution: simple type resolution === |
| 121 | |
| 122 | This is overly-simplistic for Haskell (see above) |