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

[Jesper Cockx]

Hi Benjamin,

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
https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Rewriting/NonLinMatch.hs#L272-L275
in the implementation if you're interested, 'getFullyAppliedConType does
the application of the constructor type to the parameters).

-- Jesper

On Wed, Nov 6, 2019 at 7:12 PM Benjamin Price <benjamin.price at strath.ac.uk>
wrote:

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