[Agda] `where' scope

[Serge D. Mechveliani]

On Mon, Sep 24, 2012 at 10:30:37PM +0200, Cezar Ionescu wrote:
> 
> Agda is not complaining about the localy defined |f|.  Indeed, that
> works just like in Haskell.  It just doesn't know whether you intend the
> local |f| to be applied to (suc x) in the definition of |g|, or the
> global one.  Neither do I, and I would be disturbed if Agda did.
> 
> Best,
> Cezar.

No, no.
Agda  reports of a  _multiple definintion_ of  f  -- of an error.

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

  f :: Int -> Int
  f = succ
  g :: Int -> Int
  g x =  f $ succ x  where
                     f :: Int -> Int
                     f y = y
  h x = f $ f x

  main = putStr (shows (g 0) "\n")

It substitutes  f = (\ y -> y)  into  g,  not the  succ  one.
So that  main  prints  "1".

So, are you disturbed about Haskell?

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.

And in  h,  Haskell substitutes  f = succ,  because the scope of `where' 
in  g  is not visible at this point. 

This all, probably, follows from the lambda representation for functions, 
say, 
     g =  (\ f -> (\ x -> f $ succ x)) (\ y -> y)

(I am not quite sure about this compilation to lambda).

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

But may be Agda has some particular reason for not following this clear
line. I wonder.


> Serge D. Mechveliani <mechvel at botik.ru> wrote:
> 
> > People,	
> > how does this occur that `where' does not protect its local scope?
> > Thus, for
> >   f : Nat -> Nat
> >   f = suc
> >   g : Nat -> Nat
> >   g x =  f $ suc x  where
> >                     f : Nat -> Nat
> >                     f y = y
> > 
> > Agda-2.3.0.1 MAlonzo  reports a  multiple definition of  f.
> > It is natural to put that a value defined under `where' is local and
> > overrides the outer value of the synonym (like in Haskell).
> > 
> > What is a profound reason to change this nice rule?
> > 
> > May be `private' will help, but why does one need to put an extra 
> > `private' ?
> > 
> > Thanks,
> > 
> > ------
> > Sergei
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> 
>