[Agda] `where' scope

[Cezar Ionescu]

Serge D. Mechveliani <mechvel at botik.ru> wrote:

> And Haskell does recognize _everything_, it does not see an error
> here:

Sorry, you are right.  I have expressed myself badly, I meant |f| is
indeed defined locally just as in Haskell, not that |g| is defined as in
Haskell.  Since |f| is defined both locally and globally, you get a
"multiple definition error".

> So, are you disturbed about Haskell?

Since you ask, yes.

> In the body of  g  there is the	`where' construct,
> and as the name  f  is bound under this `where', Haskell puts that    
> this bounding overrides others.

This appears to be an arbitrary choice.  I see no reason for it over
using the global variable by default.  In any case, there should be a
warning: there is too much scope for error (ghc has options for this
warning, by the way).

> I am sure that Haskell is all right in this point about `where', 
> I used this feature many times, it helps writing clear programs.

We obviously have very different views on "clear programs".

Best,
Cezar.