A recent thread in Lean’s Zulip server with some insights by Mario Carneiro and other folks motivated this post.
The question posed by Chris Lovett was: how can we encode Object Oriented Polymorphism in Lean 4?
The Challenge
As a running example we’ll use the following class hierarchy:
Scala  Java 


Before jumping in let’s recall a few key features of Object Oriented Programming:
 Inheritance
 Subtyping
 Bundling data + functions (a.k.a. methods)
 Methods have access to private state, frequently mutably.
 Dynamic Polymorphism
(Flame) wars have been fought over the exact characterization, but this list seems good enough for our purposes.
Approach 1: Structure Inheritance
First we create a structure corresponding to our interface/trait
structure Shape where
perimeter: Float
area: Float
This will introduce 5 things into the scope:
 A new type
Shape
 A namespace
Shape
 A constructor
Shape.mk : Float → Float → Shape
Shape.perimeter : Shape → Float
Shape.area : Shape → Float
Next we use inheritance to reuse the fields in Shape
:
abbrev Radius := Float
abbrev Side := Float
def Float.pi : Float := 3.1415926535897932385
structure Circle extends Shape where
r: Radius
perimeter := 2 * Float.pi * r
area := Float.pi * r * r
structure Rectangle extends Shape where
(x y: Side)
perimeter := 2 * (x + y)
area := x * y
We’re providing default implementations for perimeter
and area
, and notice how we can refer to r
in the body of other fields, mimicking the implicit this
field common in OO languages.
At this point we can create some values like so:
def c: Circle := {r := 2.4}
def r: Rectangle := {x := 3.1, y := 4.4}
If we wanted we could define constructors to simulate Circle.apply
and Rectangle.apply
in Scala:
def Circle.new (r: Radius): Circle :=
{r := r}
def Rectangle.new (x y: Side): Rectangle :=
{x := x, y := y}
Subtyping
In Java and Scala a consecuence of subtyping is that the system creates a coercion function from subtype to supertype:
val circleToShape: Circle => Shape = <:<.refl
val rectangleToShape: Rectangle => Shape = <:<.refl
// manual coercion
val s1: Shape = circleToShape(Circle(2.4))
val s2: Shape = rectangleToShape(Rectangle(3.1, 4.4))
// automatic coercion
val s3: Shape = Circle(2.4)
val s4: Shape = Rectangle(3.1, 4.4)
Automatic coercion enables the creation of a list of Shapes
from a collection objects of different types, for example:
val shapes: List[Shape] =
List(Circle(2.4), Rectangle(3.1, 4.4))
val areas = shapes.map(_.area)
// List(18.09557368467721, 13.640000000000002)
In this example, we’re providing the type List[Shape]
explicitly, so each element is coerced automatically before adding it to the list.
(If we had not provided the type, then type inference would have found Shape
as the Least Upper Bound of Circle
and Rectangle
)
Inheritance
In Lean, the keyword extends
automatically generates a conversion function to the parent structure:
Circle.toShape: Circle > Shape
Rectangle.toShape: Rectangle > Shape
Recalling the definition of Circle
:
structure Circle extends Shape where
r: Radius
perimeter := 2 * Float.pi * r
area := Float.pi * r * r
we’re introducing the following elements in the scope:
Circle : Type
Circle.mk : Shape → Radius → Circle
Circle.r : Circle → Radius
Circle.toShape : Circle → Shape
 A namespace
Circle
Notice that only the new field r
got its own function. The other fields are nested inside the field toShape
{ toShape := { perimeter := ..., area := ... }, r := ... }
We can use this field to convert a Circle
to a Shape
. In fact Lean does it automatically when using dot notation:
def c: Circle := {r := 2.4}
def r: Rectangle := {x := 3.1, y := 4.4}
#eval c.area
 18.095574
#eval r.area
 13.640000
What is really happening here is:
c.toShape.area
r.toShape.area
On the other hand this doesn’t work:
def c': Shape := {r := 2.4 : Circle}
 type mismatch
 has type
 Circle : Type
 but is expected to have type
 Shape : Type
