Changes between Version 38 and Version 39 of Holes


Ignore:
Timestamp:
May 17, 2012 8:00:52 AM (2 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Holes

    v38 v39  
    141141Note that all type variables should be the same for all reports, so all types above refer to the same `m`.  
    142142 
     143'''SLPJ''' see comments below about class constraints on the holes. '''End of SLPJ''' 
     144 
     145 
    143146=== Expressions === 
    144147 
     
    159162Inferred type: MonadPlus m => m b 
    160163}}} 
    161 Again, note that the type variables are universally quantified over all reports, not each report separately. 
     164Again, note that the type variables are universally quantified over all reports, not each report separately.  '''SLPJ''' I have no idea what this sentence means.  '''End of SLPJ'''. 
     165 
     166'''SLPJ'''.  I am very uncomfortable with saying anything like 
     167{{{ 
     168Inferred type: MonadPlus m => m b 
     169}}} 
     170for two reasons: 
     171 * First, that absolutely is not the inferred type of the hold.  Imagine that I added a binding 
     172{{{ 
     173boo :: MonadPlus m => m b 
     174}}} 
     175 and replaced the last line of the example with 
     176{{{ 
     177  y `mplus` boo 
     178}}} 
     179 Would it type check?  Absolutely not!  Adding type constraints on the types of the holes seems wierd and and impossible to justify. 
     180 
     181 * Second, the need for `MonadPlus` is nothing to do with the holes. It's to do with the call to `mplus` and the do-notation. It seems wrong to implicate the hole. 
     182'''End of SLPJ''' 
     183 
    162184 
    163185=== Comparison === 
     
    253275If we instead allow the program to type-check, we can find out what type the hole should have ({{{_?h :: Show a => a}}} in this case) and more information. 
    254276 
     277'''SLPJ''' I would rather put it like this. If I wrote 
     278{{{ 
     279f :: String 
     280f = show undefined 
     281}}} 
     282then I '''want''' an ambiguity error.  And that is supposed to be what holes are equivalent to (see above).  But, you may argue, there is no point in reporting a cascade of errors that follow from the absence of information about a hole.  It's just distracting.  So here's an idea: 
     283 * With `-XHoles` we autmatically behave like `-fdefer-type-errors` for any unsolved type constraint that shares a free unification variable with a hole. 
     284The idea is that if we have a hole of type `a`, then an unsolved `(Show a)` or `(C [a])` or `F a ~ Int` or anything mentioning `a` are automatically deferred and perhaps not even reported as warnings (unsure on this point). If you run the program you might trip over one of them, of course. 
     285'''End of SLPJ''' 
     286 
    255287A hole with an ambiguous type should probably be treated as a hole runtime error and not a deferred type error (see [#Runtimeerror Runtime error] for an example); however, not all holes are the immediate cause of ambiguity type errors. For example, consider: 
    256288{{{