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

[Nicolas Pouillard]

On Wed 24 Oct 2012 - 15:57:45 [+0200], Andreas Abel wrote:
> 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 don't think so. However, like with "let" this Endo definition is actually
accepted and treated like its λ equivalent.

I would like to stress the fact that the implementation [1] was really
straightforward and was heavily reusing the current infrastructure in
place for "let". Essentially there is 3 lines in AbstractToConcrete and
2 lines in TypeChecking.Rules.Term.

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

I think "let" in telescope should follow what "let" in terms can do. I would
simply allow this telescoping "let" notation and keep it in sync with "let" in
terms.

[1] http://hub.darcs.net/np/Agda-TelescopingLet/patch/20121010151753-eb2e9

-- 
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/67d3cfda/attachment.bin