[Agda] Pattern matching on irrelevant types with only one constructor?

[Jesper Cockx]

Well, if we don't have strong normalization we also lose decidability of
typechecking, which is kind of an important design goal of Agda IMO.

-- Jesper

On Wed, May 1, 2019 at 12:17 PM Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> I am just wondering with normalisation under inconsistent assumptions is
> such an important feature? Is this the only thing that goes wrong?
>
>
>
> Thorsten
>
>
>
> *From: *Agda <agda-bounces at lists.chalmers.se> on behalf of Jesper Cockx <
> Jesper at sikanda.be>
> *Date: *Wednesday, 1 May 2019 at 08:48
> *To: *Matthew Daggitt <matthewdaggitt at gmail.com>
> *Cc: *Agda mailing list <agda at lists.chalmers.se>
> *Subject: *Re: [Agda] Pattern matching on irrelevant types with only one
> constructor?
>
>
>
> Hi Matthew,
>
>
>
> In our paper on definitional proof irrelevance (
> https://hal.inria.fr/hal-01859964) we give a criterion for when it is
> allowed to pattern match on an irrelevant argument. As we argue in the
> paper, the condition that the datatype has a single constructor is neither
> sufficient nor necessary. The criterion we give is not yet implemented in
> Agda, but I hope to add it in the not-too-distant future (it depends on my
> PR https://github.com/agda/agda/pull/3589 being merged first).
> Unfortunately, the Acc datatype does not satisfy this criterion. In fact,
> allowing pattern matching on irrelevant Acc would break strong
> normalization of the theory, as you can always have an absurd hypothesis of
> type Acc but evaluation would not be blocked on this argument because it's
> irrelevant. So the best you can do is get propositional  (instead of
> definitional) irrelevance by proving irrelevance of Acc by hand (or
> postulate it).
>
>
>
> A historical note: Agda used to allow matching on single-constructor
> datatypes under the --experimental-irrelevance flag, but this was
> completely broken so I decided to remove it last year (
> https://github.com/agda/agda/commit/b5f8b509bbe362c4bbb14612a6666e720cabf26a
> )
>
>
>
> -- Jesper
>
>
>
> On Wed, May 1, 2019 at 8:33 AM Matthew Daggitt <matthewdaggitt at gmail.com>
> wrote:
>
>  In the Agda documentation
> <https://agda.readthedocs.io/en/v2.6.0/language/irrelevance.html> it is
> pretty clear that the only time you can pattern match against irrelevant
> arguments is when the type is empty. My own reasoning for this has always
> been that this is to stop decisions being made depending on the result of
> the pattern match. This leads me to wonder if there are any theoretical
> reasons why it's not possible to also mark a type irrelevant when it only
> has a single constructor?
>
>
>
> Consider the motivating example below. Clearly the `Acc` argument is never
> actually used in the computation of the final value, and no decisions can
> be based on its value as it only has a single constructor. It seems like it
> should be possible to mark it irrelevant. If this were possible then we
> would immediately get rid of a whole bunch of annoying congruence lemmas.
>
> ```
>
> gcd : (m n : ℕ) → Acc _<_ m → n < m → ℕ
>
> gcd m zero     _         _   = m
>
> gcd m (suc n) (acc rec) n<m = gcd′ (suc n) (m % suc n) (rec _ n<m) (a%n<n
> m n)
>
> ```
>
> Many thanks,
>
> Matthew
>
> _______________________________________________
> Agda mailing list
> 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/20190501/299e4820/attachment.html>