[Haskell-cafe] Conflicting bindings legal?!

[Tillmann Rendel]

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