question about monad type inference

Stream: lean4

[Chris Lovett]

Can someone explain how these 2 type instances interact exactly?

instance {ε : Type u} {m : Type u → Type v}  [Monad m] : Monad (ExceptT ε m) where
  pure := ExceptT.pure
  bind := ExceptT.bind
  map  := ExceptT.map

instance : Monad (Except ε) where
  pure := Except.pure
  bind := Except.bind
  map  := Except.map

When I create ExceptT String Id it must be triggering the first instance and when I use Except String it must be triggering the second. But where my brain is exploding is when I realize the fact that logically in a type reduction kind of way ExceptT String Id is equal to Except String:

#reduce ExceptT String Id -- Except String α

So how does lean decide which of the above instances to use? Are there multiple phases of type inferencing or something, one that operates on non-reduced types and another that operates on reduced types, or does type inference never operate on reduced types? Or is the fact that I have to write the first instance above a kind of hack working around limitations in lean compiler? Or is the fact that I CAN write the first instance and redirect all the type inferencing to ExceptT.pure and ExceptT.bind and ExceptT.map a feature of Lean, it allows me to catch things before any kind of type resolution/reduction and change the game... ? How should I think about this...?

[Mario Carneiro]

One important thing that affects the answer to this question is whether ExceptT and/or Except is defined to be an abbrev of the other

[Chris Lovett]

They are not, I'd assume abbreviations would be transparent to all this, and that I would not be able to create an instance that does one thing for the abbreviated type and something different for the abbreviation?

[Mario Carneiro]

Since they are not abbreviations, they act essentially as completely different types for the purpose of type class inference. If you infer the monad instance of an ExceptT you get the ExceptT instance and if you infer Except you get the Except instance

[Chris Lovett]

So this is because ExceptT is a def instead of an abbrev ?

[Mario Carneiro]

If they were abbreviations, then the two type class instances would be overlapping, and you may get one or the other depending on which one is declared first / with higher priority, or perhaps only one applies in a particular case. Lean does not attempt to prevent overlapping instances from being declared, although they are generally a bad idea

[Chris Lovett]

So type inference happens before any type resolution (computation, reduction, elaboration? whatever the right term is)...

[Mario Carneiro]

for instance you could declare instance : Monad (Except String) and that would get picked up in preference to the instance : Monad (Except ε) if you declared it afterward

[Chris Lovett]

That helps - thanks.

[Mario Carneiro]

Chris Lovett said:

So type inference happens before any type resolution (computation, reduction, elaboration? whatever the right term is)...

No, everything is kind of interdependent

[Mario Carneiro]

it's all part of elaboration

[Chris Lovett]

I just tried abbreviations, and they work too ...

class MyMath (a : Type) where
  plus : a -> a -> a

instance : MyMath Nat where
  plus := Nat.add

def doubleIt [MyMath a] (x : a) : a :=
  MyMath.plus x x

#eval doubleIt 5 - 10

abbrev Foo := MyMath

instance : Foo Nat where
  plus := Nat.mul -- <<< redurect to multiply!

open MyMath

def fooIt [Foo a] (x : a) : a :=
  plus x x

#eval fooIt 5 -- 25

[Mario Carneiro]

Note that reduction in the sense of #reduce is not something that lean does at all during elaboration

[Mario Carneiro]

it will do some limited reduction when needed to fix type errors

[Mario Carneiro]

like if you have a function that accepts a ExceptT and you give it Except then it will unfold stuff to try to resolve that

[Mario Carneiro]

but inferType generally doesn't unfold anything unless it is forced to, so the ExceptT definition will stay fairly stable and typeclass inference is predictable on it

[Chris Lovett]

So unfold is the term I was looking for thanks... In other languages I always think about type equivalence. Seems in Lean I have to forget about that and take Type expressions more literally...

[Mario Carneiro]

your example plus := Nat.mul is showing lean doing unfolding to fix what would otherwise be a type error

[Mario Carneiro]

yeah, def is not like a type alias

[Mario Carneiro]

abbrev is closer to a type alias and notation is closer still

[Chris Lovett]

Tell me more about why plus in my Foo instance would be a type error?

[Mario Carneiro]

ah, actually there isn't any unfolding needed there

[Mario Carneiro]

it does have to unfold Foo to see why where plus := ... is a proof of it

[Mario Carneiro]

that is, to uncover that Foo is actually the class MyMath with field plus

[Chris Lovett]

