SeqRight `HAndThen`

Stream: lean4

[Mac]

I was a little surpised to leanr the following does not work:

def foobar : IO Unit :=
  IO.println "foo" >> IO.println "bar"
/-
failed to synthesize instance
  HAndThen (IO Unit) (IO Unit) (IO Unit)
-/

Lean 4 appears to missing the following instance:

instance [SeqRight m] : HAndThen (m α) (m β) (m β) := ⟨SeqRight.seqRight⟩

I imagine there is some reason this instance has been dropped, but I am curious as to what it is. Especially, as the fact that >> does not work for monads would surprise anyone coming from something like Haskell.

I could see that such an instance could cause overlap issues due to its generality. However, I would then think that there would instances for more specific cases (ex. an HAndThen (IO α) (IO β) (IO β) or AndThen (IO Unit) instance).

[Sebastian Ullrich]

We already have *> for monads. We try to avoid duplicate operators that only exist for historical reasons in Haskell (see also: repurposing return)

[Mac]

Sebastian Ullrich said:

We already have *> for monads. We try to avoid duplicate operators that only exist for historical reasons in Haskell (see also: repurposing return)

But its not a duplicate operator? It is a more general operator. Having a function that places the HAndThen/AndThen constraint on a object means that the object doesn't have to be a first-order monad, it can be just a simple action (ex. IO.RealWorld -> IO.RealWorld or ParserState -> ParserState/Parser) rather than a monadic action (ex. IO a). That is, a monadic sequence is a more specialization case of AndThen. Thus, places that accept an AndThen would generally except monads and simple actions. This makes the fact that monadic actions are not considered a part of the broader action abstraction very unexpected (and concept-breaking). After all, even at a semantic level a monad sequence means 'perform monad action m a and then perform m b.

[Wojciech Nawrocki]

For monads specifically iirc it was decided to forbid heterogeneous sequencing because it allows implicitly forgetting return values. So instead of writing getFoo >> print "got foo" you must do let _ <- getFoo; print "got foo", i.e. explicitly ignore the return.

[Mac]

Wojciech Nawrocki said:

For monads specifically iirc it was decided to forbid heterogeneous sequencing because it allows implicitly forgetting return values. So instead of writing getFoo >> print "got foo" you must do let _ <- getFoo; print "got foo", i.e. explicitly ignore the return.

Still, there is no homogenous or PUnit instance either which does not have this problem. Furthermore, you can still do heterogenous sequence with *>. Also, I don't really get what's wrong stylistically with forgetting return values. I can imagine technically, though, that such automatic forgetting could be pain for type inference (both in implementation and in end-use).