[Agda] moving common from `with'

[Andreas Abel]

On 14.10.2012 16:44, Dan Doel wrote:
> On Sun, Oct 14, 2012 at 7:08 AM, Serge D. Mechveliani <mechvel at botik.ru> wrote:
>>> thus, there is no place to put a 'where' there.  Haskell's 'where' can
>>> also be used in expressions.  But it allows funny stuff like
>>>
>>>    a = let x = 5
>>>        in  x where x = 4
>>>
>>> Well, I could not tell whether the value of a should be 4 or 5 here...
>>>
>>> Adding 'where' to expressions has beend requested before...
>>>
>>
>> I join this request.
>> Concerning `let' and `where', Haskell has proved good.
>> And it is desirable to follow Haskell in this point (as in many others).
>
> No, Haskell's where cannot be attached to expressions. It is attached
> to definitions exactly like Agda's. For instance, in the example
> given, the 'where x = 4' is attached to the 'a =' definition, despite
> the confusing layout. This is kind of obvious if you ask what a there
> is: it's 5.

You are right.  I though so as well, but then confused myself when 
looking at the grammar.

   http://www.haskell.org/onlinereport/syntax-iso.html

It says

   alt 	-> 	pat -> exp [where decls]

meaning 'where' clauses can be attached to expressions in case 
alternatives, but not in general.

Also my example above is laid out in a confusing manner, but it is parsed as

   a = let x = 5 in x
     where
       x = 4

say

   decl
     where
       decl

> The difference in Agda is that expressions do not contain the type of
> definitions that are allowed to have where attached in them. In
> Haskell, any declaration in a let and any alternative in a case may
> have a where attached. But this is not the case in Agda.

Cheers,
Andreas


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/