Proving that two funcs are equivalent is undecidable in general. Still, this SO answer describes some amazing tools!
miniblog.
Related Posts
Interesting discussion contrasting OCaml functors with Java interfaces: https://www.reddit.com/r/ocaml/comments/2gjcos/help_explaining_benefits_of_modules_and_functors
You can abstract over more things with functors, and they have some cool examples. Quaternions!
I also learnt that type checking modules is undecidable in general in OCaml.
Why does a Turing-complete type system make type checking undecidable? https://composition.al/blog/2017/02/27/why-does-a-turing-complete-type-system-make-type-checking-undecidable/ (Java's type checker is Turing complete!)