OO polymorphism?

Stream: lean4

[Chris Lovett]

Is there no equivalent to object oriented polymorphism in Lean? This doesn't compile:

structure Point where
  x : Float
  y : Float

structure Point3D extends Point where
  z : Float

def printPoint (p : Point) : IO Unit :=
  IO.println s!"{p.x}, {p.y}"

def main : IO Unit :=
  let p : Point3D := { x := 1.0, y := 2.0, z := 3.0 }
  printPoint p

Saying :

application type mismatch
  printPoint p
argument
  p
has type
  Point3D : Type
but is expected to have type
  Point : Type

But p "is a" Point since Point3D extends Point...

[Adam Topaz]

you could use Point3D.toPoint

[Adam Topaz]

Or use typeclasses:

class Point (α : Type _) where
  x : α → Float
  y : α → Float

structure Point3D where
  x : Float
  y : Float
  z : Float

def printPoint (p : α) [Point α] : IO Unit :=
  IO.println s!"{Point.x p}, {Point.y p}"

instance : Point Point3D where
  x := Point3D.x
  y := Point3D.y

def main : IO Unit :=
  let p : Point3D := { x := 1.0, y := 2.0, z := 3.0 }
  printPoint p

[Jason Rute]

I wounded if there is (or should be) an automatic type class, where (say)Point.IsExtention T means that T is Point or an extension of Point. That would provide “object oriented polymorphism”.

[Jason Rute]

…but that is probably overkill when a simple type class would suffice.

[Chris Lovett]

Ok, but that's a lot more code and complexity. Now how do I add Point4D where the 4D point can be used everywhere the 3D point can and everywhere the 2D point can? Is there a typeclass-instance explosion required here?

[Chris Lovett]

One of the major benefits of OO polymorphism is when a subtype can travel through the system and be discovered later by runtime type check, but your instance converting Point3D to Point throws that away, that result can never be "cast" back to a Point3D...

[Kyle Miller]

Dot notation will insert projections automatically:

structure Point where
  x : Float
  y : Float

structure Point3D extends Point where
  z : Float

def Point.printPoint (p : Point) : IO Unit :=
  IO.println s!"{p.x}, {p.y}"

def main : IO Unit :=
  let p : Point3D := { x := 1.0, y := 2.0, z := 3.0 }
  p.printPoint

[Adam Topaz]

Kyle Miller said:

Dot notation will insert projections automatically

Nice! I didn't know about this.

[Kyle Miller]

(That feature's been backported to Lean 3, too)

[Adam Topaz]

I don't think anyone will miss the e.to_ring_hom.to_add_monoid_hom.ker nonsense.

[Patrick Massot]

Yes, I'm already addicted to this change in Lean 3.

[Patrick Massot]

Note however that the infoview still shows the long version.

[Jason Rute]

@Chris Lovett When you say "OO polymorphism", do you mean "inheritance"? First Lean doesn't have inheritance. (Edit: Although in this particular case of structures, apparently Lean is smart enough to project to the parent structure as Kyle's answer shows). If it had full inheritance it would have to account for variances. (For example if you gave def foo : Point -> Point := id a Point3D, would it return a Point3D or a Point? If you say it should return Point, it would no longer be injective which is a provable property of foo. And if you say a Point3D, what about where the output doesn't depend on the input likedef bar (p : Point) : Point := {0, 0}?)

[Jason Rute]

I was a Scala programmer for a while, and Scala is interesting because it is a functional language with both inheritance (including co/contra-variance) and type classes. So you can have List inherit from Seq (which is the parent of a number of sequence data structures), but also could have a typeclass HasSeq which full-fills the same role. The advantage of the latter is that you can declare that other objects which didn't extend from Seq to begin with behave like a Seq and should count in the Seq API. Here is your example using that typeclass pattern:

structure Point where
  x : Float
  y : Float

class HasPoint (α : Type _) where
  toPoint:  α → Point

structure Point3D extends Point where
  z : Float

instance : HasPoint Point3D where
  toPoint := Point3D.toPoint

instance : HasPoint (Float × Float) where
  toPoint := fun (a, b) => { x := a, y := b }

def printPoint [HasPoint α] (p : α) : IO Unit :=
  let p := HasPoint.toPoint p
  IO.println s!"{p.x}, {p.y}"

def main : IO Unit :=
  let p : Point3D := { x := 1.0, y := 2.0, z := 3.0 }
  let _ := printPoint p
  let p := (1.0, 2.0)
  printPoint p

[Jason Rute]

Notice if I used this pattern for my examples foo and bar above I would have to explicitly state the return type, avoiding any contradictions and ambiguity.

[Chris Lovett]

Yes it is covariance and contravariance I'm looking for and I would understand if the real answer is "lean doesn't do it because it is too hard to prove correctness". But when I add point4d in your example I get an error? And notice the explosion I was talking about... most of this would never have to be written in a C# program:

structure Point where
  x : Float
  y : Float

class IsPoint (α : Type _) where
  toPoint:  α → Point

structure Point3D extends Point where
  z : Float

class IsPoint3D (α : Type _) where
  toPoint3D:  α → Point3D

structure Point4D extends Point3D where
  w : Float

instance : IsPoint Point3D where
  toPoint := Point3D.toPoint

instance : IsPoint3D Point4D where
  toPoint3D := Point4D.toPoint3D

instance : IsPoint Point where
  toPoint := Point4D.toPoint

instance : IsPoint (Float × Float) where
  toPoint := fun (a, b) => { x := a, y := b }

instance : IsPoint3D (Float × Float × Float) where
  toPoint3D := fun (a, b, c) => { x := a, y := b, z := c }

def printPoints [IsPoint α] (p : List α) : IO Unit :=
  for a in p do
    let p := IsPoint.toPoint a
    IO.println s!"{p.x}, {p.y}"

def print3DPoints [IsPoint3D α] (p : List α) : IO Unit :=
  for a in p do
    let p := IsPoint3D.toPoint3D a
    IO.println s!"{p.x}, {p.y}, {p.z}"

def main : IO Unit :=
  let p : Point3D := { x := 1.0, y := 2.0, z := 3.0 }
  let q : Point4D := { x := 1.0, y := 2.0, z := 3.0, w := 5.0 }
  printPoints [p]
  print3DPoints [p, q]

#eval main

[Jason Rute]

Most of the explosion is boilerplate, and if this use case was common enough it could be handled automatically with my proposal here:
Jason Rute said:

I wonder if there is (or should be) an automatic type class, where (say)Point.IsExtention T means that T is Point or an extension of Point. That would provide “object oriented polymorphism”.

[Jason Rute]

Chris Lovett said:

Yes it is covariance and contravariance I'm looking for and I would understand if the real answer is "lean doesn't do it because it is too hard to prove correctness".

I would go further and say that it would significantly change the type theory, maybe at the kernel level even. I'm not sure if anyone has worked on DTT with inheritance, and it could be easy to introduce inconsistencies. Even Scala 2 is known to be inconsistent (in a type theoretic sense which isn't a big deal for most users) and that lead to a big push to formally verify the Dotty type theory used in Scala 3.

