[Agda] trouble with let and where

[Andreas Abel]

On 01.12.2015 16:35, Andrea Vezzosi wrote:
> Don't you need to know the type of 'e' for the first alternative too?
> Otherwise how do you know which projections to apply?

Yes, I do, but it is sufficient to do this at type-checking time.

Parsing tells me that

   (x , (y , z)) = e

defines 3 new symbols x, y, and z.  This can be done during scope-checking.

The actual definitions of x, y, and z are supplied during type-checking, 
as usual.

> 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


-- 
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/