Sure. But you can see from my example that you can even specify more specific type instances on abbreviations! (so why did you ask about abbreviations earlier?)

[Mario Carneiro]

Here's a better example:

class MyMath (a : Type) where
  plus : a -> a -> a

def Foo := Nat

instance : MyMath Nat where
  plus := Nat.mul

open MyMath

def fooIt [MyMath a] (x : a) : a :=
  plus x x

def five : Foo := (5 : Nat)

#eval fooIt 5 -- 25
#eval fooIt five -- failed

[Mario Carneiro]

If you change Foo to an abbrev then the second eval works

[Mario Carneiro]

and the definition of five also doesn't need the type ascription

[Chris Lovett]

Very good, so can I conclude from your example that type inference does not unfold defs.

[Mario Carneiro]

Here's another fun example:

class IsFoo (a : Type) where
  isFoo : Bool
open IsFoo
def Foo := Nat

instance : IsFoo Nat := ⟨false⟩
instance : IsFoo Foo := ⟨true⟩

#eval isFoo Nat -- false
#eval isFoo Foo -- true

example : Nat = Foo := rfl
example : isFoo Nat ≠ isFoo Foo := by decide

[Chris Lovett]

Interesting I also cannot use a def in square brackets, this fails:

def Foo := MyMath
def fooIt [Foo a]...          -- invalid binder annotation, type is not a class instance

[Mario Carneiro]

You can only use something which is a class (up to unfolding reducible definitions) in instance brackets

[Mario Carneiro]

well, it's just a lint, you can turn it off if you want to but instances that don't have class type can never be inferred

[Chris Lovett]

Ha, so this works, ok, thanks:

@[reducible]
def Foo := MyMath

So I wonder if the ExceptT instance exists mostly because def ExceptT is not reducible... but there seems to be some other minor differences in it's implementation, using pure more often... but otherwise looks very similar, almost like a shadow hierarchy. I wonder if monad transformers have this shadow instancing going on in general...

[Mario Carneiro]

yes, many defs will inherit their instances from the underlying definition. Just search for uses of inferInstanceAs

[Mario Carneiro]

Not always though: in fact one of the reasons to use a def on types is to equip a type with a non-standard instance

[Mario Carneiro]

for example mathlib has the with_top A type that is a wrapper around option A with an ordering that puts none as the greatest element, and another with_bot A type that is also option A but puts none at the bottom instead

[Mario Carneiro]

if those were abbrevs then it would be very confusing since you might get the with_top order on with_bot and vice versa

[Mario Carneiro]

In your example though I wouldn't expect ExceptT and Except to have the same monad instance: ExceptT is wrapping another monad so it has to call the operations for that monad too

[Chris Lovett]

OOooh, yes I see now that abbrev is dangerous, it also changed my original #eval doubleIt 5 -- 25 !! So my second instance operating on Foo was not operating on Foo it was operating on MyMath, changing the behavior of the earlier instance! Wow yes this could lead to all kinds of trouble... and this is also the case with the @[reducible] def Foo, so def here didn't help me.

[Mario Carneiro]

yes, abbrev is just a shorthand for @[reducible, inline] def IIRC

[Mario Carneiro]

the important thing is the reducibility setting: reducible for abbrevs, semireducible for regular defs and irreducible for... @[irreducible] def

[Mario Carneiro]

irreducible defs won't be unfolded by normal elaboration / unification, but you can explicitly unfold it by calling the unfold tactic

[Mario Carneiro]

and then opaque is the most irreducible: even the kernel doesn't think that the opaque definition unfolds, only the compiler will use the equation when generating code

[Chris Lovett]

So back to my earlier question, even though this is true:

example : ExceptT α Id = Except α :=
  by simp[ExceptT, Except, Id] -- Goals accomplished 🎉

it has no bearing on how type inference works, since type inference doesn't care about type equivalence...

[Mario Carneiro]

it cares about definitional equality up to unfolding reducibles

[Mario Carneiro]

which is the "weakest" kind of unfolding, which you will see in most things that want to be mostly syntactic

[Mario Carneiro]

rw and simp match up to reducible defs too

[Chris Lovett]

Thanks, this info seems to be missing from: https://leanprover.github.io/theorem_proving_in_lean4/type_classes.html

[Mario Carneiro]

Indeed, abbrev isn't mentioned in the book at all. This is reasonable considering that it didn't exist in lean 3 when TPIL was first written, and it was merely syntax-upgraded to lean 4 IIUC