Conflicting bindings legal?!
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. But I studied computer science to *not* become a lawyer!! -- Andreas Abel <>< Du bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.abel@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/
Luckily, {-# OPTIONS -fwarn-unused-binds #-} saves me from searching for the formal spec... On 26.02.13 10:25 AM, 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.
But I studied computer science to *not* become a lawyer!!
-- Andreas Abel <>< Du bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY andreas.abel@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/
Hi, Am Dienstag, den 26.02.2013, 10:25 +0100 schrieb Andreas Abel:
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.
in more imperative looking Haskell code, I find it useful to shadow a previous binding by a new "foo <-" binding... People who do not like that should use -Wall (or a more specific flag like -fwarn-name-shadowing). Greetings, Joachim -- Joachim "nomeata" Breitner Debian Developer nomeata@debian.org | ICQ# 74513189 | GPG-Keyid: 4743206C JID: nomeata@joachim-breitner.de | http://people.debian.org/~nomeata
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
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@ifi.lmu.de http://www2.tcs.ifi.lmu.de/~abel/
participants (3)
-
Andreas Abel -
Joachim Breitner -
Tillmann Rendel