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

[Benjamin Price]

Hi Jesper,

Thanks for taking the time to write this post - rewrite rules are very interesting, and I feel I understand them better now.

I have a question about pattern matching on the parameters of a type:

You say that patterns must match on "generic" parameters, i.e. matching against (or having a rewrite rule on) `_::_ {Bool} x xs` is bad, but `_::_ {a} x xs` is fine.
This is due to (the internal representation of) constructors not storing those arguments, presumably because by pattern-match time, we have already forgotten those arguments corresponding to parameters, and thus have nothing to match against.
However, since pattern matching is type-directed, could we not recover the parameters from the type?
To be concrete, what goes wrong with the following rule (for data D (A : Set) : Set where C : T -> D A)?

  [B : Set // p] => sub1   [s : T[B/A] // q] => sub2
  --------------------------------------------------
  [C {_} s : D B // C {p} q] => sub1 + sub2

where I write an underscore for the elided parameter-argument of the constructor.

Cheers,
Ben

________________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Jesper Cockx <Jesper at sikanda.be>
Sent: 30 October 2019 16:58
To: agda list
Subject: Re: [Agda] New blog post: Hack your type theory with rewrite rules

Hello again,

The second part of my blog series on rewrite rules in Agda is now online: https://jesper.sikanda.be/posts/rewriting-type-theory.html. This time I go into the nitty-gritty details of how rewrite rules work and how they interact with other features of Agda. Comments are very welcome as usual!

-- Jesper

On Mon, Oct 21, 2019 at 3:22 PM Jesper Cockx <Jesper at sikanda.be<mailto: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