Coercions
At this point we can use the automatic coercion mechanism provided by Lean:
class Coe (A) (B) where
coe : A > B
An instance of this class carries a function coe
that converts values of type A
into B
. It is applied automatically whenever a type B
is expected but A
was provided:
instance: Coe Circle Shape := ⟨Circle.toShape⟩
instance: Coe Rectangle Shape := ⟨Rectangle.toShape⟩
Now we can use Circle
and Rectangle
whenever a Shape
is required.
def c': Shape := {r := 2.4 : Circle}
def r': Shape := {x := 3.1, y := 4.4 : Rectangle}
def shapes': List Shape := [c', r']
#eval shapes'.map (·.area)
 [18.095574, 13.640000]
Upper Bounds
Coercions can be used as upper bounds of sorts:
Scala  Lean 


Approach 2: Existential types
The idea is to separate data from functionality: data will go into individual structures Circle
, Rectangle
, etc, and funcionality will go into a new type class:
class ShapeOps (A) where
perimeter : A > Float
area: A > Float
Now the data structures
structure Circle where
r: Radius
structure Rectangle where
(x y: Side)
With instances:
instance : ShapeOps Circle where
perimeter  {r} => 2 * Float.pi * r
area  {r} => Float.pi * r * r
instance : ShapeOps Rectangle where
perimeter  {x, y} => 2 * (x + y)
area  {x, y} => x * y
So far so good.
At this point we can use ShapeOps
as a common interface:
def circle: Circle := ⟨2.4⟩
def rectangle: Rectangle := ⟨3.1, 4.4⟩
open ShapeOps
#eval area circle
 18.095574
#eval area rectangle
 13.640000
But there’s a couple of things we can’t do:
 Create a list with circles and rectangles
 Provide a
Circle
when aShapeOps
is required (this doesn’t even make much sense, as these are two different things)
A strange looking type
In order to simulate the idea of a common super type we need to create a type that hides individual subtypes and a way to “upcast”:
structure Shape where
{A: Type}
[ops: ShapeOps A]
shape: A
attribute [instance] Shape.ops  to make Lean use the instance when needed
This is a peculiar structure at first, so let’s spell it out. To create a Shape
we need:
 A type
A
(inferred)  an (implicit) instance
ops
of the classShapeOps A
 a value of type
A
#check @Shape.mk
 @Shape.mk : {A : Type} → [ops : ShapeOps A] → A → Shape
The reason we need to carry around the instance ShapeOps
is that otherwise we can create lists and pass shapes to functions, but we don’t know which type we’re dealing with, so we can’t do anything with the values!
By having the instance ops
alonside the value shape
we can use it to call all functions defined in ShapeOps
.
def shape1: Shape := Shape.mk (Circle.mk 2.4)
def shape2: Shape := Shape.mk (Rectangle.mk 3.1 4.4)
#eval area shape1.shape
 18.095574
#eval area shape2.shape
 13.640000
def shapes1: List Shape := [shape1, shape2]
#eval shapes1.map (fun s => area s.shape)
 [18.095574, 13.640000]
Still we’re manually:
 Creating instances of
Shape
 unwraping
shape1.shape
each time so we can callShapeOps.area
More coercions
(1) Can be addressed with Coe
as before
instance : Coe Circle Shape where coe r := Shape.mk r
instance : Coe Rectangle Shape where coe r := Shape.mk r
def c: Shape := Circle.mk 2.4
def r: Shape := Rectangle.mk 3.1 4.4
def shapes: List Shape := [c, r]
Dispatching on the type
As for (2) we can create an instance ShapeOps Shape
that dispatches on each specific “subtype” by using the operations stored in ops
instance : ShapeOps Shape where
perimeter  {shape, ops} => ops.perimeter shape
area  {shape, ops} => ops.area shape
allowing us to use ShapeOps
functions on Shape
values without unwrapping the underlaying concrete element
#eval area c
 18.095574
#eval area r
 13.640000