[Jason Rute]

Also, I think Kyle's answer (which shouldn't get lost in this conversation) covers 90% of any cases (including yours) where one would want inheritance in the simple setting where the output type doesn't use Point (and the input is an extension of Point). I just checked and this notation prevents all the issues I expressed above by just failing to compile for them.

def Point.xx (p : Point) : Float := p.x
def Point.foo (p : Point) : Point := p
def Point.bar (p : Point) : Point := { x:= 0, y := 0 }

def p3d : Point3D := { x := 1.0, y := 2.0, z := 3.0 }
#eval p3d.xx
#eval p3d.foo  -- fails
#eval p3d.bar  -- fails

[Adam Topaz]

Chris Lovett said:

Yes it is covariance and contravariance I'm looking for and I would understand if the real answer is "lean doesn't do it because it is too hard to prove correctness".

Is this a Lean-specific thing, or a functional programming thing? How would one handle such paradigms in, say, haskell?

[Jason Rute]

@Adam Topaz One answer is that the concept of variance is there even if it is not explicitly in the language. (For example here is a discussion about variance and type classes in Haskell.) But my understanding is if your language has inheritance and is are statically typed, then you need to support it in the language explicitly one way or another. I don't know Haskell well, but I I assume like Lean it doesn't have inheritance.

[Chris Lovett]

Another useful variation on this theme for oo-style programming are contravariance in Arrays and Lists (containers in general), being able to do this:

let p : Point = { x:= 0, y := 0 }
let  q  : Point3D := { x := 1.0, y := 2.0, z := 3.0 }
let a : List Point = [p, q]

Which lean also disallows. I remember Eric Meijer did a lot of work on the soundness of co and contravariance in C# when he was working on the LINQ features and I know he's a huge Haskel fan, so I wonder how much formal type theory he wrote to prove its correctness? I remember seeing pages of type theory proofs, but I don't know where they were kept or published...

[Tom]

I would expect that would it make Lean much less capable of inferring your types, or would/could lead to overgeneralized upper/lower type bounds. I've spent a fair bit of time with Scala and came away really disliking the type system - it seemed to have suffered from a lot of the "worst of both worlds".
Worth remembering that Haskell's type system is nowhere near as powerful as Lean's; and in almost all cases when you want to use "inheritance" my experience is that one would be better off using type classes, projections or just plain old inductive (sum) types.

[Juan Pablo Romero]

@Chris Lovett in addition to using dot notation (which adds a coercion automatically), you can define your own coercions like this:

structure Point where
  x : Float
  y : Float

def Point.printPoint (p : Point) : IO Unit :=
  IO.println s!"{p.x}, {p.y}"

structure Point3D extends Point where
  z : Float

def p3 : Point3D where
  x := 1.0
  y := 2.0
  z := 3.0

instance : Coe Point3D Point where
  coe := Point3D.toPoint


structure Point4D extends Point3D where
  w : Float

def p4 : Point4D where
  x := 1.0
  y := 2.0
  z := 3.0
  w := 4.0

instance : Coe Point4D Point3D where
  coe := Point4D.toPoint3D

#eval p3.printPoint
#eval Point.printPoint p3
#eval p4.printPoint
#eval Point.printPoint p4

def pps : List Point := [p3, p4]

[Juan Pablo Romero]

I was playing the other day with this notation

infixl:65 " <: " => Coe

so I could write

def myFunction [A <: B] (a: A) := ...

But that might bee too much :)

[Juan Pablo Romero]

I guess one can also mimic functor co/contravariance like so:

instance covariantCoercion [Coe A B] [Functor F] : Coe (F A) (F B) where
  coe := Functor.map Coe.coe

def p3s: List Point3D := [p3, p3]
def p4s: List Point3D := [p4, p4]

def pps2 : List Point := p3s
def pps3 : List Point := p4s

... similar for contravariance

[Mario Carneiro]

Chris Lovett said:

Ok, but that's a lot more code and complexity. Now how do I add Point4D where the 4D point can be used everywhere the 3D point can and everywhere the 2D point can? Is there a typeclass-instance explosion required here?

More boilerplate isn't really an argument against this modeling technique, because that can be automated away if it is a sufficiently important use case. I think the semantics OO inheritance is captured fairly directly via a typeclass like ToPoint; it's just a question of how to make the syntax around it sufficiently clean to be useful.

[Mario Carneiro]

@Chris Lovett Here's a working version of your example:

structure Point where
  x : Float
  y : Float

class ToPoint (α : Type _) where
  toPoint : α → Point

instance : ToPoint Point where
  toPoint := id

structure Point3D extends Point where
  z : Float

