[Agda] `let' in record decl

[Andreas Abel]

On 11.10.12 12:31 PM, 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

In this proposal, you need 3 keywords to open a module in a telescope. 
That is ocamlish...

If one could drop "in" when one unindents, and "let" is optional before 
"open", this could be shortened to

    module M {A B : Set}
             (f : A → B)
             open X f
             (p : P f)
             where

Without newlines, the "in" would be necessary

    ... (f : A -> B) open X f in (p : P f) ...

Another example for "in" vs. unindent:

   data D (p : A * B)
          let x , y = p
          (z : C x) ...

Even in expressions I would favor "in" being optional when an unindent 
is present.

   f x = let y = ...
             z , v = ...
         g y z v

I never liked the extra indentation that comes with "in"...

>> 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.
>
>> Summary:  Have three different telescope entries:
>>
>>    x : A
>>    x = t
>>    open M args
>
> I think I would find this more appealing if "let" was removed entirely
> (but that would be a rather disruptive change).
>

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