[Agda] Pattern matching on irrelevant types with only one constructor?
Thorsten Altenkirch
Thorsten.Altenkirch at nottingham.ac.uk
Thu May 2 14:55:36 CEST 2019
Hi Jesper,
I was thinking just about deciding definitional equality, confluence somehow becomes an aspect of soundness, I think. But certainly dealing with Metavariables is a very important issue. Do you think one needs small step semantics to specify this or isn’t it rather the case that you deal with a set of constraints and there is some non-determinism which constraints are simplified next and that the final result is independent of these choices is what is referred to as confluence?
Thorsten
From: Jesper Cockx <Jesper at sikanda.be>
Date: Thursday, 2 May 2019 at 13:41
To: Jon Sterling <jon at jonmsterling.com>
Cc: Thorsten Altenkirch <psztxa at exmail.nottingham.ac.uk>, Andrea Vezzosi <sanzhiyan at gmail.com>, agda <agda at lists.chalmers.se>
Subject: Re: [Agda] Pattern matching on irrelevant types with only one constructor?
Hi Jon,
I feel personally addressed when you talk about "people talking about confluence" so let me try to formulate a response. I would argue that confluence (or at least something like it) *is* an important consideration also for languages like Agda and Coq. The reason why is because in practice evaluation is often non-deterministic because of unsolved metavariables: if evaluation is blocked on a metavariable, we often still want to try other evaluation rules that might fire. But we can only do this if the order in which we apply the evaluation rules doesn't matter (which is the meaning of 'confluence' to me). So in some sense confluence allows us to abstract over the concrete (deterministic) evaluation strategy and choose whatever strategy we like for our reasoning. In the end, this helps towards the goal of enabling people to use our languages without having to understand all the implementation details.
-- Jesper
On Thu, May 2, 2019 at 2:27 PM Jon Sterling <jon at jonmsterling.com<mailto:jon at jonmsterling.com>> wrote:
I second this message from Thorsten :) I usually just call "normalization" the abstract idea of obtaining canonical representatives of equivalence classes by a function which is at least sound and complete in the sense Thorsten described, and I also like the stability criterion too.
Indeed, I have noticed that a _lot_ of people are constantly talking about things like "strong normalization" in the context of a language for which an abstract rewriting system has never been defined, and it's really confusing --- maybe not as confusing to us, but probably very confusing for people who know only the definitions of these terms, and are puzzled as to whether we have somehow solved the well-known difficulties in rewriting theory that have made it unpopular as a basis for modern type theories. Worse, I even hear people talk about "confluence" for languages which (1) have never been based on abstract rewriting systems, and (2) the only reduction semantics ever considered was deterministic (!!). I perhaps do not need to explain why it is silly to talk about confluence for something that you already know to be deterministic ;-)
I was hoping that this thread would be an opportunity for people to get conscious of the fact that SN/WN/confluence etc. are all about rewriting, which is very cool, but not closely related to what is happening in modern type theories of the Swedish tradition.
Best,
Jon
On Thu, May 2, 2019, at 7:11 AM, Thorsten Altenkirch wrote:
> I call it "symbolic evaluation" or just "normalisation".
>
> I agree that the term "strong normalisation" is out of date, since we
> usually don't specify different normalisation strategies. I prefer to
> think of a congruence (judgemental or definitional equality) for which
> we can compute normal forms usually using a semantical (NBE) or an
> operational big-step normalisation function. The normalisation function
> should be sound (maps equal terms to identical normal forms), complete
> (the computed normal form is equal to the term we started with modulo
> the embedding of normal forms into terms) and stable (normalizing a
> normal form doesn't change anything, again modulo the embedding).
> Stability entails that we don't have too many normal forms.
>
> See our JFP paper on big step normalisation for example:
> http://www.cs.nott.ac.uk/~psztxa/publ/jtait07.pdf
>
> On 02/05/2019, 09:41, "Agda on behalf of Andrea Vezzosi"
> <agda-bounces at lists.chalmers.se<mailto:agda-bounces at lists.chalmers.se> on behalf of sanzhiyan at gmail.com<mailto:sanzhiyan at gmail.com>> wrote:
>
> Is there an established term for "normalizing in an open context"
> because often I end up saying strong normalization for that, even if
> the part about _every_ reduction path is not quite relevant.
>
>
>
>
>
> On Wed, May 1, 2019 at 4:34 PM Jon Sterling <jon at jonmsterling.com<mailto:jon at jonmsterling.com>>
> wrote:
> >
> > Just to clarify, strong normalization (SN) is irrelevant here ---
> what is relevant is that there exists _some_ normalization strategy.
> Strong normalization is a property of an abstract rewriting system, a
> methodology which generally is not even considered for type theories
> which have strong type-directed equational rules, which tend to disrupt
> confluence. Modern Swedish-style type theories rely on techniques
> beyond abstract rewriting systems for their metatheory, and SN is
> therefore not coming into the picture. It is likely that Agda's core
> language is normalization in the general sense (there is a way to
> choose canonical representatives of definitional equivalence classses),
> and this is really orthogonal to SN/WN/etc (since "normalization" in
> the sense that I just described can be expressed without even
> mentioning an abstract rewriting system).
> >
> > To respond to Thorsten's comments a bit further down the thread,
> I tried really hard to make proof assistants without a complete
> decision procedure for typing practical, and I determined that it is
> not likely to work out. Decidable type checking is good.
> >
> > Best,
> > Jon
> >
> >
> > On Wed, May 1, 2019, at 6:33 AM, Jesper Cockx wrote:
> > > 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<mailto: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<mailto:agda-bounces at lists.chalmers.se>> on behalf of
> Jesper Cockx <Jesper at sikanda.be<mailto:Jesper at sikanda.be>>
> > > > *Date: *Wednesday, 1 May 2019 at 08:48
> > > > *To: *Matthew Daggitt <matthewdaggitt at gmail.com<mailto:matthewdaggitt at gmail.com>>
> > > > *Cc: *Agda mailing list <agda at lists.chalmers.se<mailto: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<mailto: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<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.
> > >
> > >
> > >
> > > _______________________________________________
> > > Agda mailing list
> > > Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
> > > https://lists.chalmers.se/mailman/listinfo/agda
> > >
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
> > https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> 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.
>
>
>
>
>
_______________________________________________
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/20190502/9a9b5fa7/attachment.html>
More information about the Agda
mailing list