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

[Jesper Cockx]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190501/06b17863/attachment.html>