Induction principles extract to ill-typed C++ code

[joom]

Here is an example Coq program:

Module Tree.

Inductive tree (A : Type) :=
| leaf : tree A
| node : A -> tree A -> tree A -> tree A.

End Tree.

Require Extraction.
Extraction Language JSON.
Extraction "Tree.json" Tree.
Extraction Language OCaml.
Extraction "Tree.ml" Tree.

Since I am extracting the entire module, the induction principles (except the Prop ones) tree_rect and tree_rec are also extracted (they can be used for recursion, after all). This is the code I obtain from MCQC:

template<class T, class U, class V, class U = std::invoke_result_t<V, T, std::shared_ptr<tree<T>>, U, std::shared_ptr<tree<T>>, U>>
U tree_rect(U f, V f0, std::shared_ptr<tree<T>> t) {
  return match(t,   [=]() { return f; },
                    [=](auto y, auto t0, auto t1) { return f0(y, t0, tree_rect(f, f0, t0), t1, tree_rect(f, f0, t1)); });
}

This doesn't compile, since U is repeated in the template part. This problem is most apparent in induction principles but I imagine it can appear in other higher-order functions too.

In comparison, this is the code extracted to OCaml for the same induction principle:

(** val tree_rect :
    'a2 -> ('a1 -> 'a1 tree -> 'a2 -> 'a1 tree -> 'a2 -> 'a2) -> 'a1 tree
    -> 'a2 **)

let rec tree_rect f f0 = function
| Coq_leaf -> f
| Coq_node (y, t0, t1) -> f0 y t0 (tree_rect f f0 t0) t1 (tree_rect f f0 t1)

[joom]

Expressing the higher-order function's type with a static_assert might be the solution, but I don't have enough C++ experience to see the possible pitfalls of this approach:

template<class T, class U, class V>
U tree_rect(U f, V f0, std::shared_ptr<tree<T>> t) {
  static_assert(
      std::is_same_v<
        std::invoke_result_t<V, T, std::shared_ptr<tree<T>>, U, std::shared_ptr<tree<T>>, U>, 
        U
      >,
      "f0 must be callable as U f0(T, tree_ptr<T>, U, tree_ptr<T>, U)."
  );
  return match(t,   [=]() { return f; },
                    [=](auto y, auto t0, auto t1) { return f0(y, t0, tree_rect(f, f0, t0), t1, tree_rect(f, f0, t1)); });
}

[elefthei]

Does this work without the static_assert? I don't remember why I enforce function types inside templates, perhaps this helps GCC with function resolution. But indeed there seems to be a bug with higher-order function types in MCQC. So we can either fix code generation so the correct templates are emitted, or get rid of template constraints in generated code (if everything works without them). Maybe instead of U and V you can try using auto, I think that would work and would be the quickest fix.

[joom]

It works without the static_assert, so yes, that's the easiest fix.

auto doesn't work, however: error: 'auto' not allowed in function prototype

But yes, the higher-order function issue goes further than that. For example, this Coq program:

Record foo := { bar : bool -> bool ; baz : bool -> bool }.

Definition mkfoo (b : bool) : foo :=
  {| bar := fun x => b ; baz := fun y => b |}.

Definition myfoo : foo :=
  {| bar := negb ; baz := negb |}.

is extracted to this C++ code:

template<class T, class U>
struct Build_foo {
  bool(bool) a;
  bool(bool) b;
  Build_foo(bool(bool) a, bool(bool) b) {
    this->a = a;
    this->b = b;
  };
};

using foo = std::variant<Build_foo>;

template<class T, class U>
std::shared_ptr<foo> build_foo(T a, U b) {
  return std::make_shared(Build_foo(a, b));
}

std::shared_ptr<foo> mkfoo(bool b) {
  return Build_foo([=](auto _) { return b; }, [=](auto _) { return b; });
}

There are a few issues with this, if I understand correctly:

• Syntax issues (function pointer fields in the struct and the Build_foo arguments should be written bool (*a)(bool).
• build_foo has a type that is too general (for some reason there is no std::invoke_result_t here).
• mkfoo should call build_foo instead of Build_foo, since it returns a std::shared_ptr.
• The C++ lambdas in mkfoo do not type check: they capture b so we cannot pass them as function pointers.

I know you have performance concerns with std::function, but I might give up and do that in my fork, which handles these all of these issues, though I admit, with a performance penalty.

[elefthei]

Using std::function sounds reasonable to me, but I do not expect it will solve all your problems. Admittedly I did a bad job with higher-order functions, but only because I couldn't see a way to do a good job.

For example I don't see a way to make let-polymorphism work in C++.
The language does not allow introducing type variables in the middle of a program.

The capturing problem you pointed out in mkfoo also looks fairly insidious.
In Coq definitions have "memory" (the b here) but in C++ they are simply function calls. Where should b go instead of being captured?

[joom]

For example I don't see a way to make let-polymorphism work in C++.

This may require casting to void *, similar to how extraction to OCaml has to use Obj.magic. I'll think more about it.

Where should b go instead of being captured?

I agree! It should be captured. But putting a function pointer in the struct doesn't allow that. std::function would, though:

struct Build_foo {
  std::function<bool(bool)> a;
  std::function<bool(bool)> b;
  Build_foo(std::function<bool(bool)> a, std::function<bool(bool)> b) {
    this->a = a;
    this->b = b;
  };
};

[elefthei]

Ok that looks promising. I am not able to offer much help until the Fall but I would be happy to merge PRs that fix higher-order functions in a reasonable way. I don't see any reason to maintain two forks of this repo, especially since we seem to be in agreement about what to fix (maybe not so clear on the how yet).

[joom]

Yeah no worries! About the fork: We are planning to do a lot of other changes like custom mappings (like Extract Constant) instead of hard-coded ones, as well as concurrency primitives, and mappings of Coq types into our internal libraries. Maybe we'll be able to push some of our changes (at least the bug fixes) upstream, but otherwise I don't want to bother you (and slow ourselves down) with upstream PRs and code reviews etc.