Changes between Version 33 and Version 34 of Holes


Ignore:
Timestamp:
May 10, 2012 3:27:32 PM (2 years ago)
Author:
spl
Comment:

Revise description of variations in response to SLPJ

Legend:

Unmodified
Added
Removed
Modified
  • Holes

    v33 v34  
    8282The clear problem with deliberate type errors is that the program does not type-check. We cannot use this technique on multiple locations at one time. We also only get type errors and not other information. 
    8383 
    84 With '''deliberate errors and deferred type errors''', we do get a program that type-checks. This is actually a reasonable solution; however, it still has two problems: 
     84With ''deliberate errors and deferred type errors'', we do get a program that type-checks. This is actually a reasonable solution; however, it still has two problems: 
    8585  * Deferring type errors is indiscriminate: you defer both the deliberate and unintended type errors. 
    8686  * It does not provide useful information other than type errors. 
     
    116116Since we are changing the syntax and semantics of Haskell, we feel that this should become a language extension (rather than another kind of compiler flag). For now, we proposed the name {{{Holes}}} (as in {{{-XHoles}}}), though this could change after discussion. 
    117117 
    118 == Variations == 
    119  
    120 We view a hole as a piece of syntax that is inserted in code as a placeholder until the programmer fills that location with something else. Numerous views on the syntax and semantics of holes have been discussed. Here are a few: 
    121  
    122 === Term wildcards === 
    123  
    124 This approach mirrors Agda goals. The actual syntax is debatable, but we think {{{_}}} is quite nice, since it appears to be illegal as an expression. 
    125  
     118== Syntactic placement of holes == 
     119 
     120We view a hole as a piece of syntax that is inserted in code as a placeholder until the programmer fills that location with something else. That placeholder can not only allow the program to be compiled but also allow the compiler to report information that is significant to the location of the placeholder. 
     121 
     122Numerous views on the syntax and semantics of holes have been suggested. We first classify the various options by the syntactic categories of types or expressions. Then, we classify them within each category and describe the various trade-offs. 
     123 
     124=== Types === 
     125 
     126Here is an example: 
    126127Example: 
    127128{{{ 
    128 test :: [Bool] 
    129 test = _ : (_ ++ []) 
    130 }}} 
    131  
    132 Comments: 
    133   * Reports the source location of each hole 
    134   * Does not allow the programmer to specify that two holes have the same type  '''SLPJ: This sounds wierd.   Do you mean that `_ && _` would be illegal somehow?  Here the two holes both have type Bool''' -- '''SPL: No, it's just careless phrasing. Corrected.''' 
    135   * Requires evaluation semantics for hole.   '''SLPJ: What does this mean?  Example?''' 
    136  
    137 === Named term variables === 
    138  
    139 This approach mirrors implicit parameters. Each hole is given a name. Within a module (or even a program/library?), each every hole with the same name has the same type. Again, the actual syntax is debatable, but for now, we use {{{_?x}}} for a hole with the (possibly shared) name {{{x}}}. 
    140  
    141 Example: 
    142 {{{ 
    143 test :: [Bool] 
    144 test = _?x : (_?y ++ []) 
    145 }}} 
    146  
    147 Comments: 
    148   * Reports the name and source location of each hole 
    149   * Requires a fresh name to distinguish one hole from others 
    150   * Requires evaluation semantics for hole 
    151  
    152 '''SLPJ question'''.  I'm really not sure what you mean by "must have the same type.  For example 
    153 {{{ 
    154 f xs = _?p : xs 
    155 g ys = _?q : ys 
    156 }}} 
    157 If we typechecked each binding independently we'd get 
    158 {{{ 
    159 f :: forall a. [a] -> [a] 
    160 g :: forlal b. [b] -> [b] 
    161 }}} 
    162 If 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  
    164 It 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 question''' 
    165  
    166 === Term brackets (ranges) === 
    167  
    168 Instead of an actual term, we can use a special form of bracketing to indicate a hole. As above, syntax is debatable, but for now, we use {{{{_}}} and {{{_}}}} for the brackets of the hole. 
    169  
    170 Example: 
    171 {{{ 
    172 test :: [Bool] 
    173 test = {_ undefined _} : ({_ undefined ++ [] _}) 
    174 }}} 
    175  
    176 Comments: 
    177   * Reports the source location of each hole 
    178   * Requires opening and closing brackets 
    179   * Allows wildcard term to be treated as syntactic sugar, e.g. {{{_}}} desugars into {{{{_ undefined _}}}}  
    180   * Does not require evaluation semantics for the brackets 
    181  
    182 Note that we can extend this with names for each pair of brackets. 
    183  
    184 === Type wildcards === 
    185  
    186 Instead of term holes, we can use a special type to indicate an unknown type. The type hole would be reported. We use {{{_}}} for the syntax here. 
    187  
    188 Example: 
    189 {{{ 
    190 test :: [_] 
    191 test = (undefined::_) : (undefined ++ [] ::_) 
    192 }}} 
    193  
    194 Comments: 
    195   * Reports the source location of each hole 
    196   * Does not allow two holes to be equal 
    197   * Does not require evaluation semantics for the holes 
    198   * Can be used in type annotations for both variables and large expressions (as in the term brackets) 
    199   * Allows partial types to be specified 
    200   * (?)May not support reporting local bindings 
    201  
    202 Note that we can extend this with names for each type hole. 
     129f :: Bool -> _ () 
     130f x = if x then return () else (undefined :: _) >>= guard 
     131}}} 
     132We show a hole (with the wildcard syntax `_`) in several locations: a type signature and a type annotation. In the signature, a hole fills in for a type constructor, and in the annotation, the hole fills in for the type of `undefined`. Upon typing, we expect to learn the types that are inferred for these holes. For example, we might get the following report: 
     133{{{ 
     134Found a hole in the signature: test :: Bool -> _ () 
     135Source location: ... 
     136Inferred type: MonadPlus m => m :: * -> * 
     137 
     138Found a hole in the annotation: undefined :: _ 
     139Source location: ... 
     140Inferred type: MonadPlus m => m Bool :: * 
     141}}} 
     142Note that all type variables should be the same for all reports, so all types above refer to the same `m`.  
     143 
     144=== Expressions === 
     145 
     146Here is an example: 
     147{{{ 
     148f x = do 
     149  y <- _ x 
     150  y `mplus` _ 
     151}}} 
     152We show a monadic expression with holes (`_`) in the function position of an application and as an argument to `mplus`. Upon typing, we expect to learn the types that would be inferred for the missing expressions in these holes. For example, we might get the following report: 
     153{{{ 
     154Found a hole in the expression: _ x 
     155Source location: ... 
     156Inferred type: MonadPlus m => a -> m b 
     157 
     158Found a hole in the expression: y `mplus` _ 
     159Source location: ... 
     160Inferred type: MonadPlus m => m b 
     161}}} 
     162Again, note that the type variables are universally quantified over all reports, not each report separately. 
     163 
     164=== Comparison === 
     165 
     166If we had to choose, should holes be in types or expressions? Let's look at the advantages and disadvantages. 
     167 
     168''Kinds.'' With types, we can put a hole in a type constructor position (see example above), so we have more flexibility in the restrictions we can place on a particular type: e.g. `_ ()` or `Monad m => m _`. With expressions, we are limited to the kinds of types that expressions can have (e.g. `*` and not `* -> *`). 
     169 
     170''Information reporting.'' We would like to extract additional information from a hole other than just the type. The primary consideration is the set of available bindings and their types. With type (annotation) holes, it is not clear if that is possible. With expression holes, it seems intuitive. 
     171 
     172''Evaluation.'' With expressions, we must consider how holes are evaluated. We would expect `_` would be treated the same as `undefined`, so this may cause unexpected program death when evaluating a hole. With types, we are not concerned with this. Type holes are never evaluated, so they cannot break a well-typed program. 
     173 
     174''Expression size.'' Type annotation holes can be used to find the type of arbitrarily large expressions, relying only on the normal expression bracketing. Expression holes (as presented so far) only replace a whole expression with a placeholder. Another approach would be needed to support expression hole bracketing. 
     175 
     176''Verbosity.'' Type annotation holes, e.g. `undefined :: _`, are possibly too verbose for simple uses, while expression holes are straightforward. 
     177 
     178== Extensions to basic holes == 
     179 
     180In the previous section, we described holes as simple "wildcard" syntax that can be put in either a type or an expression. There are a few basic extensions or variations to this idea. 
     181 
     182=== Names === 
     183 
     184We might consider the wildcard syntax `_` to be an "anonymous" or "unnamed" hole. We could also support a named hole, e.g. `_?x`. Named holes have two advantages over wildcards. 
     185 
     186''Better reporting.'' The reports can now explicitly mention the hole (in addition to the source location). For example: 
     187{{{ 
     188Found the hole _?x in the expression: _?x + 4 
     189... 
     190}}} 
     191 
     192''Multiple uses.'' When a named hole is used in multiple source locations, intuitively, that named hole should have the type resulting from the unification of the hole types at each location. For example: 
     193{{{ 
     194f y = print (y + _?x) 
     195g z = mappend z _?x 
     196}}} 
     197This might produce the following report: 
     198{{{ 
     199Found the hole _?x in the expressions: 
     200  print (y + _?x) at source location ... 
     201  mappend z _?x at source location ... 
     202Inferred type: Show a, Num a, Monoid a => a 
     203}}} 
     204 
     205It seems intuitive how named holes work in expressions. How would they work in types? 
     206 
     207=== Brackets (ranges) === 
     208 
     209As we mentioned in #Comparison, the expression wildcard does not allow finding out the type of an existing expression. A special pair of brackets could be used to do this. 
     210 
     211Assuming {{{{_}}} and {{{_}}}} are the brackets for a hole, we have this example: 
     212{{{ 
     213f y = print {_ y + mempty _} 
     214}}} 
     215And the report might be: 
     216{{{ 
     217Found hole brackets around the expression: y + mempty 
     218Source location: ... 
     219Inferred type: Num a, Monoid a => a 
     220}}} 
     221 
     222We could combine the naming and bracketing extensions into one. 
    203223 
    204224== User's view ==