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