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

[Andreas Abel]

On 24.10.12 2:43 PM, Nicolas Pouillard wrote:
> On Fri 12 Oct 2012 - 13:44:21 [+0200], Nils Anders Danielsson wrote:
>> On 2012-10-11 16:50, Andreas Abel wrote:
>>> On 11.10.2012 12:31, Nils Anders Danielsson wrote:
>>>> 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.
>>
>> At the moment a syntactically valid telescope Γ is also a syntactically
>> valid expression "prefix": Γ → Set is syntactically valid, for instance.
>> I don't understand why you would want to break this property.
>
> I don't think any of the proposals break this property (but I might have
> misunderstood). In this patch we actually extends all forms of telescopes
> in Agda. This includes the form "Γ → τ". For instance:
>
>    g : (A : Set) (let EA = Endo A) (f : EA) → EA
>    g A f = f
>
> this would be a valid Agda definition. Or with Andreas suggestion:
>
>    g : (A : Set) (EA = Endo A) (f : EA) → EA
>    g A f = f
>
> About Andreas suggestion, its is in conflict with local definitions with a
> type signature. Example:
>
> d : (let Endo : Set → Set
>           Endo A = A → A) → …
>
>    vs.
>
> d : (Endo : Set → Set
>       Endo A = A → A) → …

So you want more than abbreviations?  I do not thing we should allow 
declarations there which cannot be expanded away.  Like the one you 
gave.  Endo can still be treated with an abbreviation:

   (Endo = \ (A : Set). A -> A) ...

or

   (Endo = (\ A -> A) : Set -> Set) ...

where : is the funny unicode colon to provide a type annotation.

> Which would be both hard to parse and would bring some confusion I guess.
>
> I propose to stick to our current proposal which I think fits well in the
> telescope notation and is explicit enough for the parser and the reader.

Before we fix our decision, we should have good reasons for our choice. 
  What about other languages, what were their choices? (LEGO, Epigram?, 
Coq?)

Cheers,
Andreas

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