17
$\begingroup$

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:

  1. Do any proof assistants provide more comprehensive record types that offer (better) support for multiple inheritance?
  2. 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)?
  3. Has there been any further progress made on the aforementioned problem specifically in the Isabelle/HOL community?
Improve this question
$\endgroup$
5
  • 1
    $\begingroup$ I think Lean has number (2). If A is a type (record type or not), a : A and A.f : A -> B -> C (notice f is in the namespace A) then a.f b is short for A.f a b. It works well in practice. Also, you can use type classes to similarly assign functions to some types A. For example, since list is a monad, then l.map f works for l : list A. (That last feature reminds me a lot of Scala and Rust.) $\endgroup$
    – Jason Rute
    Commented Feb 11, 2022 at 20:00
  • 3
    $\begingroup$ I think Lean (especially Lean 4, which is in beta) has all or most of the features you are looking for. I'll leave it up to a more knowledgable person to answer, but I'll leave a few links: Lean has multiple inheritance. Like Scala (which is OO), Rust, OCaml and Haskell, there are type classes in Lean which provide an alternative to inheritance (and work for any type). Diamonds were a problem in Lean 3, but not in Lean 4. $\endgroup$
    – Jason Rute
    Commented Feb 11, 2022 at 22:59
  • 1
    $\begingroup$ @JasonRute The l.map dispatch via typeclasses example does not exist in Lean (but there is a separate list.map, of course). It has been suggested before though, so it may yet find its way into Lean 4. $\endgroup$
    – Sebastian Ullrich
    Commented Feb 12, 2022 at 8:48
  • $\begingroup$ @SebastianUllrich I should have double checked before posting. :/ I was mixing up l.map f and f <$> l. In particular, the OP might still be interested to know that even in Lean 3 type classes do allow one to assign operations to types. For example f <$> l is basically an abbreviation for functor.map f l and reduces to list.map f l because list is an instance of the monad type class (which is an instance of the functor type class). Similarly, n + m reduces to nat.add n m because nat is an instance of the has_add type class. $\endgroup$
    – Jason Rute
    Commented Feb 12, 2022 at 14:53
  • $\begingroup$ I would say proof assistants are more about their cores rather than their frontends, and all the desired OOP features should be implemented in the frontend (i.e. the elaborator). IMO, it is reasonable to have multiple frontends for one proof assistant. $\endgroup$
    – Qinshi Wang
    Commented May 17, 2023 at 21:28

3 Answers 3

Reset to default
15
$\begingroup$

Semantics

The main OOP investigation and modeling in second order type theory was done by Luca Cardelli and Martin Abadi, e.g. in Theory of Objects and later was continued by Anton Setzer in Object-Oriented Programming in Dependent Type Theory. The main idea of OOP embedding intro MLTT (as stated in answer on M-types) is that object instances are infinitary processes that could be modelled directly with coinductive streams (M-types) but in practice for protocol purposes expect a data type and thus at least a free comonad to represent infinitary IO. This machinery slightly reminds general process calculus by Robin Milner, Erlang Virtual Machine (simplified untyped $\pi$-calculus with only spawn, recv, send), and even Smalltalk-80. So today I would bring to table Guarded Cubical as basis to model both OOP and Process Calculus in the look and feel of Cardelli. However this intro is given here only for completeness of answer, this research reminds more modeling environment (semantics) rather than dealing with syntax.

Syntax

As for syntax, for developers in practice as stated by Jason Rute, there is no need to such complex machinery. You need just plain records with field accessors and extends multiple inheritance which is a syntax sugar on top of plain sigmas. You can add unnecessary type classes but in reality they are the same as extensible records. So Lean 4 implements the best machinery on market you need to replace OOP completely.

E.g. in Lean syntax with extensible records and multiple inheritance:

     record pure (P: Type → Type) (A: Type) := 
            (return: P A) 
 
     record functor (F: Type → Type) (A B: Type) := 
            (fmap: (A → B) → F A → F B) 
 
     record applicative (F: Type → Type) (A B: Type)  
    extends pure F A, functor F A B := 
            (ap: F (A → B) → F A → F B)

After macro expansion in plain Sigma for trusted kernels:

def return_sig (F: U → U) : U₁ := Π (A: U), A → F A
def fmap_sig   (F: U → U) : U₁ := Π (A B: U), (A → B) → F A → F B
def ap_sig     (F: U → U) : U₁ := Π (A B: U), F (A → B) → F A → F B

def pure:        U₁ := Σ (F: U → U) (return: return_sig F), 𝟏
def functor:     U₁ := Σ (F: U → U) (fmap: fmap_sig F), 𝟏
def applicative: U₁ := Σ (F: U → U) (return: return_sig F)
                                    (fmap: fmap_sig F)
                                    (ap: ap_sig F), 𝟏

Where 𝟏 means a unit-terminated record in favour of naming last field in telescope for .-syntaxed field accessors:

def ap (a: applicative) := a.ap -- = a.2.2.2.1
Improve this answer
$\endgroup$
15
$\begingroup$

Object oriented programming cannot easily be integrated into proof assistants, because object types are naturally mixed-variance. For example, a Java interface like:

interface IntSet {
  IntSet empty();
  bool member(int x);
  IntSet union(IntSet xs);
}

corresponds to the recursive record type:

$$ \mu a. \{ \mathsf{empty}: a, \mathsf{member}: \mathbb{Z} \to 2, \mathsf{union}: \color{red}{a \to a} \} $$

I've highlighted the problematic part -- this recursive type has an occurrence of the recursive type variable at a negative position, which is inconsistent, by Curry's paradox.

More operationally, mixed-variance recursive types suffice to type the Y combinator. This lets you introduce unbounded recursion into the language, which is inconsistent in a dependently-typed language.

If you did want both dependent and mixed-variance recursive types, the thing to look at is guarded type theory.

(As an aside, Nakano invented guarded recursion precisely to model OO, but for some reason it has been used for almost everything except OO -- everything from the semantics of ML to assembly language!)

Improve this answer
$\endgroup$
1
  • $\begingroup$ I wouldn't bring F-Algebras to explain OOP. This is more for Recursion Schemes, Inductive Types, Fixpoint, System F, etc. $\endgroup$
    – Namdak Tönpa
    Commented Feb 12, 2022 at 13:24
2
$\begingroup$

A certain amount of OOP features can be emulated using ML style modules.

A basic interface for sets for example.

Module Type NSet.
  Axiom T: Set.
  Axiom empty: T -> bool.
  Axiom member: T -> nat -> bool.
  Axiom union: T -> T -> T.
End NSet.
Improve this answer
$\endgroup$
0

Not the answer you're looking for? Browse other questions tagged or ask your own question.