What is the benefit of `Id` over `id`?

Stream: new members

[Vilim Lendvaj]

For example, I can do this

universe u v

instance : Monad id where
  map := id
  pure := id
  bind := flip id

@[inline] def id.run {α : Sort u} : id α -> α := id

def containsFive (xs : List Nat) : Bool := id.run do
  for x in xs do
    if x == 5 then return true
  return false

def Array.foldr' {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Array α) (start := as.size) (stop := 0) : β :=
  as.foldrM (m := id) f init start stop

I don't see where the problems would start. What am I missing?

[Aaron Liu]

the docs#id_eq is a simp lemma

[Eric Wieser]

The answer to this question belongs in docs#Id if it is not already there

[Vilim Lendvaj]

Aaron Liu said:

the docs#id_eq is a simp lemma

I'm sorry, but I don't understand how this relates to my question. Could you explain in more detail? I'm still new to Lean.
Are you saying I should use (id_eq _).mp instead of defining id.run?

Eric Wieser said:

The answer to this question belongs in docs#Id if it is not already there

It is not, or at least I didn't understand it from it. In my original post I rewrote the example from there using id instead of Id.

[Eric Wieser]

@Aaron Liu's point is that id Nat will simplify to Nat, at which point it will have no monad instance. Id Nat doesn't simplify, so will continue to have a monad instance.

[Aaron Liu]

The answer is that you can't use simp anymore now since it will just simplify away all your occurrences of id

[Vilim Lendvaj]

But wouldn't it be easy to reintroduce it?

[Vilim Lendvaj]

I guess I'll try to fork and replace Id with id in the whole library to see how bad it would actually be

[Aaron Liu]

we have docs#Id.run_pure, docs#Id.run_map, docs#Id.run_bind

[Aaron Liu]

simp will only use those if it sees a term of type Id _

[Aaron Liu]

you can't do those with id _ since it'll get simplified away

[Vilim Lendvaj]

But if id gets simplified away, there's no need for those three theorems in the first place, since they hold trivially by simplification. Right?

[Aaron Liu]

no?

[Aaron Liu]

the id gets simplified away but the id.run and the Bind.bind are still there

[Eric Rodriguez]

If you see in docs#Id, there's some instances; these allow the monadic notation that is described above. In order to apply instances like this, Lean needs a symbol to match against. id would work, but generally we want to remove all uses of id possible via simplification; this is _not_ the behaviour we want in this case. So we must make a separate symbol

[Vilim Lendvaj]

https://github.com/viliml/lean4/commit/963ece083e028587a522785fd1dbf113b2a13d54
I had to add a negative simp lemma in one place. Otherwise, everything just works.

[Vilim Lendvaj]

I managed to remove a lot of the pure/run wrappers and it's much cleaner now.
It's a shame how even though Lean actually has real type functions (unlike Haskell), the identity monad is still the equivalent of a "newtype" instead of utilizing that feature.
Maybe something to keep in mind for version 5.

[Eric Wieser]

The whole point of the run wrappers is to allow you to explicitly hop in and out of the monadic abstraction

[Vilim Lendvaj]

Why does it need to be explicit? "monadic" computations in the identity monad are just regular values. Are you saying that fun x => f x.run and (pure <| f . . .) are clearer and better code style than f?

[Aaron Liu]

It's so that automation can recognize when you're in the id monad and it's also so you can recognize when you're in the id monad

[Eric Wieser]

I'll also note that the change you propose amounts to reverting my lean4#7352 and going further in the opposite direction

[Vilim Lendvaj]

yeah I did notice those deprecation warnings :sweat_smile:

[Vilim Lendvaj]

So yeah, the extra simping didn't cause me much trouble when converting the base library from Id to id, against your predictions.
Maybe the problems you speak of would start cropping up if I tried to convert Mathlib, but I think I've wasted enough of my time on this already.
I'll just accept "backwards compatibility" as the answer to my question, and move on.