class ToPoint3D (α : Type _) where
  toPoint3D : α → Point3D

instance : ToPoint3D Point3D where
  toPoint3D := id

instance [ToPoint3D α] : ToPoint α where
  toPoint x := (ToPoint3D.toPoint3D x).toPoint

structure Point4D extends Point3D where
  w : Float

class ToPoint4D (α : Type _) where
  toPoint4D : α → Point4D

instance : ToPoint4D Point4D where
  toPoint4D := id

instance [ToPoint4D α] : ToPoint3D α where
  toPoint3D x := (ToPoint4D.toPoint4D x).toPoint3D

instance [ToPoint α] : Coe α Point where
  coe := ToPoint.toPoint

instance [ToPoint3D α] : Coe α Point3D where
  coe := ToPoint3D.toPoint3D

instance [ToPoint4D α] : Coe α Point4D where
  coe := ToPoint4D.toPoint4D

def printPoints (p : List Point) : IO Unit :=
  for p in p do
    IO.println s!"{p.x}, {p.y}"

def print3DPoints (p : List Point3D) : IO Unit :=
  for p in p do
    IO.println s!"{p.x}, {p.y}, {p.z}"

def main : IO Unit := do
  let p : Point3D := { x := 1.0, y := 2.0, z := 3.0 }
  let q : Point4D := { x := 1.0, y := 2.0, z := 3.0, w := 5.0 }
  printPoints [p]
  print3DPoints [p, q]

[Mario Carneiro]

I would generally want to stay away from implicit conversions (Coe) for this sort of thing though. That's what leads to type inference issues in the presence of all the other polymorphism

[Mario Carneiro]

All of the classes and instances are very easily automatable as a macro, it just uses the shape of the extends on the structure. But my rust-based sensibilities tell me that the whole thing is probably a bad idea and it's not a good way to structure your program, so I would probably try to #xy your problem if you have a specific reason to investigate this.

[Sebastian Ullrich]

Yeah, Rust is a very prominent example of a general trend away from inheritance towards composition, from object oriented to functional. It's also interesting to note that while Rust does not have coercions, it does have a very general typeclass/trait-based system for "redirecting" dot notation.

[Sebastian Ullrich]

Chris Lovett said:

Another useful variation on this theme for oo-style programming are contravariance in Arrays and Lists (containers in general)

Note that array variance is famously broken in both C# and Java

[Julian Berman]

Even some of us OO people don't think inheritance is a particularly nice thing :P

[Yuri de Wit]

Re: dot notation inserting projections automatically, I noticed the following:

structure Point where
  x : Float
  y : Float
deriving Repr

structure Point3D extends Point where
  z : Float
deriving Repr

def Point3D.printPoint (p : Point) : IO Unit :=
  IO.println s!"{repr p}"

#eval { x := 1.0, y := 2.0, z := 3.0 : Point3D}.printPoint
-- ERROR: invalid field notation, function 'Point3D.printPoint' does not have argument with type (Point3D ...) that can be used, it must be explicit or implicit with an unique name

I guess in theory there could be a coercion here too? I.e. look for a argument of the same (structure) type but in case it fails look for Point (following the extends relation)?

[Yuri de Wit]

Along the same lines (also briefly touched upon in an earlier Zulip thread): could this same coercion happen (automatically) on a regular, non-dot notation call? For example:

structure Point where
  x : Float
  y : Float
deriving Repr

structure Point3D extends Point where
  z : Float
deriving Repr

def printPoint (p : Point) : IO Unit :=
  IO.println s!"{repr p}"

#eval printPoint { x := 1.0, y := 2.0, z := 3.0 : Point3D}
--  application type mismatch
--   printPoint { toPoint := { x := 1.0, y := 2.0 }, z := 3.0 }
-- argument
--   { toPoint := { x := 1.0, y := 2.0 }, z := 3.0 }
-- has type
--   Point3D : Type
-- but is expected to have type
--   Point : Type

I can't judge how useful these would be in practice, so just thinking out loud here.

[Mario Carneiro]

Why would you call the definition Point3D.printPoint if it takes a Point?

[Mario Carneiro]

The dot-notation smarts are for determining what namespaces to look in when the receiver at the application site has a different type from the function we want to call. It doesn't try to resolve inconsistencies between the definition and its own namespace, since you can easily fix that by just putting it in the right namespace

[Yuri de Wit]

The idea is that printPoint may take either a Point3D or Point without enforcing in what namespace it is declared.

But maybe that is the intention of the asymmetry? I.e. dot notation works "down" from an extended structure (from Point to Point3D, in this case) but not "up"?

[Kyle Miller]

Chris Lovett said:

One of the major benefits of OO polymorphism is when a subtype can travel through the system and be discovered later by runtime type check, but your instance converting Point3D to Point throws that away, that result can never be "cast" back to a Point3D...

This can't happen in Lean without additional modeling since the type of a term is the complete interface for the term. If two Points are indistinguishable as Points, then they are equal -- it's impossible to know whether or not one of them was "really" a Point3D.

That doesn't mean it can't be done, but it takes some boilerplate to get terms to remember what they really are. I've put together a mockup where you know ahead of time all the types that you want to participate in this subtyping scheme, and then (borrowing Common Lisp terminology) each of these types has an associated structure of "slots" along with casts that let you project these slots structures onto supertype slots structures. There's probably a way to make the types participating in subtyping more extensible, but at least with this version since you have a complete picture of your type system you can prove things about it.

The code is below, but for an example, here's a run-time cast:

def Obj.get_w (o : Obj Point2D) : Float :=
  if h : o.can_cast Point4D then
    (o.cast h).get.w
  else
    0

Here's creating a Point4D object, casting it to a Point2D, then applying this function

#eval Id.run do
  let p := ({x := 1, y := 2, z := 3, w := 4 : Slots_Point4D} : Obj Point4D)
  return p.cast_up.get_w -- N.B. p.cast_up is an `Obj Point2D` here
