I am aware that some of the proof assistants (e.g., Isabelle/HOL, Coq) provide an implementation of the so-called record types. For example, the library HOL-Algebra associated with the standard library of Isabelle/HOL relies on the record types for the specification of algebraic structures, such as groups:
Here is a more specific use case:
record 'a monoid = "'a partial_object" + mult :: "['a, 'a] ⇒ 'a" (infixl "⊗ı" 70) one :: 'a ("𝟭ı")
As you can see, the record types are extensible (in the example above,
monoid is "derived" from
partial_object). Nonetheless, they are still very limited in their functionality in comparison to, for example, conventional classes in object-oriented programming. One particular limitation that had practical implications was exposed in several threads of the mailing list of Isabelle, including the following one:
The exposed problem could be seen as closely related to the lack of multiple inheritance in Isabelle's record types.
I have several closely related questions:
- Do any proof assistants provide more comprehensive record types that offer (better) support for multiple inheritance?
- Are there any ongoing/planned projects for bringing (further) OOP features into any of the proof assistants (e.g. introducing methods that can operate only on the record types, etc)?
- Has there been any further progress made on the aforementioned problem specifically in the Isabelle/HOL community?