<div dir="ltr"><div dir="ltr"><div>Hi Benjamin,</div><div><br></div><div>My remarks on the constructor parameters refers to rewrite rules on constructors, i.e. ones where the constructor is the head symbol. Since reduction in Agda is untyped, there's no way to reconstruct the parameters in this situation (without major changes to Agda). OTOH when there's a constructor at a nested position in the pattern then there's not even a need to reconstruct the parameters, as they are guaranteed to match by typing. So basically the implementation already works as in the rule you suggest (see <a href="https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs#L272-L275">https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs#L272-L275</a> in the implementation if you're interested, 'getFullyAppliedConType does the application of the constructor type to the parameters).</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Wed, Nov 6, 2019 at 7:12 PM Benjamin Price <<a href="mailto:benjamin.price@strath.ac.uk">benjamin.price@strath.ac.uk</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Jesper,<br>
<br>
Thanks for taking the time to write this post - rewrite rules are very interesting, and I feel I understand them better now.<br>
<br>
I have a question about pattern matching on the parameters of a type:<br>
<br>
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.<br>
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.<br>
However, since pattern matching is type-directed, could we not recover the parameters from the type?<br>
To be concrete, what goes wrong with the following rule (for data D (A : Set) : Set where C : T -> D A)?<br>
<br>
  [B : Set // p] => sub1   [s : T[B/A] // q] => sub2<br>
  --------------------------------------------------<br>
  [C {_} s : D B // C {p} q] => sub1 + sub2<br>
<br>
where I write an underscore for the elided parameter-argument of the constructor.<br>
<br>
Cheers,<br>
Ben<br>
<br>
________________________________________<br>
From: Agda <<a href="mailto:agda-bounces@lists.chalmers.se" target="_blank">agda-bounces@lists.chalmers.se</a>> on behalf of Jesper Cockx <<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>><br>
Sent: 30 October 2019 16:58<br>
To: agda list<br>
Subject: Re: [Agda] New blog post: Hack your type theory with rewrite rules<br>
<br>
Hello again,<br>
<br>
The second part of my blog series on rewrite rules in Agda is now online: <a href="https://jesper.sikanda.be/posts/rewriting-type-theory.html" rel="noreferrer" target="_blank">https://jesper.sikanda.be/posts/rewriting-type-theory.html</a>. 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!<br>
<br>
-- Jesper<br>
<br>
On Mon, Oct 21, 2019 at 3:22 PM Jesper Cockx <<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a><mailto:<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>>> wrote:<br>
Hi Agda folks,<br>
<br>
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 <a href="https://jesper.sikanda.be/posts/hack-your-type-theory.html" rel="noreferrer" target="_blank">https://jesper.sikanda.be/posts/hack-your-type-theory.html</a>. Any comments are welcome here on the mailing list as usual.<br>
<br>
Cheers,<br>
Jesper<br>
</blockquote></div></div>