Stream: Elpi users & devs

Topic: Support for mutually inductive types


view this post on Zulip Arthur Azevedo de Amorim (Nov 23 2020 at 22:58):

Is there any plan to add support for mutually inductive types soon? I wanted to add them to my deriving library, and was considering using ELPI for writing the reification code.

view this post on Zulip Enrico Tassi (Nov 24 2020 at 06:48):

Not for 8.13. I almost have universe polymorphism, but nothing for mutual fix/inductive. I guess you will have to use something else if you need it soon.

view this post on Zulip Arthur Azevedo de Amorim (Nov 24 2020 at 15:43):

Got it. I'll use something else for now, but I am looking forward to doing the switch to ELPI in the future!

view this post on Zulip Enrico Tassi (Nov 24 2020 at 15:55):

I'm just curious, which are the inductives you want to derive? I mean, mutual inductives are common in, say, semantics but you don't need an eqType on these (usually).

view this post on Zulip Arthur Azevedo de Amorim (Nov 25 2020 at 13:57):

The first time I needed one was precisely to formalize a language (https://github.com/arthuraa/netter/blob/master/coq/Expr.v). It would have been possible to do without the power of eq, but having it readily available is pretty convenient (e.g. sometimes it is better to write e1 == e2 than doing a complicated match).

view this post on Zulip Enrico Tassi (Nov 25 2020 at 14:03):

disentangling zexpr and qexpr is a bit painful, but it seems easy to parametrize the two over bexpr. Then bexpr can be non mutual (assuming you need == there)

view this post on Zulip Enrico Tassi (Nov 25 2020 at 14:06):

Said otherwise, the encoding, at least in this case, of mutual -> single + params, seems possible. But I didn't try, so the positivity checker may not like it.

view this post on Zulip Arthur Azevedo de Amorim (Nov 25 2020 at 14:10):

Yes, I agree that it would have been possible to encode this away. But the encoding would have been awkward... Moreover, I only had to add the eq instance later on in the development, so I would have had to refactor the code. It is just nice to be able to use inductives without having to think about these issues.


Last updated: Feb 04 2023 at 01:03 UTC