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

Andreas Abel andreas.abel at ifi.lmu.de
Thu Oct 11 16:50:48 CEST 2012

```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:
>
>>>
>>>    module MEndo let open Star in (A : ★) where
>>>      Endo : ★
>>>      Endo = A → A
>>
>> Frankly, I think your notation is more confusing...
>
>
>    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.

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