[Agda] let vs where

[Thorsten Altenkirch]

Ah thank you. I see actually I can use let arbitrary deep in an expression while where is only allowed on the top level, right?

Yes, building pattern matching into the syntax would make sense. I also like to use local case expressions, where the definitional equality is extended when checking the right hand side of a case expression (we called this the “smart case”.

Thorsten

From: Jesper Cockx <Jesper at sikanda.be>
Date: Saturday, 29 February 2020 at 14:09
To: Thorsten Altenkirch <psztxa at exmail.nottingham.ac.uk>
Cc: agda list <agda at lists.chalmers.se>
Subject: Re: [Agda] let vs where

Hi Thorsten,

'Let' statements are part of the term syntax of Agda and are desugared during typechecking (by inlining). In contrast, 'where' statements are part of the syntax for declarations so they cannot appear inside terms directly. Pattern matching is not part of the term syntax of Agda (unlike Coq where eliminators can appear in terms), so in general pattern matching can only happen at the declaration level.

The exception to this rule are pattern matching lambdas, which are actually implemented internally by lifting the whole expression to an (anonymous) top-level definition. It should probably be possible to extend let-expressions with the same trick. However, this would mean pattern-matching let's would be generative, i.e. two syntactically equal let-expressions might not be definitionally equal since they are desugared to two separate anonymous definitions internally.

Another more drastic solution would be to extend Agda's internal syntax with some kind of pattern-matching construct, e.g. eliminators or case trees. But this would basically require a complete overhaul of Agda's internals, so I do not expect this will happen in the forseeable future (perhaps it could be part of the mythical Agda 3.0).

-- Jesper

On Sat, Feb 29, 2020 at 2:13 PM Thorsten Altenkirch <Thorsten.Altenkirch at nottingham.ac.uk<mailto:Thorsten.Altenkirch at nottingham.ac.uk>> wrote:
Hi,

Can somebody remind me for what (historical ?) reasons “where” allows pattern matching but not “let”? What are the obstacles to fixing this?

Thanks,
Thorsten


This message and any attachment are intended solely for the addressee

and may contain confidential information. If you have received this

message in error, please contact the sender and delete the email and

attachment.



Any views or opinions expressed by the author of this email do not

necessarily reflect the views of the University of Nottingham. Email

communications with the University of Nottingham may be monitored

where permitted by law.






_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda



This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200229/528f76bd/attachment.html>