Changes between Version 20 and Version 21 of Holes


Ignore:
Timestamp:
Apr 27, 2012 3:34:36 PM (2 years ago)
Author:
spl
Comment:

Proposal section revised

Legend:

Unmodified
Added
Removed
Modified
  • Holes

    v20 v21  
    107107}}} 
    108108 
    109 = A proposed concrete design for Haskell = 
    110  
    111 Here is a specification of the proposed user-level view of the design. 
    112  
    113 A hole in a term is written `_?thing`.  Example: 
    114 {{{ 
    115 test : List Bool 
    116 test = Cons _?x (Cons _?x Nil) 
    117 }}} 
    118 If {{{-XHoles}}} is set, we want the following: 
    119   1. The program should be type-checked as if every hole {{{_?h}}} is replaced by {{{undefined}}}, except: 
    120     * If type-checking would fail due to unsolved constraints that could be solved by giving a type to a hole. 
     109= Proposal = 
     110 
     111In this section, we discuss the proposed extension to GHC. 
     112 
     113== Language extension == 
     114 
     115Since 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. 
     116 
     117== Variations == 
     118 
     119We 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: 
     120 
     121=== Term wildcards === 
     122 
     123This approach mirrors Agda goals. The actual syntax is debatable, but we think {{{_}}} is quite nice, since it appears to be illegal as an expression. 
     124 
     125Example: 
     126{{{ 
     127test :: [Bool] 
     128test = _ : (_ ++ []) 
     129}}} 
     130 
     131Comments: 
     132  * Reports the source location of each hole 
     133  * Does not allow two holes to have the same type 
     134  * Requires evaluation semantics for hole 
     135 
     136=== Named term variables === 
     137 
     138This 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}}}. 
     139 
     140Example: 
     141{{{ 
     142test :: [Bool] 
     143test = _?x : (_?y ++ []) 
     144}}} 
     145 
     146Comments: 
     147  * Reports the name and source location of each hole 
     148  * Requires a fresh name to distinguish one hole from others 
     149  * Requires evaluation semantics for hole 
     150 
     151=== Term brackets (ranges) === 
     152 
     153Instead 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. 
     154 
     155Example: 
     156{{{ 
     157test :: [Bool] 
     158test = {_ undefined _} : ({_ undefined ++ [] _}) 
     159}}} 
     160 
     161Comments: 
     162  * Reports the source location of each hole 
     163  * Requires opening and closing brackets 
     164  * Allows wildcard term to be treated as syntactic sugar, e.g. {{{_}}} desugars into {{{{_ undefined _}}}}  
     165  * Does not require evaluation semantics for the brackets 
     166 
     167Note that we can extend this with names for each pair of brackets. 
     168 
     169=== Type wildcards === 
     170 
     171Instead 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. 
     172 
     173Example: 
     174{{{ 
     175test :: [_] 
     176test = (undefined::_) : (undefined ++ [] ::_) 
     177}}} 
     178 
     179Comments: 
     180  * Reports the source location of each hole 
     181  * Does not allow two holes to be equal 
     182  * Does not require evaluation semantics for the holes 
     183  * Can be used in type annotations for both variables and large expressions (as in the term brackets) 
     184  * Allows partial types to be specified 
     185  * (?)May not support reporting local bindings 
     186 
     187Note that we can extend this with names for each type hole. 
     188 
     189== User's view == 
     190 
     191For this specification, we use the named term variables variant (though it may also apply to other variants). 
     192 
     193When using holes (i.e. {{{-XHoles}}} is set), we expect the following: 
     194  1. The program should type-check as if every hole {{{_?h}}} is replaced with {{{undefined}}}. This is one exception: see [#Ambiguoustypes Ambiguous types] below. 
    121195  1. If the program is well-typed (as above), then: 
    122196    * The types of all holes should be reported. 
     
    125199    * The types of all holes should be reported. 
    126200 
    127 The above should hold true with and without the monomorphism restriction. In particular, if an {{{undefined}}} somewhere in a program type-checked with the monomorphism restriction would cause type-checking to fail, then a hole in that same position should also cause type-checking to fail. 
    128  
    129 The type of a hole should be the resolved type with minimum constraints. That is, the type of a hole should only have constraints that have not be solved but are either inferred from the context (e.g. {{{show _?h}}}) or given in a type annotation/signature (e.g. {{{_?h :: Show a => a}}}. 
    130 --------------------------------- 
    131 '''Stuff below here might be out of date; please edit''' 
    132  
    133 = How this could be implemented in GHC = 
    134  
    135 These two approaches are not ideal, they either don't give enough information, or they hinder using the code. 
    136  
    137 === Agda-style === 
    138 The simplest way would be to implement them in the same way as Agda: add a new syntax (we shall use two underscores as an example here, {{{__}}}) to denote a hole, and after typechecking, show the user a list of all the types of all the holes in their source files. In what cases "after typechecking" we do this is still subject of discussion. We expect at the very least to show it after (re)loading a module into GHCi or typechecking an expression in GHCi directly ({{{:t}}}). 
    139  
    140 Example: 
    141 {{{ 
    142 test :: [Bool] 
    143 test = __ : (__ ++ []) 
    144 }}} 
    145 Theoretical output: 
    146 {{{ 
    147 > :l test.hs 
    148 [1 of 1] Compiling Main             ( test.hs, interpreted ) 
    149 Found a hole at test.hs:2:6-7: Bool 
    150 Found a hole at test.hs:2:12-13: [Bool] 
    151 >  
    152 }}} 
    153  
    154 === Named holes === 
    155 Implicit parameters have some good features too: they can be named, and so used in multiple places. In the Agda-style, this would require let-binding a hole, which is a lot of effort for something that should be a temporary placeholder. So one idea is to allow giving holes a name, just like implicit parameters. 
    156  
    157 For example: 
    158  
    159 {{{ 
    160 test :: [Bool] 
    161 test = _a : (_b ++ []) 
    162  
    163 test2 = _c ++ _b 
    164 }}} 
    165 Theoretical output: 
    166 {{{ 
    167 > :l test.hs 
    168 [1 of 1] Compiling Main             ( test.hs, interpreted ) 
    169 Found a hole _a: Bool 
    170 Found a hole _b: [Bool] 
    171 Found a hole _c: [Bool] 
    172 >  
    173 }}} 
    174  
    175 These could either be made shared within all functions in module, or not shared between functions at all (so not the confusing situation with implicit parameters, which are only shared when required). 
    176  
    177 === Not holes, ranges === 
    178 Holes can be useful for finding the type of something that still needs to be written, but a more general way of looking at it is this: it is currently quite easy to typecheck a complete expression, for example with {{{:t}}}, in GHCi. However, finding the type of a part of an expression within a module is hard. In a large, complicated function it could be useful to ask the compiler for the types of certain subexpressions. {{{:t}}} does not help here, as the function's parameters and where/let/lambda-bound terms are not in scope. It would be useful if it were possible to annotate code to ask the compiler to give you the type found for the annotated expression. 
    179  
    180 Simple example (let {{{{_ _}}}} denote a request for the type here): 
    181 {{{ 
    182 test :: [Bool] 
    183 test = {_ undefined _} : ({_ undefined ++ [] _}) 
    184 }}} 
    185  
    186 Could result in: 
    187 {{{ 
    188 > :l test.hs 
    189 [1 of 1] Compiling Main             ( test.hs, interpreted ) 
    190 Found type of undefined (test.hs:2:11-19): Bool 
    191 Found type of undefined ++ [] (test.hs:2:30-38): [Bool] 
    192 }}} 
    193  
    194 The same effect of holes can then be achieved by using {{{ {_ undefined _} }}}. To return to the conciseness of holes, {{{__}}} could be syntactic sugar for {{{{_ undefined _}}}}. (Note that defining {{{__ = {_ undefined _}}}} in Haskell would not do this. The type would be {{{forall a. a}}}.) 
    195  
    196 == Not ranges, but types == 
    197  
    198 A variation of the previous proposal that is a bit more powerful and less syntactically intrusive is to implement this in the type language. So giving an expression (or even a pattern) a type of {{{__}}} would leave this type arbitrary and make GHC print the type. This subsumes the previous proposals, e.g.  
    199 {{{ 
    200 test :: [Bool] 
    201 test = (undefined::__) : (undefined ++ [] ::__) 
    202 }}} 
    203 and again a {{{__}}} on the term level could be syntactic sugar for {{{(undefined::__)}}}. 
    204  
    205 The benefit from this variant is that {{{__}}} could occur as parts of types as well, e.g.  
    206 {{{ 
    207 test :: [__] 
    208 test = (undefined::__) : (undefined ++ [True] ::__) 
    209 }}} 
     201=== Ambiguous types === 
     202 
     203If type-checking would fail due to unsolved constraints that could be solved by giving a type to a hole, then the program should still be considered well-typed. This mainly occurs when types are ambiguous, with class constraints and no concrete types. If you replace the hole in the expression {{{show _?h}}} with {{{undefined}}}, then {{{show undefined}}} has an unsolved {{{Show}}} constraint and is ill-typed. But with the hole, we would prefer {{{show _?h}}} to be well-typed with a reported hole type {{{_?h :: Show a => a}}}. 
     204 
     205=== Monomorphism restriction === 
     206 
     207The above expectations should hold with and without the monomorphism restriction. In particular, if an {{{undefined}}} somewhere in a program type-checked with the monomorphism restriction would cause type-checking to fail, then a hole in that same position should also cause type-checking to fail. 
     208 
     209'''NOTE''': Give example. 
     210 
     211=== Type of a hole === 
     212 
     213The type of a hole should be the resolved type with minimum constraints. That is, the type of a hole should only have constraints that have not been solved but are either inferred from the context (e.g. {{{show _?h}}}) or given in a type annotation/signature (e.g. {{{_?h :: Show a => a}}}.