Avoiding extra matching with extensible GADTs

Thank you for sharing this! I glanced earlier at this lecture, and would take some time to work it out. I also noticed that there’s a bit more related information available at this section of your website.

Do you have some scholarly articles to recommend on this issue?

Also, may I inquire, what is your impression about approaching the issues of extensibility and code reuse in OCaml? There exists an opinion that objects are undesirable, even though in another post in the same thread an important feature is mentioned — the “open recursion” [1]. I do find objects very useful in cases when I need to define a family of slightly different records — in game development context that could be different categories of a weapon, which may be a rifle, a cannon, an auto-cannon, a crossbow, etc. with the set of relevant attributes largely intersecting, but not quite being the same. While, this issue may be tackled through a form of extensible records — and object types are more than sufficient here — the classes emerge as a natural solution to any basic code reuse problems. Why is there such an objection to the object systems in OCaml supported by prominent members of the community? Is there a good replacement, particularly the problem domain I consider — whence there are many distinct entities that have many closely related attributes?

[1] It seems to me that the “open recursion” problem is more of a problem of defining mutually recursive modules, solvable by the use of functors and recursive instantiation.