[Agda] trouble with let and where

[Andrea Vezzosi]

Don't you need to know the type of 'e' for the first alternative too?
Otherwise how do you know which projections to apply?

On Tue, Dec 1, 2015 at 4:06 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda