Changes between Version 18 and Version 19 of Holes


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

Implicit parameters

Legend:

Unmodified
Added
Removed
Modified
  • Holes

    v18 v19  
    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. 
     87 
     88== Implicit parameters == 
     89 
     90The [http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#implicit-parameters implicit parameters] extension allows a programmer to delay the binding of a variable while still preserving its type. 
     91 
     92Here is an example: 
     93{{{ 
     94$ ghci -XImplicitParams 
     95Prelude> :t ?x : (?y ++ []) 
     96?x : (?y ++ []) :: (?x::a, ?y::[a]) => [a] 
     97}}} 
     98The implicit parameters {{{?a}}} and {{{?b}}} appear as constraints in the type of the term containing them. 
     99 
     100Implicit parameters must be bound, either in a term, e.g. {{{let ?x = ... in ...}}}, or in a type signature, e.g. {{{let f :: (?x::a, Num a) => a; f = 1 + ?x}}}. If an implicit parameter is not bound, it results in a type error. Of course, we can defer the type errors, but then we have the same problem with indiscriminate deferral. 
     101 
     102Implicit parameters do not serve very well for debugging. Due to the binding requirement, they are not suitable for typing things with unknown types. Either you must change type signatures or you must deal with the unbound implicit parameter type errors (or warnings in case the errors are deferred). Lastly, since implicit parameters are meant for usage in programs, it does not seem like they should be used for extracting additional information about the parameter's location. (This is not a technical argument, of course.) 
     103 
     104{{{ 
     105#!comment 
     106Another thing to keep in mind with implicit parameters is that implicit parameters with the same name in different functions are not assumed to be the same (i.e., required to be unifiable), ''except'' if some function has both implicit parameters in its constraints. 
     107}}} 
    87108 
    88109= A proposed concrete design for Haskell = 
     
    115136First, two existing features that can be used as holes. 
    116137 
    117 === Implicit Parameters === 
    118 The GHC extension [http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#implicit-parameters Implicit Parameters] comes closer to how holes are expected to work. This extension makes it possible to specify a term with a question mark, denoting a implicit variable, but this could also be seen as a hole. 
    119  
    120 Same example: 
    121 {{{ 
    122 test = ?a : (?b ++ []) 
    123 }}} 
    124  
    125 Inspecting the type of {{{test}}} when defined in GHCi now shows the types of the (unbound) implicit parameters: 
    126  
    127 {{{ 
    128 > :t let test = ?a : (?b ++ []) in test :: [Bool] 
    129 let test = ?a : (?b ++ []) in test :: [Bool] 
    130   :: (?a::Bool, ?b::[Bool]) => [Bool] 
    131 }}} 
    132  
    133 However, defining {{{test}}} like this in a module gives the following error: 
    134  
    135 {{{ 
    136 test.hs:4:8: 
    137     Unbound implicit parameter (?a::Bool) 
    138       arising from a use of implicit parameter `?a' 
    139     In the first argument of `(:)', namely `?a' 
    140     In the expression: ?a : (?b ++ []) 
    141     In an equation for `test': test = ?a : (?b ++ []) 
    142  
    143 test.hs:4:14: 
    144     Unbound implicit parameter (?b::[Bool]) 
    145       arising from a use of implicit parameter `?b' 
    146     In the first argument of `(++)', namely `?b' 
    147     In the second argument of `(:)', namely `(?b ++ [])' 
    148     In the expression: ?a : (?b ++ []) 
    149 Failed, modules loaded: none. 
    150 }}} 
    151  
    152 This will show you the type, however, it is an error and aborts compilation, so there may be other problems you don't get to see because of it. It also will refuse to load and compile the module, so it's impossible to run the parts of it that are finished. 
    153  
    154 The reason is that the hole becomes a part of the type signature, as a constraint. So to correctly use it here, the function would have to be written as: 
    155  
    156 {{{ 
    157 test :: (?a::Bool, ?b::[Bool]) => [Bool] 
    158 test = ?a : (?b ++ []) 
    159 }}} 
    160  
    161 This makes it very impractical to use them as holes, as all type signatures have to be updated to let the typechecker continue. Not only in the functions that use the implicit parameter itself, but they propagate upwards, just like class constraints: if another function were to call {{{test}}}, it would have the same implicit parameters (and therefore, all of these type signatures would have to be updated when a new hole is added). 
    162  
    163 Another thing to keep in mind with implicit parameters is that implicit parameters with the same name in different functions are not assumed to be the same (i.e., required to be unifiable), ''except'' if some function has both implicit parameters in its constraints. Lastly, it's impossible to run code with unbound implicit parameters, even if the parameters are never actually used. 
    164138 
    165139= How this could be implemented in GHC =