[Haskell-cafe] Conflicting bindings legal?!

[Andreas Abel]

Hi Tillmann,

no, I am not against shadowing.  It's a two-edged sword, but I find it 
very useful.

Shadowing is very intuitive if one can proceed in a left-to-right, 
top-to-bottom order, just as one reads.  Then it is clear that the later 
occurrence of a binding shadows the earlier one.  No formal spec. is 
needed to resolve binding in that case.

The confusion comes when one binding comes from a 'where' which is below 
the use, and another comes from a 'do' or 'let' which is above the use. 
  Then there is no trivial intuitive reading (especially if the block 
structure is implicit and handled by indentation).

Cheers,
Andreas

On 26.02.2013 10:57, Tillmann Rendel wrote:
> Hi,
>
> Andreas Abel wrote:
>> To your amusement, I found the following in the Agda source:
>>
>> abstractToConcreteCtx :: ToConcrete a c => Precedence -> a -> TCM c
>> abstractToConcreteCtx ctx x = do
>>    scope <- getScope
>>    let scope' = scope { scopePrecedence = ctx }
>>    return $ abstractToConcrete (makeEnv scope') x
>>    where
>>      scope = (currentScope defaultEnv) { scopePrecedence = ctx }
>>
>> I am surprised this is a legal form of shadowing.  To understand which
>> definition of 'scope' shadows the other, I have to consult the formal
>> definition of Haskell.
>
> Isn't this just an instance of the following, more general rule:
>
> To understand what a piece of code means, I have to consult the formal
> definition of the language the code is written in.
>
>
> In the case you cite, you "just" have to desugar the do notation
>
>> abstractToConcreteCtx :: ToConcrete a c => Precedence -> a -> TCM c
>> abstractToConcreteCtx ctx x =
>>      getScope >>= (\scope ->
>>      let scope' = scope { scopePrecedence = ctx } in
>>      return $ abstractToConcrete (makeEnv scope') x)
>>    where
>>      scope = (currentScope defaultEnv) { scopePrecedence = ctx }
>
> and it becomes clear by the nesting structure that the lambda-binding
> shadows the where-binding. It seems that if you argue against this case,
> you argue against shadowing in general. Should we adopt the Barendregt
> convention as a style guide for programming?
>
>    Tillmann
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/