Finding an abstract type in a heterogeneous list

Stream: new members

[misterdrgn]

I appreciate how helpful the community has been with beginner questions. I have yet another one. This question is a bit more open-ended, as I'm really not sure where to begin. Suppose I set up a heterogeneous list as follows.

structure Point where
  x : Int
  y : Int
deriving Repr

structure Size where
  width : Int
  height : Int
deriving Repr

structure Rect where
  x : Int
  y : Int
  width : Int
  height : Int
deriving Repr

inductive Element where
  | point (data : Point) : Element
  | size (data: Size) : Element
  | rect (data : Rect) : Element

-- Example of a heterogeneous List Element
def elems := [Element.point {x := 0, y := 0}, Element.rect {x := 0, y := 0, width := 0, height := 0}]

I can now write a function that filters a List Element to find, for example, all the points.

def getPoints (elems: List Element) : List Point :=
  let toPoint (elem: Element) : Option Point :=
    if let .point point := elem then
      some point
    else
      none

  elems.filterMap toPoint

But suppose I want to do something more abstract. I want to filter a heterogeneous list to find all the elements that have x and y fields. I can set up a type class for this property, as described below, but could anyone suggest a way to look through a list and find all the elements that satisfy this type class, returning a list of elements that are guaranteed to have x and y values? Thanks.

class Locatable (α : Type) where
  x: α → Int
  y: α → Int

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

instance : Locatable Rect where
  x := Rect.x
  y := Rect.y

[Eric Wieser]

but could anyone suggest a way to look through a list

Can you say what type you intend said List to have? Are you still using List Element?

[Matt Diamond]

I'm getting the sense that @misterdrgn is trying to do structural typing, but Lean's type system is nominal

[Matt Diamond]

for example, the Locatable classes don't actually add any new data/props, they merely re-use existing fields... I don't think that's typical of the way Lean uses typeclasses

[Matt Diamond]

I could provide a Locatable instance for Size:

instance : Locatable Size where
  x _ := 0
  y _ := 0

of course that would be stupid, but the point is that Locatable doesn't provide any guarantees about the fields on the original structure

[Matt Diamond]

(maybe this is irrelevant to the problem at hand... I just think there might be some conceptual confusion here that could lead to issues down the road)

[misterdrgn]

Eric Wieser said:

Can you say what type you intend said List to have? Are you still using List Element?

Yeah, that's kind of the question. I've long wondered about the best way to capture this functionality that my research group uses in our AI (not machine learning) framework, which was originally in Clojure, and then I later ported it to Swift. Of course, those languages are very different. Clojure allows you to stick whatever you want in a hashmap, and Swift allows you to upcast and downcast freely. So in Swift, you could have Point and Rect as structs, and then they both conform to the Locatable protocol, and then everything conforms to the Element protocol (swift protocols are type classes without higher-kinded types, if you're unfamiliar). So you can start with an array of Element, and then downcast to an array of Locatable (filtering out the things that don't conform to Locatable), and you can interact with the Locatables and get their x and y values, and then you could later downcast to an array of Point (again, filtering out the things that aren't Point).

When I first looked at Lean maybe 6 months back, I tried to do something similar with downcasting, but it was tricky. It seems like the correct way to handle heterogeneous lists in many languages is to use enums, or in lean inductive types. Those make it easy to go from Element to Point, but I don't know how to get to the intermediate Locatable type.

One way to do it is to nest the types. Something like the following:

structure Locatable where
  x: Int
  y: Int
  data: Located

inductive Located where
  | point (data : Point) : Located
  | rect (data : Rect) : Located

But this doesn't seem ideal because when you've unwrapped everything down to Point or Rect, you've lost the x and y fields that are represented up at the Locatable level.

[misterdrgn]

Oh, another approach is to make Locatable a separate struct that just has x and y fields, and then have a way to convert some types to Locatable.

And then you could write a version of the getPoints function I defined above that's getLocatables, and it gets all the types that can be converted to Locatable and converts them. A couple downsides are:
1) There's no way to downcast further. That is, you can't convert a Locatable back to a Point. But that might be okay for present purposes.
2) I suspect the getLocatables function would have to reference every type that can be converted to Locatable explicitly, which means you'd have to modify the function whenever you add a new type.

[Eric Wieser]

Does this help you?

structure Point where
  x : Int
  y : Int
deriving Repr

structure Size where
  width : Int
  height : Int
deriving Repr

structure Rect where
  x : Int
  y : Int
  width : Int
  height : Int
