Question on Seq

Stream: new members

[Kevin Cheung]

In the documentation for the class Seq, it is written:

seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β

If mf : F (α → β) and mx : F α, then mf <*> mx : F β. In a monad this is the same as do let f ← mf; x ← mx; pure (f x): it evaluates first the function, then the argument, and applies one to the other.

To avoid surprising evaluation semantics, mx is taken "lazily", using a Unit→ f α function.

My question is on the last sentence: What is an example of a "surprising evaluation semantic" that one would like to avoid?

[Jason Reed]

I also found myself wondering about this comment. The docstring seems to go back to at least PR#1445.

Does the putative counterexample of surprising behavior have to do with nested actions in do-notation, perhaps? I can imagine how forcing the user to write a thunk might disallow the nested action, thereby disallowing the unexpected effect order.

[Mario Carneiro]

For one thing, I think that line is there for consistency with all the other monad combinators like *>, <*, <|> which do the same thing. But an example which would be affected by evaluation order of <*> would be in parser combinators, where e.g. you have

import Lean
open Std.Internal Parsec String

inductive Expr where
  | nat : Nat → Expr
  | add : Expr → Expr → Expr

partial def parseExpr : Parser Expr :=
  (pchar '+' *> .add <$> parseExpr <*> parseExpr) <|>
  .nat <$> digits

you would like the occurrences of parseExpr not to be evaluated immediately in the body of parseExpr because then it would immediately infinitely recurse before parsing anything.

[Jason Reed]

Thanks, that example is helpful

[Mario Carneiro]

Jason Reed said:

I can imagine how forcing the user to write a thunk might disallow the nested action, thereby disallowing the unexpected effect order.

Note that this doesn't happen - nested actions are permitted in that context, because the check for surrounding fun binders runs before macro expansion

[Jason Reed]

Hmm. My comment reflected the error message
cannot lift `(<- ...)` over a binder, this error usually happens when you are trying to lift a method nested in a `fun`, `let`, or `match`-alternative, and it can often be fixed by adding a missing `do`Lean 4
arising from, for example,

import Mathlib

-- this is fine:
def foo1 : List ℕ := do
  pure ((← [(· + 1), (· + 2), (· + 1000)]) (← [4, 5, 6]))

-- this is an error:
def foo2 : List ℕ := do
  pure ((fun x => x + (← [1, 2, 1000])) (← [4, 5, 6]))

but maybe you have something in mind that circumvents that in a different way. I'm still getting used to the edge cases of the scoping rules for (← ... ) but it seems like a great convenience feature.

[Jason Reed]

And in any case, I think I take your point that this is a tangential issue unrelated to why monad/applicative combinators take thunks. Just trying to clarify what I speculatively had in mind in the first place :)

[Jason Reed]

(and if I cured this error by doing, e.g.,

def foo2 : List ℕ :=
  let f (x : ℕ) : List ℕ := do
     pure (x + (← [1, 2, 1000]))
  do
  let res ← f (← [4, 5, 6])
  pure res

then I would think any evaluation-order consequences of this would be made fully explicit by the extra do and therefore not confusing)

[Mario Carneiro]

Yes, this error message appears when you literally write a function binder and use <- e under it. If you have macro "myfun" e => `(fun _ => e) then myfun (<- e) will not trigger the error but fun _ => (<- e) will

[Mario Carneiro]

This error message is mostly just a warning, trying to avoid the surprising order of evaluation that arises. It has both false positives and false negatives

[Mario Carneiro]

Jason Reed said:

(and if I cured this error by doing, e.g.,

def foo2 : List ℕ :=
  let f (x : ℕ) : List ℕ := do
     pure (x + (← [1, 2, 1000]))
  do
  let res ← f (← [4, 5, 6])
  pure res

then I would think any evaluation-order consequences of this would be made fully explicit by the extra do and therefore not confusing)

That's not the equivalent code to what the errored code would do if it were not for the error message. What it actually desugars to is

def foo2 : List ℕ := do
  let a ← [1, 2, 1000]
  let b ← [4, 5, 6]
  pure ((fun x => x + a) b)

[Mario Carneiro]

The fact that it doesn't evaluate the monadic action every time in the function is exactly the counterintuitive behavior which the error message is trying to warn you about