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:

trait Shape:
  def perimeter: Double
  def area: Double

type Radius = Double
type Side   = Double

class Circle(r: Radius) extends Shape:
  def perimeter: Double = 2 * math.Pi * r
  def area: Double = math.Pi * r * r

class Rectangle(x: Side, y: Side) extends Shape:
  def perimeter: Double = 2 * (x + y)
  def area: Double = x * y

interface Shape {
  public Double perimeter();
  public Double area();
}

class Circle implements Shape {
  private Double radius;
  
  public Circle(Double radius) { this.radius = radius; }
  
  @Override
  public Double perimeter() { return 2 * Math.PI * radius; }

  @Override
  public Double area() { return Math.PI * radius * radius; }
}

class Rectangle implements Shape {
  private Double sideX;
  private Double sideY;
  
  public Rectangle(Double sideX, Double sideY) {
    this.sideX = sideX;
    this.sideY = sideY;
  }

  @Override
  public Double perimeter() { return 2 * (sideX + sideY); }

  @Override
  public Double area() { return sideX * sideY; }
}

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:

class ShapeContainer[S <: Shape](s: S):
  def shape: S = s

structure ShapeContainer (S) [Coe S Shape] where
  shape: S

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 a ShapeOps 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 class ShapeOps 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:

1. Creating instances of Shape
2. unwraping shape1.shape each time so we can call ShapeOps.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

References

• Structures in Lean 4
• Existential types in Haskell