deriving Repr


class Locatable (α : Type) where
  x : α → Int
  y : α → Int

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

instance : Locatable Rect where
  x := Rect.x
  y := Rect.y

structure AbstractLocatable where
  {α : Type}
  [locatable : Locatable α]
  val : α

-- Example of a heterogeneous List Element
def elems : List (AbstractLocatable) := [⟨{x := 0, y := 0 : Point}⟩, ⟨{ x := 0, y := 0, width := 0, height := 0 : Rect}⟩]

[Matt Diamond]

what about using inheritance?

structure Locatable where
  x : Int
  y : Int
deriving Repr

structure Size where
  width : Int
  height : Int
deriving Repr

structure Rect extends Locatable, Size
deriving Repr

structure Point extends Locatable
deriving Repr

inductive Element where
  | point (data : Point) : Element
  | size (data: Size) : Element
  | rect (data : Rect) : Element

[misterdrgn]

@Eric Wieser Thanks for the suggestion. This is actually close to the original approach I tried several months ago. The idea was to encode both the original data (e.g., x and y values) and the original type (e.g., Point) in a generic struct, so that these could be recovered later. However, in practice recovering the original types was difficult because Lean4, like many statically typed languages (but unlike Swift and I think Scala), doesn't keep type information at runtime. If you know of a good way to take yourList AbstractLocation and convert that back to a List Point, removing all the values that can't be downcast to Point, I'd be very interested.

[misterdrgn]

@Matt Diamond Wow, somehow I missed that extending structs was even a thing. I can see where that would be convenient, but my question is the same as above. In fact, a quick look at the functional programming in lean4 book indicates that once you upcast a Point to a Locatable, there's no way to recover the original Point. So you can upcast but not downcast.

Thanks for the suggestion.

[Aaron Liu]

You could bundle a toPoint? field into all the elements of the list

[pandaman]

I think what you want is the ability to downcast like Rust's Any::downcast_ref. One possible implementation to assign a unique ID to each type (such as the type's name represented as Lean.Name), and use that information to implement the downcast.

Unfortunately, it's possible that Nat = Int in Lean via a so-called cardinality model, so I think it's not possible to assign such an ID to every type within Lean's logic. I guess we need an unsafe (or at least opaque) definition to handle the ID assignment.

[Mario Carneiro]

misterdrgn said:

@Matt Diamond Wow, somehow I missed that extending structs was even a thing. I can see where that would be convenient, but my question is the same as above. In fact, a quick look at the functional programming in lean4 book indicates that once you upcast a Point to a Locatable, there's no way to recover the original Point. So you can upcast but not downcast.

Just to temper your expectations here, lean doesn't have subtyping. When you extend a structure it's just sugar for declaring a structure with a field whose type is the parent (aka "composition over inheritance"). The "upcast" isn't really a cast, it's just a field projection

[misterdrgn]

Mario Carneiro said:

Just to temper your expectations here, lean doesn't have subtyping. When you extend a structure it's just sugar for declaring a structure with a field whose type is the parent (aka "composition over inheritance"). The "upcast" isn't really a cast, it's just a field projection

Yeah, understood. Go does something similar, though it looks like Lean does it better. If I was looking for OOP, I'd look elsewhere.

[Mario Carneiro]

The equivalent of Rust Any is docs#Dynamic, where Any::downcast_ref becomes docs#Dynamic.get? . But it's an opaque function, so you won't be able to prove theorems using this method

[Mario Carneiro]

The usual approach here is to just use the "universe pattern" and make an inductive type containing all of your types of interest, as you have done. The typeclass becomes a red herring then, you can just write

def getLocatable (elems: List Element) : List Point :=
  elems.filterMap fun
    | .point {x, y}
    | .rect {x, y, ..} => some {x, y}
    | _ => none

[Mario Carneiro]

But if you wanted to generalize this over different types replacing Element, you can build the function out of typeclasses:

class MaybeLocatable (α : Type) where
  pt: α → Option Point

instance (priority := low) (α) : MaybeLocatable α where -- default instance
  pt _ := none

instance : MaybeLocatable Point where
  pt a := some a

instance : MaybeLocatable Rect where
  pt | {x,y,..} => some {x,y}

instance : MaybeLocatable Element where
  pt
  | .point a
  | .rect a
  | .size a => MaybeLocatable.pt a

def getLocatable (elems: List Element) : List Point :=
  elems.filterMap MaybeLocatable.pt