Changes between Version 36 and Version 37 of Records/NameSpacing


Ignore:
Timestamp:
Jan 18, 2012 4:22:02 AM (4 years ago)
Author:
GregWeber
Comment:

add SORF type resolution comment from SPJ's e-mail

Legend:

Unmodified
Added
Removed
Modified
  • Records/NameSpacing

    v36 v37  
    6161
    6262
    63 == Simple type resolution ==
     63== Type resolution ==
     64
     65Here'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
     75Consider type inference on k.  Initially we know nothing about the
     76type 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
     85Notice 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
     92This looks like a swamp.  In a simple Hindley-Milner typed language
     93you might get away with some informal heuristics, but Haskell is far
     94too complicated.
     95
     96Fortunately we know exactly what to do; it is described in some detail
     97in our paper "Modular type inference with local assumptions"
     98http://www.haskell.org/haskellwiki/Simonpj/Talk:OutsideIn
     99
     100The trick is to *defer* all these decisions by generating *type constraints*
     101and solving them later.  We express it like this:
     102
     103  G, r:t1  |-  r.f : t2,  (Has t1 "f" t2)
     104
     105This says that if r is in scope with type t1, then (r.f) has type t2,
     106plus the constraint (Has t1 "f" t2), which we read as saying
     107
     108  Type t1 must have a field "f" of type t2
     109
     110We gather up all the constraints and solve them.  In solving them
     111we may figure out t1 from some *other* constraint (to the left or
     112right, it's immaterial. That allow us to solve *this* constraint.
     113
     114So it's all quite simple, uniform, and beautiful.  It'll fit right
     115into GHC's type-constraint solver.
     116
     117But note what has happened: we have simply re-invented SORF.  So the
     118conclusion is this: the only sensible way to implement FDR is using SORF.
     119
     120=== Frege solution: simple type resolution ===
     121
     122This is overly-simplistic for Haskell (see above)
    64123
    65124Frege has a detailed explanation of the semantics of its record implementation, and the language is *very* similar to Haskell. After reading the Frege manual sections, one is still left wondering: how does Frege implement type resolution for its dot syntax. The answer is fairly simple: overloaded record fields are not allowed. So you can't write code that works against multiple record types. Please see the comparison with Overloading in [wiki:Records], which includes a discussion of the relative merits. Note that the DDC thesis takes the same approach.