Inheritance question

Stream: lean4

[Patrick Massot]

I have a very basic question but I'm not sure about the idiomatic solution. Maybe I'm too much used to python, but I want to be able to write a function taking as argument any object inheriting from some basic class. Ideally I would like to write

structure Enough where
  x : Nat
  y : Nat

and then define a function

def getX {α : Type _} "some way to state that α is a structure extending Enough" (a : α) : Nat := a.x

That could be applied to x : Extra where

structure Extra where
  x : Nat
  y : Nat
  z : Nat

I know I can use

class Enough (α : Type) where
  x : α → Nat
  y : α → Nat

def getX [Enough α] (a : α) : Nat := Enough.x a

structure Extra where
  x : Nat
  y : Nat
  z : Nat

instance : Enough (Extra) where
  x := Extra.x
  y := Extra.y

#eval getX (Extra.mk 1 2 3)

But this doesn't feel right. What am I missing?

[Eric Wieser]

I think that's the idiomatic solution, as it's what we use to generalize over subobjects and morphisms

[Eric Wieser]

What you (and everyone else) are missing is automation to build this automatically

[Eric Wieser]

Your alternative is to exploit dot notation "seeing through" extends:

structure Enough where
  x : Nat
  y : Nat

def Enough.getX (a : Enough) : Nat := a.x

structure Extra extends Enough where
  z : Nat

#eval ({x := 1, y := 2, z := 3} : Extra).getX

[Patrick Massot]

Yes, this is inspired by what we do in algebraic situations, but somehow it feels weirder when Extra has no parameter at all.

[Eric Wieser]

These correspond roughly to what C++ calls dynamic polymorphism and static polymorphism, respectively

[Eric Wieser]

I'm curious how Rust and Haskell solve this

[Patrick Massot]

I have a hard time deciding whether I should use the dot notation trick. It really feels dirty.

[Eric Wieser]

It also breaks Extra.mk 1 2 3, though you can fix that by writing Extra.mk {} 1 2 3 and using the FlatHack trick from my CICM paper

[Patrick Massot]

Currently in my code I use the solution I showed at the beginning of this thread, with a ugly derive handler.

[Patrick Massot]

And I really mean ugly: https://github.com/leanprover-community/mathlib4/blob/pm_widgets/Mathlib/Tactic/Widget/SelectInsertParamsClass.lean

[Patrick Massot]

It does the job at https://github.com/leanprover-community/mathlib4/blob/pm_widgets/Mathlib/Tactic/Widget/Calc.lean#L50-L54 but don't dare PRing this.

[Eric Wieser]

What's the getX in your application?

[Eric Wieser]

Eric Wieser said:

I'm curious how Rust and Haskell solve this

It looks like Rust does the same thing as what you did above (their trait is our class/instance)

[Patrick Massot]

Eric Wieser said:

What's the getX in your application?

There are simply the fields of SelectInsertParamsClass.

[Patrick Massot]

So my example would be closer to my actual code as:

class Enough (α : Type) where
  x : α → Nat
  y : α → Nat

structure Extra where
  x : Nat
  y : Nat
  z : Nat

instance : Enough (Extra) where
  x := Extra.x
  y := Extra.y

#eval Enough.x (Extra.mk 1 2 3)

[Patrick Massot]

I think the dot notation trick doesn't work anyway, it does not allow to assign a type to functions that would need to use this trick.

[James Gallicchio]

I think extends generates a Coe instance, doesn't it? Could you use Coe A Enough?

[Eric Wieser]

I think the dot notation trick doesn't work anyway, it does not allow to assign a type to functions that would need to use this trick.

These functions would just consume an Enough (the base structure)

[Matthew Ballard]

I would have reached for a coercion first also

[Patrick Massot]

Eric Wieser said:

I think the dot notation trick doesn't work anyway, it does not allow to assign a type to functions that would need to use this trick.

These functions would just consume an Enough (the base structure)

I need them to consume more general arguments, otherwise there would be no discussion.

[Eric Wieser]

You could also consider

def Enough where
  x : Nat
  y : Nat

class ToEnough (α : Type) where
  toEnough : α → Enough

structure Extra where
  x : Nat
  y : Nat
  z : Nat

instance : Enough (Extra) where
  toEnough e := { e with }

#eval Enough.x (ToEnough.toEnough <| Extra.mk 1 2 3)

[Patrick Massot]

Indeed that also works, but still feels clunky (and requires a derive handler too).

[James Gallicchio]

James Gallicchio said:

I think extends generates a Coe instance, doesn't it? Could you use Coe A Enough?

maybe it should autogenerate a Coe instance...... but that's something that would require core changes, I assume

[Eric Wieser]

I don't think automatic generation of Coe is a good idea

[James Gallicchio]

Then a To A B class that is isomorphic to Coe B A but without the transitivity and notational baggage :)