-- 4.000000

code

inductive Geo_Type
| Point2D
| Point3D
| Point4D
| Square2D
deriving DecidableEq

open Geo_Type

structure Slots_Point2D where
  (x y : Float)

structure Slots_Point3D extends Slots_Point2D where
  z : Float

structure Slots_Point4D extends Slots_Point3D where
  w : Float

structure Slots_Square2D extends Slots_Point2D where
  width : Float

def Geo_Type.Slots : Geo_Type → Type
| Point2D => Slots_Point2D
| Point3D => Slots_Point3D
| Point4D => Slots_Point4D
| Square2D => Slots_Square2D

/-- Get casting function to first type from second type -/
def Geo_Type.cast : (t : Geo_Type) → (t' : Geo_Type) → Option (t'.Slots → t.Slots)
| Point2D, Point2D => some id
| Point2D, Point3D => some (λ x => x.toSlots_Point2D)
| Point3D, Point3D => some id
| Point2D, Point4D => some (λ x => x.toSlots_Point2D)
| Point3D, Point4D => some (λ x => x.toSlots_Point3D)
| Point4D, Point4D => some id
| Point2D, Square2D => some (λ x => x.toSlots_Point2D)
| Square2D, Square2D => some id
| _, _ => none

/-- Whether the second type is a subtype of the first. -/
def Geo_Type.supertype (t t' : Geo_Type) : Bool := (t.cast t').isSome

