if-else block that isn't `m Unit` can discard result

Stream: lean4

[Jovan Gerbscheid]

Is it expected that this doesn't throw an error?

def foo {α : Type} (a b c : α) : Id α := do
  if true then
    pure a
  else
    pure b
  pure c

#eval foo 1 2 3 -- 3

[Arthur Paulino]

Yeah this looks odd. But I think it's doing this:

def foo {α : Type} (a b c : α) : Id α := do
  let _ <- if true then
      pure a
    else
      pure b
  pure c

Which is sensible

[Edward van de Meent]

the odd(?) thing is that it doesn't do that when you drop the pure c line

[Mario Carneiro]

I think you should view this as similar to

example : Id Nat := do
  pure 1
  pure 2

[Mario Carneiro]

oh, actually that's a bad example, that works only with import Mathlib because 1 is interpreted as living in PUnit because it's a ring :face_with_peeking_eye:

[Mario Carneiro]

So I'm on the side "this is not sensible", the let _ <- part is deliberately omitted when you just have a sequence of do elems (in fact it is more like let () <-)

[Mario Carneiro]

to make the distinction a little more stark:

example : Id Nat := do
  if true then pure 1 else pure 2 -- ok
  pure 3

example : Id Nat := do
  (if true then pure 1 else pure 2) -- fail
  pure 3

[Kim Morrison]

Perhaps PUnit should not itself be a ring, and Mathlib could make an alternative equivalent type to carry this structure!

[Edward van de Meent]

Mario Carneiro said:

I think you should view this as similar to

example : Id Nat := do
  pure 1
  pure 2

Indeed, I was hoping that throwing away the result would be the default behaviour in do notation, just like in Haskell, but since that isn't the case, it's odd that if does have this behaviour

[Mario Carneiro]

it used to discard, this behavior was changed I think because it makes it easier to spot bugs where return values are silently discarded. You should use let _ <- to explicitly drop a value you don't want

[Mario Carneiro]

or _ <- if you are feeling pressed for characters