[Agda] New blog post: Hack your type theory with rewrite rules

[Jesper Cockx]

Hi Jon,

The confluence checker is currently only checking local confluence, so if
we want to get the kind of syntactic guarantees you are talking about we
need to either make the confluence check stricter or also check termination
of rewrite rules. Checking termination would of course also be useful to
prevent typechecking from looping. I'm hoping that in the future we can
adapt Dedukti's SizeChangeTool (https://github.com/Deducteam/SizeChangeTool)
by Guillaume Genestier to also work for Agda's rewrite rules.

I fully agree with the sentiment that we should be able to prototype new
extensions to type theory without implementing a new language from scratch.
I have many ideas beyond rewrite rules that would make this more feasible,
e.g. having custom eta rules would be very useful I think.

Best regards,
Jesper

On Mon, Oct 21, 2019 at 9:36 PM Jon Sterling <jon at jonmsterling.com> wrote:

> Hi Jesper,
>
> I'm very pleased to hear that the confluence checker is coming along! Once
> it is in place, what kind of syntactic guarantees (relative to "pure Agda")
> can we expect to be available in the presence of custom rewrite rules?
>
> The main one I'm asking about is transitivity: if judgmental equality is
> transitive in plain Agda, then does one expect it to be transitive in Agda
> mod T, for T a set of rewrite rules that would accepted by the completed
> checker? If so, the rewriting facility sounds totally amazing and really
> useful.
>
> Maybe in the future we can just use Agda to prototype most new extensions
> to type theory, rather than writing our own implementations right away.
>
>
> Best,
> Jon
>
>
>
> On Mon, Oct 21, 2019, at 12:14 PM, Jesper Cockx wrote:
> > Hi Apostolis,
> >
> > Excellent question! Unfortunately, the answer is not an unqualified
> > 'yes'. It is true that using such rewrite rules always preserves
> > soundness of the theory, since rewrite rules are in a sense a limited
> > form of equality reflection, and equality reflection is known to be
> > consistent.
> >
> > However, other more syntactic properties such as confluence,
> > termination, and subject reduction (aka type preservation) can still be
> > broken. In our 2014 paper, I give one such example: the rewrite rules
> > `(suc x) * y == (x * y) + y` and `x * (suc y) == x + (x * y)` are not
> > confluent unless you also have associativity of + as a rewrite rule.
> > It's not very straightforward, but by tricking Agda's constraint solver
> > to solve equations in a particular order, you can exploit a
> > non-confluence like this to break subject reduction. This manifests as
> > a type error complaining two things should be equal even though they
> > are according to the rules.
> >
> > I have actually been working on implementing a confluence checker for
> > rewrite rules (which I'm planning to talk about in an upcoming post).
> > If you want, you can try it out by installing the current master branch
> > of Agda and enabling the --confluence-check flag.
> >
> > Cheers,
> > Jesper
> >
> > On Mon, Oct 21, 2019 at 4:21 PM Apostolis Xekoukoulotakis
> > <apostolis.xekoukoulotakis at gmail.com> wrote:
> > > If you have proved the equality as in your 2nd example, is there any
> reason not to use REWRITE?
> > > My impression is that I should use REWRITE everywhere where I have
> proven a propositional equality so as to make it definitional.
> > >
> > > Nice blog post, and a good reference to a book on type theory. I was
> looking into a good introductory book that would help me understand agda a
> bit better.
> > >
> > > On Mon, Oct 21, 2019 at 4:22 PM Jesper Cockx <Jesper at sikanda.be>
> wrote:
> > >> Hi Agda folks,
> > >>
> > >> I have another blog post for you on extending Agda with rewrite
> rules, with no less than six examples of how they can be used. You can read
> it at https://jesper.sikanda.be/posts/hack-your-type-theory.html. Any
> comments are welcome here on the mailing list as usual.
> > >>
> > >> Cheers,
> > >> Jesper
> > >>  _______________________________________________
> > >>  Agda mailing list
> > >> Agda at lists.chalmers.se
> > >> https://lists.chalmers.se/mailman/listinfo/agda
> > _______________________________________________
> > Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda
> >
> _______________________________________________
> 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/20191024/b4107c3a/attachment.html>