Let in telescopes, where to put the color? [Re: [Agda] `let' in record decl]

[Andreas Abel]

On 11.10.2012 12:31, Nils Anders Danielsson wrote:
> On 2012-10-11 11:51, Andreas Abel wrote:
>> On 11.10.2012 10:56, Nils Anders Danielsson wrote:
>
>>> Would it be hard to adopt the following notation instead?
>>>
>>>    module MEndo let open Star in (A : ★) where
>>>      Endo : ★
>>>      Endo = A → A
>>
>> Frankly, I think your notation is more confusing...
>
> Well, typically you don't start with a let:
>
>    module M {A B : Set}
>             (f : A → B)
>             let open X f in
>             (p : P f)
>             where
>
>> But maybe the "let" should be dropped instead, e.g.,
>>
>>    data D (A : Setoid)(A = Setoid.Carrier)(a : A) : A -> Set where
>
> I assume that you don't want to drop let from the syntax of expressions.
> I don't want to use different notation for the same thing, depending on
> whether I happen to be writing a telescope or an expression.

I do not think it is very different notation.  The three telecope 
entries listed below are things you can use in a where block or at the 
top level.  There, you do not prefix bindings "x = t" with a let.

>> Summary:  Have three different telescope entries:
>>
>>    x : A
>>    x = t
>>    open M args

Basically, a telescope is a list of declarations of one of the three 
forms.  But since we are not in a block, we do not separate by newlines, 
but encapsulate in parentheses.

What is inconsistent about this is that hiding or instance marking does 
not make sense...

   data D (S : Setoid){A = Setoid.Carrier S}(a : A) ...

"Hidden lets" should be a parse error.

Irrelevant lets are fine, though.

   data D (.S : Setoid){.A = Setoid.Carrier S} ...

A nut to crack for Jean-Philippe and Guilem is where to put the color 
when there is no ":"

   y :{c} A
   let x :{c} A
       x = ?

Where do you put the color {c} if there is no type signature for x?  You 
have to rely on inference only, making it impossible to write that ? 
that can be instantiated with x later.

   data D (S :{c} Setoid)(x = Setoid.Carrier ?) ...

Putting the color on the colon is not consistent with the other forms of 
argument decoration.  An alternative that does not use any new reserved 
symbols is

   data D (.:{c} S : Setoid)(.:{c} x = Setoid.Carrier S)...

but a token like

   .:{

is certainly ugly.  For single color decorations one could allow .:c, e.g.

   data D (.:c S : Setoid) ...

Mmh...


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