Puzzling type class behavior

Stream: lean4

[Scott N. Walck]

Hi Folks,

I'm trying to make a type class for numbers that can be added,
subtracted, multiplied, divided, and a few other things.

I thought I had succeeded, but the following inverse function is
not behaving as I had expected. I thought that when I use Float
as the particular type, then the division that occurs in the
inverse function would be floating point division. But since the
inverse of ten evaluates to zero, I'm thinking that maybe Lean is
doing Nat division for some reason and only subsequently
converting the result to a Float.

Can someone explain this behavior?

Thanks.

class Number (n : Type) extends Add n, Sub n, Mul n, Div n, Neg n,
  OfNat n 0, OfNat n 1, OfNat n 2, OfNat n 6 where

def inv [Number n] (x : n) : n := (1 : n) / x

instance : Number Float where

def ten : Float := 10

#eval inv ten    -- 0.000000, why?

[Kevin Buzzard]

Can you post a #mwe ? Your question is very hard to answer coherently otherwise [edit: thanks for editing the question :-) ]

[Timo Carlin-Burns]

(It looks like the beginning got chopped off in a copy-paste)

[Timo Carlin-Burns]

Lean has some counterintuitive behavior when you extend multiple structures which have projections with the same name. Here Number extends both OfNat n 0 and OfNat n 1, both of which have a projection ofNat, and only the OfNat n 0 ends up counting. You can see that (1 : n) is actually getting defined as (0 : n) through this example:

class Number (T : Type) extends OfNat T 0, OfNat T 1

instance : Number Float where

def Number.one {T : Type} [Number T] : T := 1

#eval (Number.one : Float) -- 0.000000

[Timo Carlin-Burns]

The way mathlib works around this is that they define two classes docs#Zero and docs#One which each have bidirectional instances with OfNat and docs#AddMonoidWithOne extends Zero T and One T instead of OfNat T 0 and OfNat T 1. You could do the same except have classes for Zero, One, Two, and Six.

[Scott N. Walck]

Wow. That's very helpful. Thanks.

[Eric Wieser]

This feels like a bug to me; it seems like Lean should refuse to merge base classes which have different types

[Floris van Doorn]

This also feels counterintuitive to me. But what exactly are you suggesting @Eric Wieser? @OfNat.ofNat T 0 _ and @OfNat.ofNat T 1 _ both have type T, and I'm not quite sure in what way this example is different to merging the mul fields when extending CommSemigroup and Monoid.

[Eric Wieser]

In that case the two base classes are both of type Mul

[Eric Wieser]

The one place that we might run into trouble here is with the dependently-typed base classes of Module, but I think that's easiest to answer by implementing and seeing what breaks

[Eric Wieser]

I guess this would be a breaking change; field unification would no longer be nominal, and would only happen via explicit diamond inheritance

[Floris van Doorn]

I expect there are some explicit fields (i.e. not through extend) in our algebraic hierarchy with the same name and type? And those would indeed break under your suggestion... But maybe that isn't too painful...

[Eric Wieser]

I guess this rule only needs to apply for data fields, prop fields can always be merged

[Timo Carlin-Burns]

So the desired behavior is that extending both OfNat T 0 and OfNat T 1 results in @[instance] fields toOfNat : OfNat T 0 and toOfNat_0 : OfNat T 1?

[Timo Carlin-Burns]

Making the field names unique seems a little awkward. I wonder if the new instance naming algorithm could be reused

[Kyle Miller]

At least you can always give your own names outside of extend, at the cost of needing to define the projection instances yourself. You do lose default values from pre-existing instances, but you can use autoParams as a hack:

class Number (n : Type) extends Add n, Sub n, Mul n, Div n, Neg n where
  (zero : n := by exact 0)
  (one : n := by exact 1)
  (two : n := by exact 2)
  (six : n := by exact 6)

instance (n : Type) [Number n] : OfNat n 0 := ⟨Number.zero⟩
instance (n : Type) [Number n] : OfNat n 1 := ⟨Number.one⟩
instance (n : Type) [Number n] : OfNat n 2 := ⟨Number.two⟩
instance (n : Type) [Number n] : OfNat n 6 := ⟨Number.six⟩

def inv {n : Type} [Number n] (x : n) : n := (1 : n) / x

instance : Number Float where

def ten : Float := 10

#eval inv ten
-- 0.100000

[Kyle Miller]

Making the field names unique seems a little awkward. I wonder if the new instance naming algorithm could be reused

Name mangling is an option, but a problem here is that these names need to be used in user code when defining instances (unless there is an expectation that these fields must come from preexisting instances).

Lean 3 had a feature where you could rename fields when you extended.

[Kyle Miller]

Oh right, I forgot about this design pattern, where you use encapsulation instead of extension:

class Number (n : Type) extends Add n, Sub n, Mul n, Div n, Neg n where
  [ofNatZero : OfNat n 0]
  [ofNatOne : OfNat n 1]
  [ofNatTwo : OfNat n 2]
  [ofNatSix : OfNat n 6]

instance (n : Type) [Number n] : OfNat n 0 := Number.ofNatZero
instance (n : Type) [Number n] : OfNat n 1 := Number.ofNatOne
instance (n : Type) [Number n] : OfNat n 2 := Number.ofNatTwo
instance (n : Type) [Number n] : OfNat n 6 := Number.ofNatSix

def inv {n : Type} [Number n] (x : n) : n := (1 : n) / x

instance : Number Float where

def ten : Float := 10

#eval inv ten
-- 0.100000

[Kyle Miller]

I wonder if the class command could have a way to say that certain fields are supposed to provide instances, to save needing to write these instance commands?

[Timo Carlin-Burns]

Is it accurate to say that this is exactly what extend desugars to, at least when the base structures have mutually exclusive fields? As long as we're not losing any special affordances that come from using extend, I think it would be a reasonable design to say that you must use this manual desugaring when you're extending distinct base structures which share a field with the same name. The nice thing about the desugared syntax is that it provides a natural way to specify the projection names.

[Timo Carlin-Burns]

Kyle Miller said:

I wonder if the class command could have a way to say that certain fields are supposed to provide instances, to save needing to write these instance commands?

Should we just make it the default that instance implicit class fields get projection instances automatically? I can't think of a reason you wouldn't want that, and if you really didn't, you could always get around it using class inductive

[Eric Wieser]

I think attribute [instance] Number.ofNatZero is the currently-idiomatic spelling?

[Robert Maxton]

Timo Carlin-Burns said:

Should we just make it the default that instance implicit class fields get projection instances automatically? I can't think of a reason you wouldn't want that, and if you really didn't, you could always get around it using class inductive

If we do get this, docs#CategoryTheory.Bundled would be a great first test subject, using it becomes nontrivially more convenient with an auto-instance for c.str.