theorem Geo_Type.supertype.trans (h : Geo_Type.supertype t t') (h' : Geo_Type.supertype t' t'') :
  Geo_Type.supertype t t'' :=
by
  cases t
  all_goals
    cases t'
    all_goals
      cases t''
      all_goals
        simp at h
        try simp at h'
        try simp

def Option.get : (x : Option α) → x.isSome → α
| some v, _ => v
| none, h => by simp [isSome] at h

/-- Get the cast function from a proof that `t'` is a subtype of `t`. -/
def Geo_Type.supertype.cast (h : Geo_Type.supertype t t') : t'.Slots → t.Slots :=
(Geo_Type.cast t t').get (by rw [supertype] at h; exact h)

/-- Objects of subtype t -/
structure Obj (t : Geo_Type) where
  ty : Geo_Type
  sub : Geo_Type.supertype t ty
  slots : ty.Slots

instance : Coe Slots_Point2D (Obj Point2D) where coe s := ⟨Point2D, rfl, s⟩
instance : Coe Slots_Point3D (Obj Point3D) where coe s := ⟨Point3D, rfl, s⟩
instance : Coe Slots_Point4D (Obj Point4D) where coe s := ⟨Point4D, rfl, s⟩
instance : Coe Slots_Square2D (Obj Square2D) where coe s := ⟨Square2D, rfl, s⟩

/-- Extract the slots from an `Obj`. -/
def Obj.get (o : Obj t) : t.Slots := Geo_Type.supertype.cast o.sub o.slots

/-- Cast up, which can be done statically. -/
def Obj.cast_up (o : Obj t) (h : Geo_Type.supertype t' t := by rfl) : Obj t' where
  ty := o.ty
  sub := Geo_Type.supertype.trans h o.sub
  slots := o.slots

def Obj.can_cast (o : Obj t) (t' : Geo_Type) : Bool := Geo_Type.supertype t' o.ty

/-- Cast up or down using run-time information. -/
def Obj.cast (o : Obj t) (h : o.can_cast t') : Obj t' where
  ty := o.ty
  sub := h
  slots := o.slots

/-- Example using a run-time cast. -/
def Obj.get_w (o : Obj Point2D) : Float :=
  if h : o.can_cast Point4D then
    (o.cast h).get.w
  else
    0

#eval ({x := 1, y := 2 : Slots_Point2D} : Obj Point2D).get_w
-- 0.000000

#eval Id.run do
  let p := ({x := 1, y := 2, z := 3, w := 4 : Slots_Point4D} : Obj Point4D)
  return p.cast_up.get_w
-- 4.000000

[Chris Lovett]

Thanks @Kyle Miller, that's impressive. Now I wonder if such a system could be made extensible where one Lean package can add a new subtype. I think that would be hard given the Geo_Type, Geo_Type.Slots and Geo_Type.cast are all fixed in one lean package at compile time. So perhaps lean has no "extensibility by subtyping", only by pre-decided extension hooks, for example, I could add some extension point to my structure as a "bag of properties" and then a 3rd party module can add properties if they want to extend things, my new properties will travel through the system, and when it comes back to me I can find the property I added and part on. Type classes provide a different kind of extensibility since I can add an my own instances (like ToString or Coe), but my understanding is that my new instances cannot influence what previously compiled code is going to do at runtime, it can only influence how my package is going to be compiled, where my new code can pick up my new instances?

[Mario Carneiro]

I don't understand your description but I'm fairly sure there is nothing impossible in this space - some combination of types and typeclasses will do what you want. What is a "bag of properties"? Is that a bunch of functions or a data type?

[Mario Carneiro]

but my understanding is that my new instances cannot influence what previously compiled code is going to do at runtime, it can only influence how my package is going to be compiled, where my new code can pick up my new instances?

If old code takes a typeclass argument, then new code can pass a typeclass instance for that argument to make the old code do new tricks. That's fundamentally the same technique (dynamic dispatch) used to make subclassing work in OO languages

[Chris Lovett]

If old code takes a typeclass argument, then new code can pass a typeclass instance for that argument to make the old code do new tricks

Sounds great, but type classes won't let me write a generic summation of Command.run results that I could extend later:

--------- package I'm importing ----------------
class Command (α: Type)  where
  run : α → Nat

def sumResults (xs : List α) : Nat := Id.run do
  let mut n := 0
  for i in xs do
    n := n + (Command.run i) -- failed to synthesize instance:  Command α
  return n

------------my module----------------

-- teach it a new trick.
instance : Command String where
  run arg := arg.length

#eval sumResults ["hello", "world"]

After defining my instance of course I can run #eval Command.run "hello" -- 5 but this is not the point. I want to use type class instances to teach old compiled code some new tricks, as you say. Do you have a better example?

[Mario Carneiro]

That example is very easy to fix:

--------- package I'm importing ----------------
class Command (α: Type)  where
  run : α → Nat

def sumResults [Command α] (xs : List α) : Nat := Id.run do
  let mut n := 0
  for i in xs do
    n := n + (Command.run i)
  return n

------------my module----------------

-- teach it a new trick.
instance : Command String where
  run arg := arg.length

#eval sumResults ["hello", "world"]

[Mario Carneiro]

the main difference between this and OO polymorphism is that the list still has to be homogeneous when written this way

[Mario Carneiro]

There are ways to make it work in the heterogeneous scenario as well, but this has the advantage that the compiler can actually construct a specialized version of sumResults applied to your Command String instance to avoid the overhead of dynamic dispatch

[Chris Lovett]

Ah, missed the [Command α], thanks. Ok, so yes, this is a kind of polymorphic extensibility I was looking for, thanks for your help. It is the fully generic kind, not the "data extends" kind. The structure "extends" keyword makes an OO person think there's something there, but there isn't really. Moving back to my point example, I would write this:

--------- package I'm importing ----------------
class Vector (α: Type)  where
  length : α → Float

def sumLengths [Vector α] (xs : List α) : Float :=
  xs.foldl (fun sum i => sum + (Vector.length i)) 0

------------ module A with 2D points ----------------

abbrev Point2D := (Float × Float)

-- teach it a new trick with 2D points.
instance : Vector Point2D where
  length v := let (x, y) := v; Float.sqrt (x * x + y * y)

def a : Point2D := (3, 4)

#eval sumLengths [a] -- 5.0

------ another module with 3D points -------

abbrev Point3D := (Float × Float × Float)

-- teach it a new trick with 3D points.
instance : Vector Point3D where
  length v := let (x, y, z) := v; Float.sqrt (x * x + y * y + z * z)

def b : Point3D := (8, 9, 12)

#eval sumLengths [b] -- 17.0

The total abstraction of the data here with α being a Point2D or Point3D and the "vectorization" lens over that data through a Vector interface will take some getting used to. It's not how an OO programmer thinks... it's kind of like the type class and it's instances are manually filling in the slots of a vtable :-) It's definitely more powerful, but it just doesn't feel as simple as the OO combo of subclassing and virtual overriding:

class Vector
{
    public virtual float length { get; }

    public static float sumLengths(IEnumerable<Vector> a)
    {
        return a.Sum(x => x.length);
    }
}

class Vector2D : Vector
{
    public float x;
    public float y;

    public override float length => (float)Math.Sqrt(x * x + y * y);
}

class Vector3D : Vector2D
{
    public float z;

    public override float length => (float)Math.Sqrt(x * x + y * y + z * z);
}

class Program
{
    static void Main()
    {
        var a = new Vector2D() { x = 3, y = 4 };
        Console.WriteLine(Vector.sumLengths(new[] { a })); // 5

        var b = new Vector3D() { x = 8, y = 9, z = 12 };
        Console.WriteLine(Vector.sumLengths(new[] { b })); // 17

        // and the more interesting one...
        Console.WriteLine(Vector.sumLengths(new[] { a, b })); // 22
    }
}

But perhaps simplicity is in the eye of the beholder...

[Mario Carneiro]

The total abstraction of the data here with α being a Point2D or Point3D and the "vectorization" lens over that data through a Vector interface will take some getting used to. It's not how an OO programmer thinks... it's kind of like the type class and it's instances are manually filling in the slots of a vtable :-)

Yes, although if passing typeclasses is actually "manual" you probably aren't doing it right.

[Mario Carneiro]

Here's a transcription of your C# example into lean, including the heterogeneous list example:

class Vector (α : Type) where
  length : α → Float

structure DynVector := (α : Type) [inst : Vector α] (val : α)
attribute [instance] DynVector.inst

instance [Vector α] : Coe α DynVector := ⟨({ val := · })⟩

def sumLengths (xs : List DynVector) : Float :=
  xs.map (Vector.length ·.val) |>.foldl (·+·) 0

structure Vector2D := (x y : Float)

instance : Vector Vector2D where
  length | {x, y} => Float.sqrt (x * x + y * y)

structure Vector3D extends Vector2D := (z : Float)

instance : Vector Vector3D where
  length | {x, y, z} => Float.sqrt (x * x + y * y + z * z)

#eval do
  let a : Vector2D := { x := 3, y := 4 }
  IO.println (sumLengths [a]) -- 5

  let b : Vector3D := { x := 8, y := 9, z := 12 }
  IO.println (sumLengths [b]) -- 17

  IO.println (sumLengths [a, b]) -- 22

[Juan Pablo Romero]

@Mario Carneiro could you explain this bit?

attribute [instance] DynVector.inst

[Mario Carneiro]

When you have a structure with an instance field, it is not marked as an instance by default so you have to do that. That line is equivalent to

instance (self : DynVector) : Vector self.α := self.inst

[Mario Carneiro]

That is, whenever you access something whose type is self.α (like self.val), lean will be able to infer the necessary Vector self.α instance. This is needed to make the sumLengths definition work

[Eric Wieser]

I don't see it mentioned here, but this is_point typeclass vs the Point structure is a lot like how we have docs#monoid_hom vs docs#monoid_hom_class in Lean 3

[Juan Pablo Romero]

Ahh, got it!

[Juan Pablo Romero]

that's pretty neat, an instance that depends on value (a type in this case but it could be any value I guess)

[Juan Pablo Romero]

Interestingly, if the function sumLengths is written this way:

def sumLengths (xs : List DynVector) : Float :=
  (xs.map fun | DynVector.mk v => Vector.length v) |>.foldl (.+.) 0

then the instance declaration is not needed. I guess fun + pattern matching is making the instance available somehow?

[Mario Carneiro]

yes, that pattern match puts the instance in the context as a local variable, and those are always available for typeclass search

[Mario Carneiro]

although it's interesting to me that {val ..} works rather than {val, ..}. I think that's one of those cursed juxtapositions

[Chris Lovett]

@Mario Carneiro your code looks awesome, but I'm struggling with parsing this line:

structure DynVector := (α : Type) [inst : Vector α] (val : α)

This := syntax is not mentioned in https://leanprover.github.io/theorem_proving_in_lean4/structures_and_records.html nor is it mentioned in https://leanprover.github.io/functional_programming_in_lean/getting-to-know/structures.html and nor is it mentioned in https://leanprover.github.io/lean4/doc/struct.html ?

Also, probably related, but what are the parens doing in this expression ⟨({ val := · })⟩ ?

I also like this more compact syntax in the instance declaration length | {x, y} => Float.sqrt (x * x + y * y) instead of my more verbose version: length v := let (x, y) := v; Float.sqrt (x * x + y * y). Where is this vertical bar + curly brace pattern matching described in our documentation so I can read more about this?

[Kyle Miller]

@Chris Lovett That's equivalent to

structure DynVector where
  (α : Type)
  [inst : Vector α]
  (val : α)

It's some Lean 3 syntax that's still in Lean 4.

[Chris Lovett]

Thanks, I wasn't aware you could also use square brackets for a field of a structure, or is that more like an attribute of the field (val : α) saying there is a constraint on the val field that there must be an instance of Vector α ?

[Chris Lovett]

And why can't I write it like this, which is how I see most of the structure examples written (like structure Point in TPIL):

structure DynVector  (α : Type) where
  [inst : Vector α]
  val : α

What does it mean for DynVector to have a field named α ? Looks like it does:

image.png

[Jason Rute]

I assume the alpha is the type parameter. I wonder if that works for inductives too? It is nice since it is mostly by convention that some parameters go inside the structure as fields and others don’t, right? So it is nice to be able to access the ones outside as well.

[Jason Rute]

I guess what is implicitly going on here is that structure definitions are injective maps from their parameters to type, so the inverse map is well defined.

[Mauricio Collares]

I think Jason is talking about the structure DynVector (α : Type) example, not Mario's (please correct me if I'm wrong!). I think the screenshot corresponds to Mario's example, not to the code snippet immediately preceding it (but in theory it could correspond to both, as Jason points out).

The reason α is a field and not a parameter in Mario's example is because we want a single list of type List DynVector to be able to simultaneously contain a Vector2D and a Vector3D (well, a DynVector with α = Vector2D and a DynVector with α = Vector3D). Indeed, such a list can contain elements of any type α as long as Lean is able to find the appropriate Vector α instance by typeclass search (this is represented by the square brackets, which are not an attribute). Had it been declared as structure DynVector (α : Type), a concrete list value would have type List (DynVector α) for some α (that is, the α would be the same for all list elements).

[Chris Lovett]

Ok, so let me know if I'm wrong, but it sounds like this is what is happening in this structure:

structure DynVector where
  α : Type
  [inst : Vector α]
  val : α

We have a field named α that contains a Type so that every item in an List DynVector can have a different type. Then it has another field named inst which is the result of doing a typeclass search for an instance of Vector α, for example, in the case of Vector2D, this inst points to the following?

instance : Vector Vector2D where
  length | {x, y} => Float.sqrt (x * x + y * y)

This inst field works together with attribute [instance] DynVector.inst to tell Lean it has something to do with type class instancing...

Then there is the actual value of type α named val. So DynVector is sort of a dynamic box for any type of Vector, with runtime type info.

Great, now explain to me again what this is doing exactly?

instance [Vector α] : Coe α DynVector := ⟨({ val := · })⟩

Is this the same as writing this?

instance [Vector α] : Coe α DynVector where
  coe s := { val := s }

I find the second version way simpler to read.

[James Gallicchio]

Yup, it's using a new Lean 4 feature for writing simple lambdas. See https://leanprover.github.io/lean4/doc/functions.html#syntax-sugar-for-simple-lambda-expressions

[Chris Lovett]

Thanks and can you explain the role of these 2 sets of brackets: ⟨( ... )⟩ that surround the { val := · } ?

[Chris Lovett]

I understand ⟨ ... ⟩ is invoking a default constructor for something, perhaps a DynVector which the Coe is required to produce, ok, then what about the parens, are those required because it is using lambda sugar syntax and this is what turns the \centerdot into lambda sugar?

[Mario Carneiro]

Yes. The outer angle brackets are constructing a Coe A DynVector from A -> Dynvector, the parentheses are being used with the . to produce a lambda that puts the argument at the location of the ., and the braces are the syntax for building structure instances by naming the fields and inferring the rest (α is inferred by unification and inst is inferred by typeclass inference).

[Mario Carneiro]

the outer brackets could also have been written as { coe := ({ val := · }) }

[Nicolas Rouquette]

@Kyle Miller showed an interesting type class encoding of polymorphism with a function mapping types to types:

def Geo_Type.Slots : Geo_Type → Type
| Point2D => Slots_Point2D
| Point3D => Slots_Point3D
| Point4D => Slots_Point4D
| Square2D => Slots_Square2D

What if I wanted Geo_Type.Slots to give me not just a vanilla Type but something that also has some type class instances as well, e.g. Repr?

For example, I could write:

structure Slots_Point2D where
  (x y : Float)
  deriving Repr

structure Slots_Point3D extends Slots_Point2D where
  z : Float
  deriving Repr

structure Slots_Point4D extends Slots_Point3D where
  w : Float
  deriving Repr

structure Slots_Square2D extends Slots_Point2D where
  width : Float
  deriving Repr

Now, I would like to express the fact that Geo_Type.Slots maps a Geo_Type to a T that has an instance Repr T as well.

Suggestions?

[Horațiu Cheval]

You could use a sigma type.

def Geo_Type.slots : Geo_Type -> Σ T : Type, Repr T
| Point2D => ⟨Slots_Point2D, inferInstance⟩

So you return a pair with the type and the corresponding instance

[Horațiu Cheval]

The problem is that I don't think you can then make that instance synthesized by typeclass inference

[Tomas Skrivan]

Alternative is to define Geo_Type.Slots as abbrev and you get the instances for Slots_Point..

[Yaël Dillies]

The canonical way to do what you want would be to prove the instance (T : Geo_Type) -> Repr T.slots

[Nicolas Rouquette]

@Yaël Dillies Where can I find more about this canonical approach?

I'm getting stuck...

def Geo_Type.Slots : Geo_Type → Type
| Point2D => Slots_Point2D
| Point3D => Slots_Point3D
| Point4D => Slots_Point4D
| Square2D => Slots_Square2D

theorem Geo_Type.Slots.Repr (T : Geo_Type) : Repr T.Slots :=
by
  cases T

Since Geo_Type is an inductive type, cases T splits into subgoals, one for each subtype; e.g.:

case Point2D
⊢ _root_.Repr (Slots Point2D)

It seems that this would require encoding the cases of the function into the proof:

def Geo_Type.Slots : Geo_Type → Type
| Point2D => Slots_Point2D

I am wondering if this requires a different proof strategy or if I am missing something simple.

[Yaël Dillies]

You didn't provide a #mwe, so here's my attempt at one.

structure Slots_Point2D where
  (x y : Float)
  deriving Repr

structure Slots_Point3D extends Slots_Point2D where
  z : Float
  deriving Repr

structure Slots_Point4D extends Slots_Point3D where
  w : Float
  deriving Repr

structure Slots_Square2D extends Slots_Point2D where
  width : Float
  deriving Repr

inductive Geo_Type : Type
| Point2D
| Point3D
| Point4D
| Square2D

def Geo_Type.Slots : Geo_Type → Type
| Point2D => Slots_Point2D
| Point3D => Slots_Point3D
| Point4D => Slots_Point4D
| Square2D => Slots_Square2D

open Geo_Type

instance : (T : Geo_Type) → Repr T.Slots
| Point2D => instReprSlots_Point2D
| Point3D => instReprSlots_Point3D
| Point4D => instReprSlots_Point4D
| Square2D => instReprSlots_Square2D

[Nicolas Rouquette]

Thanks, for an #mwe, here is an adaptation of @Kyle Miller 's example using your trick.

inductive Geo_Type
| Point2D
| Point3D
| Point4D
| Square2D
deriving Repr, DecidableEq

open Geo_Type

structure Slots_Point2D where
  (x y : Float)
  deriving Repr

structure Slots_Point3D extends Slots_Point2D where
  z : Float
  deriving Repr

structure Slots_Point4D extends Slots_Point3D where
  w : Float
  deriving Repr

structure Slots_Square2D extends Slots_Point2D where
  width : Float
  deriving Repr

universe u

def Geo_Type.Slots : Geo_Type → Type
| Point2D => Slots_Point2D
| Point3D => Slots_Point3D
| Point4D => Slots_Point4D
| Square2D => Slots_Square2D

open Geo_Type

def toRepr : (T : Geo_Type) → Repr T.Slots
| Point2D => instReprSlots_Point2D
| Point3D => instReprSlots_Point3D
| Point4D => instReprSlots_Point4D
| Square2D => instReprSlots_Square2D

/-- Get casting function to first type from second type -/
def Geo_Type.cast : (t : Geo_Type) → (t' : Geo_Type) → Option (t'.Slots → t.Slots)
| Point2D, Point2D => some id
| Point2D, Point3D => some (λ x => x.toSlots_Point2D)
| Point3D, Point3D => some id
| Point2D, Point4D => some (λ x => x.toSlots_Point2D)
| Point3D, Point4D => some (λ x => x.toSlots_Point3D)
| Point4D, Point4D => some id
| Point2D, Square2D => some (λ x => x.toSlots_Point2D)
| Square2D, Square2D => some id
| _, _ => none

/-- Whether the second type is a subtype of the first. -/
def Geo_Type.supertype (t t' : Geo_Type) : Bool := (t.cast t').isSome

theorem Geo_Type.supertype.trans (h : Geo_Type.supertype t t') (h' : Geo_Type.supertype t' t'') :
  Geo_Type.supertype t t'' :=
by
  cases t
  all_goals
    cases t'
    all_goals
      cases t''
      all_goals
        simp at h
        try simp at h'
        try simp

def Option.get : (x : Option α) → x.isSome → α
| some v, _ => v
| none, h => by simp [Option.isSome] at h

/-- Get the cast function from a proof that `t'` is a subtype of `t`. -/
def Geo_Type.supertype.cast (h : Geo_Type.supertype t t') : t'.Slots → t.Slots :=
  Option.get (Geo_Type.cast t t') h

/-- Objects of subtype t -/
structure Obj (t : Geo_Type) where
  ty : Geo_Type
  sub : Geo_Type.supertype t ty
  slots : ty.Slots

instance : Coe Slots_Point2D (Obj Point2D) where coe s := ⟨Point2D, rfl, s⟩
instance : Coe Slots_Point3D (Obj Point3D) where coe s := ⟨Point3D, rfl, s⟩
instance : Coe Slots_Point4D (Obj Point4D) where coe s := ⟨Point4D, rfl, s⟩
instance : Coe Slots_Square2D (Obj Square2D) where coe s := ⟨Square2D, rfl, s⟩

/-- Extract the slots from an `Obj`. -/
def Obj.get (o : Obj t) : t.Slots := Geo_Type.supertype.cast o.sub o.slots

/-- Cast up, which can be done statically. -/
def Obj.cast_up (o : Obj t) (h : Geo_Type.supertype t' t := by rfl) : Obj t' where
  ty := o.ty
  sub := Geo_Type.supertype.trans h o.sub
  slots := o.slots

def Obj.can_cast (o : Obj t) (t' : Geo_Type) : Bool := Geo_Type.supertype t' o.ty

/-- Cast up or down using run-time information. -/
def Obj.cast (o : Obj t) (h : o.can_cast t') : Obj t' where
  ty := o.ty
  sub := h
  slots := o.slots

instance : Repr (Obj (T : Geo_Type)) where
  reprPrec o _ := ((instReprGeo_Type.reprPrec o.ty 1).append (Std.Format.text " ")).append ((toRepr o.ty).reprPrec o.slots 1)

def s2: Slots_Point2D := {x := 1, y := 2}
#eval s2

def o2: Obj Point2D := s2
#eval o2

def o3: Obj Point3D := ({x := 1, y := 2, z := 3}: Slots_Point3D)
#eval o3
#eval o3.get
#eval o3.slots
#eval o3.slots.x
#eval o3.slots.y
#eval o3.slots.z

def o4: Obj Point4D := ({x := 1, y := 2, z := 3, w := 4}: Slots_Point4D)
#eval o4
#eval o4.get.w
-- 4.000000

def o43: Obj Point3D := o4.cast_up
#eval o43
#eval o43.slots.w
-- 4.000000
#eval o43.get.w
-- invalid field 'w', the environment does not contain 'O41.Geo_Type.Slots.w'
--  Obj.get o43
-- has type
--  Slots Point3D

The interesting behavior here is in the difference between o43.get.w vs. o43.slots.w.

Is there a way to write Geo_Type.toRepr without depending on Repr instance names?

[Yaël Dillies]

I would say by unfold Geo_Type.Slots; apply_instance, but I haven't tried it.

[Nicolas Rouquette]

Hum, I get a message that apply_instance is an unknown tactic.

I made a smaller example to focus on the problem:

inductive Geo_Type
| Point2D
| Point3D
deriving Repr, DecidableEq

open Geo_Type

structure Slots_Point2D where
  (x y : Float)
  deriving Repr

structure Slots_Point3D extends Slots_Point2D where
  z : Float
  deriving Repr


def Geo_Type.Slots : Geo_Type → Type
| Point2D => Slots_Point2D
| Point3D => Slots_Point3D

open Geo_Type

-- Q: how to avoid depending on generated instance names?
-- def toRepr : (T : Geo_Type) → Repr T.Slots
-- | Point2D => instReprSlots_Point2D
-- | Point3D => instReprSlots_Point3D

-- def toRepr : (T : Geo_Type) → Repr T.Slots :=
-- by {
--   unfold Slots <;>
--  apply_instance
--   -- unknown tactic
-- }

def toRepr : (T : Geo_Type) → Repr T.Slots :=
by {
  intro T;
  cases T <;>
  unfold Slots <;>
  simp <;>
  sorry
}

/-- Get casting function to first type from second type -/
def Geo_Type.cast : (t : Geo_Type) → (t' : Geo_Type) → Option (t'.Slots → t.Slots)
| Point2D, Point2D => some id
| Point2D, Point3D => some (λ x => x.toSlots_Point2D)
| Point3D, Point3D => some id
| _, _ => none

/-- Whether the second type is a subtype of the first. -/
def Geo_Type.supertype (t t' : Geo_Type) : Bool := (t.cast t').isSome


/-- Objects of subtype t -/
structure Obj (t : Geo_Type) where
  ty : Geo_Type
  sub : Geo_Type.supertype t ty
  slots : ty.Slots

instance : Coe Slots_Point2D (Obj Point2D) where coe s := ⟨Point2D, rfl, s⟩
instance : Coe Slots_Point3D (Obj Point3D) where coe s := ⟨Point3D, rfl, s⟩

instance : Repr (Obj (T : Geo_Type)) where
  reprPrec o _ := ((instReprGeo_Type.reprPrec o.ty 1).append (Std.Format.text " ")).append ((toRepr o.ty).reprPrec o.slots 1)

def s2: Slots_Point2D := {x := 1, y := 2}
#eval s2

def o2: Obj Point2D := s2
#eval o2

The last toRepr is unfinished; the tactic state before sorryis:

case Point2D
⊢ Repr Slots_Point2D
case Point3D
⊢ Repr Slots_Point3D

I don't understand why some tactics are available in some contexts but not others.
Is there a way to ask Lean what tactics are available ? VS Code completion gives me a bunch of options that seem to reflect my editor history more than a genuine query.

[Nicolas Rouquette]

Hum... I managed to get this to work:

instance p2 : Repr Slots_Point2D := inferInstance
instance p3 : Repr Slots_Point3D := inferInstance

def toRepr : (T : Geo_Type) → Repr T.Slots :=
by {
  intro T;
  cases T <;>
  unfold Slots <;>
  simp
  apply p2
  apply p3
}

We could have used this for your earlier suggestion:

instance p2 : Repr Slots_Point2D := inferInstance
instance p3 : Repr Slots_Point3D := inferInstance

def toRepr : (T : Geo_Type) → Repr T.Slots
| Point2D => p2
| Point3D => p3

Is there a way to inline the instance inference into the corresponding case?

[Nicolas Rouquette]

Ah... I figured it out!

def toRepr : (T : Geo_Type) → Repr T.Slots :=
by {
  intro T;
  cases T <;>
  unfold Slots <;>
  simp <;>
  infer_instance
}

This kind of programming is magical!

[Yaël Dillies]

Ah, infer_instance was underused in Lean 3 and doing the same thing as apply_instance but as a term, so I assumed we'd kept apply_instance and ditched infer_instance. But apparently it happened the other way around.