Changes between Version 30 and Version 31 of Holes


Ignore:
Timestamp:
May 4, 2012 10:33:48 PM (2 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Holes

    v30 v31  
    132132Comments: 
    133133  * Reports the source location of each hole 
    134   * Does not allow two holes to have the same type 
    135   * Requires evaluation semantics for hole 
     134  * Does not allow two holes to have the same type  '''SLPJ: This sounds wierd.   Do you mean that `_ && _` would be illegal somehow?  Here the two holes both have type Bool''' 
     135  * Requires evaluation semantics for hole.   '''SLPJ: What does this mean?  Example?''' 
    136136 
    137137=== Named term variables === 
     
    149149  * Requires a fresh name to distinguish one hole from others 
    150150  * Requires evaluation semantics for hole 
     151 
     152'''SLPJ'''.  I'm really not sure what you mean by "must have the same type.  For example 
     153{{{ 
     154f xs = _?p : xs 
     155g ys = _?q : ys 
     156}}} 
     157If we typechecked each binding independently we'd get 
     158{{{ 
     159f :: forall a. [a] -> [a] 
     160g :: forlal b. [b] -> [b] 
     161}}} 
     162If we generalise `f` then NOTHING can have the same type as the hole.  But it would be very strange not to generalise `f` (and `g`).   
     163 
     164It seems much simpler to me either to have anonymous holes, or to let the user give them names, but to pay no attention to the name except to display them in error messages, so that user can say "oh, that hole" rather than having to look at the exact source location. '''End of SLPJ''' 
    151165 
    152166=== Term brackets (ranges) === 
     
    196210  1. If the program is well-typed (as above), then: 
    197211    * The types of all holes should be reported. 
    198     * Reporting the hole types should not cause type-checking (or compiling in general) to stop (in error). 
     212    * Reporting the hole types should not cause type-checking (or compiling in general) to stop (in error). '''SLPJ what does this mean? ''' A type error *never* causes type checking to stop.  Do you mean that a program with holes (but no other errors) should compile and run, falling over at runtime only if you evaluate a hole?  Please give an example.  '''End of SLPJ''' 
    199213  1. (optional) If the program is ill-typed, then: 
    200214    * The types of all holes should be reported. 
     
    206220We think holes can be extremely useful with ambiguous types. We prefer that a program, in which there is a hole with unsolved constraints on the type of the hole, still be considered well-typed, assuming the rest of the program is well-typed. In the above example, we would expect {{{show _?h}}} to have the type {{{String}}} with the reported hole type {{{_?h :: Show a => a}}}. 
    207221 
     222'''SLPJ do you want programs with these ambiguity errors to run too?  Or what?  Can you give a complete little example module, with the error messages you expect, whether you expect it to run, and if so what should happen?''' 
     223 
    208224==== Monomorphism restriction ==== 
    209225