Changes between Version 36 and Version 37 of Records/NameSpacing


Ignore:
Timestamp:
Jan 18, 2012 4:22:02 AM (3 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.