Deriving: a library for deriving class instances for inductive types

[arthuraa]

Hi everyone,

I would like to announce the release of Deriving v0.1.0 (GitHub - arthuraa/deriving: Class instances for Coq inductive types with little boilerplate, available as coq-deriving on OPAM). It is a library for automating the generation of MathComp class instances for inductive types, akin to how deriving declarations work in OCaml or Haskell. With a few lines of code, you can derive instances of eqType, choiceType, etc. for your types. The instances are defined using the recursion scheme for the types, and they can be generated even for mutually inductive and nested inductive types (provided that you define the recursion scheme yourself). Check the GitHub page for examples!

[pedroabreu]

Cool project, thanks for sharing!

Could you give me a brief summary of what functions will derive give me when I instantiate a type with countType, finType or orderType.

Also, is it theoretically possible to automatically derive these things for non-uniform parameters? If so what are the difficulties that pops up?

What about for dependent types?

Coinductive types are another beast that I know almost nothing about. So I’ll spare you of questions here.

[arthuraa]

For count and choice, it converts the inductive type to a tree representation (GenTree.tree in choice.v), and transports the instances by cancellation. For finite, it generates an enumeration of the type, trying to respect the order of the constructors. For order, it generates a comparison function that compares the elements lexicographically, using the order of the constructors to break ties.

The main difficulty I foresee for dealing with non-uniform parameters is coming up with a generic representation of an inductive type. With uniform parameters, I can just use a list with the types of the arguments of each constructor; when they are non-uniform (or when we have a dependent type), I imagine I would have to use a telescope to encode the constructor types.

[jackyjoy123]

@arthuraa

For count and choice , it converts the inductive type to a tree representation ( GenTree.tree in choice.v ), and transports the instances by cancellation. For finite , it generates an enumeration of the type, trying to respect the order of the constructors. For order , it generates a comparison function that compares the elements lexicographically, using the order of the constructors to break ties.

The main difficulty I foresee for dealing with non-uniform parameters is coming up with a generic representation of an inductive type. With uniform parameters, I can just use a list with the types of the arguments of each constructor; when they are non-uniform (or when we have a dependent type), I imagine I would have to use a telescope to encode the constructor types.

thanks for the awesome information.