Stream: math-comp users

Topic: Deriving instances


view this post on Zulip Arthur Azevedo de Amorim (Dec 02 2020 at 20:12):

Hi everyone. I've been working on a library to derive instances of mathcomp classes for basic inductive types. The code lives here, and it is available as coq-deriving on the extra-dev OPAM repository. I was planning on cleaning the code releasing a first version soon, so I would be very interested in any feedback that you guys have!

view this post on Zulip Christian Doczkal (Dec 03 2020 at 09:04):

You may be interested in the strongly related work by @Enrico Tassi : Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq.

view this post on Zulip Enrico Tassi (Dec 03 2020 at 09:07):

I think @Arthur Azevedo de Amorim is aware of my work. His work covers less inductive types, IIRC, but is pure gallina, so zero external dependencies and zero maintenance cost (it's correct by typing). IMO it would be a nice companion to eqType for example.

view this post on Zulip Christian Doczkal (Dec 03 2020 at 09:15):

Okay, my main interest for bringing this up was to get someone to compare the two, thank you. If I recall your talk on the subject correctly, then your work does not require the user to write recursors for nested inductive types, does it? (I guess whether coq-elpi is to be considered an external dependency depends on how quickly the port to HB becomes part of mathcomp master).

view this post on Zulip Arthur Azevedo de Amorim (Dec 03 2020 at 14:07):

Until recently, Deriving could only handle non-mutual inductive definitions. I just added support for mutual inductives, which allows you to handle nested inductives as well (provided the user is willing to write their own recursors).

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

What is not very pretty about the library is the inference part, which reifies the recursor of a type. It uses a combination of Ltac, type classes and canonical structures, and it's been a bit challenging to maintain. It would be nice to see if this would be more natural to program in ELPI.

view this post on Zulip Arthur Azevedo de Amorim (Dec 03 2020 at 14:16):

I have also found it challenging to simplify the generated terms for things like eq_op. Doing it naively causes the performance to blow up quickly, and doing it faster is hard to maintain. I've managed to get the performance to acceptable levels for small types, and tolerable levels for larger types. But there is a lot of room for improvement.


Last updated: Oct 13 2024 at 01:02 UTC