A recent thread (public archive) 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 (plus some auxiliary definitions, like Shape.rec, that we won't need):

• 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 reference 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}

Keep in mind that these defaults are values, not methods: Lean computes them once, when it creates the structure. If we update r later, the area stays the same:

#eval ({ c with r := 10 } : Circle).area
-- 18.095574

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 consequence of subtyping is that we get a coercion function from subtype to supertype for free (it is just the identity):

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 of 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 accepted as a Shape (no conversion happens at run time).

(If we had not provided the type, then type inference would have found Shape as a common supertype of Circle and Rectangle. The least upper bound is the union type Circle | Rectangle, but Scala 3 widens it to Shape)

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 := ... }

(Newer versions of Lean print this value flat, as { perimeter := ..., area := ..., r := ... }. Use set_option pp.structureInstances.flatten false to see the nesting.)

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
--   { perimeter := 2 * Float.pi * 2.4, area := Float.pi * 2.4 * 2.4, r := 2.4 }
-- has type
--   Circle
-- but is expected to have type
--   Shape

Coercions

At this point we can use the automatic coercion mechanism provided by Lean. It is based on this class (simplified; Lean already defines it, so we don't write it ourselves):

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 values whenever a Shape is required (but a List Circle is still not a List Shape: there's no covariance).

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]

A word of caution, though. In the thread, Mario Carneiro said: "I would generally want to stay away from implicit conversions (Coe)". The reason is that they can cause type inference problems when there is also other polymorphism.

Upper Bounds

Coercions can be used as a kind of upper bound:

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

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

One difference: <: is reflexive and transitive, but a Coe instance is not. ShapeContainer Shape doesn't compile (there's no Coe Shape Shape), and a chain of coercions doesn't count either. The class CoeTC (the reflexive, transitive closure of Coe) is closer to <:.

Approach 2: Existential types

(This is a fresh start: use a new file or a new namespace. We still need Radius, Side and Float.pi from above.)

The idea is to separate data from functionality: data will go into individual structures Circle, Rectangle, etc., and functionality 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 idea comes from Mario Carneiro in the Zulip thread: his DynVector structure has the same fields (a type, an instance and a value), and he explained why we need the attribute [instance] line.

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

In Lean terms, Shape is a dependent pair, like (A : Type) × ShapeOps A × A. (We can't use Lean's ∃ here: it lives in Prop, so we couldn't get A back out.)

#check @Shape.mk
-- @Shape.mk : {A : Type} → [ops : ShapeOps A] → A → Shape

Because Shape holds a type, it lives one universe up: Shape : Type 1. That's why ShapeOps takes (A) without a type: with (A : Type), the instance ShapeOps Shape that we define below doesn't compile.

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 alongside 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. unwrapping 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 underlying concrete element

#eval area c
-- 18.095574
#eval area r
-- 13.640000

References

• Structures in Lean 4
• Existential types in Haskell