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

[Nicolas Pouillard]

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) → …

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.

All the best,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 490 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20121024/67d73af5/attachment.bin