[Agda] trouble with let and where

[Andreas Abel]

Hi Nicolas,

   (x , (y , z)) = e

can be translated as either

   x,y,z = e
   x = fst x,y,z
   y = fst (snd x,y,z)
   z = snd (snd x,y,z)

or as

   open Sigma e renaming (fst to x; snd to y,z)
   open Sigma y,z renaming (fst to y; snd to z)

The difference is that the second alternative creates anonymous modules 
and is probably harder to implement, as the translation cannot be done 
at scope-checking time but has to be at type-checking time (we need to 
infer the type of e first).  In fact, this almost rules out your 
alternative, as `open` has to do something on the scope, but we do not 
call back to scope checking from the type checker.

Cheers,
Andreas

On 01.12.2015 11:03, Nicolas Pouillard wrote:
> On 11/30/2015 02:26 PM, Andreas Abel wrote:
>> Hi Peter & folks,
>
> Hi all,
>
> [...]
>
>> To implement your suggestion,
>>
>>    where
>>      (x , y) = e
>>
>> we could do similar as for `let` and interpret this as
>>
>>    where
>>      x,y = e    -- x,y is a private identifier for sharing e's evaluation
>>      x   = fst x,y
>>      y   = snd x,y
>
> I'm wondering if this is any different but I would suggest the following
> translation:
>
>    where
>      open Σ e renaming (proj₁ to x; proj₂ to y)
>


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

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

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