15
$\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?
$\endgroup$
4
  • 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
    Feb 11 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
    Feb 11 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$ Feb 12 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
    Feb 12 at 14:53

3 Answers 3

14
$\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
$\endgroup$
14
$\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 occurence of the recursive type variable at a negative position, which is by Curry's paradox inconsistent.

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!)

$\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$ Feb 12 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.
$\endgroup$
0

Your Answer

By clicking β€œPost Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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