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.a...@ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
