[Agda] let vs where

[Jesper Cockx]

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> 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
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200229/fb2d2338/attachment.html>