Monad and Applicative

Stream: new members

[Nam]

Hi, I am reading https://leanprover.github.io/lean4/doc/monads/monads.lean.html#what-separates-monads-from-applicatives but I don't quite understand that paragraph. It says "You cannot really determine the structure of "future" operations" but we do. For example, a Maybe monad can only produce another Maybe monad in the future. Is that not right?

[Mario Carneiro]

There seem to be some missing words in that sentence. It's talking about applicatives there

[Mario Carneiro]

A monad allows you to determine the structure of future computations based on the results of past computations

[Mario Carneiro]

In an applicative, you determine the structure in advance of getting any of the results

[Mario Carneiro]

Here by "structure of computations" we mean things like which functions get called

[Nam]

Thank you. I think I've got it now. That sentence might have been a general statement, applicable to both Applicative and Monad.

[Nam]

the first sentence sets up the premise that context is what separates the two. the second sentence states that general observation. the third says that with applicative you can't get final value (i guess you can with monad, e.g. Nothing), but you can determine the call tree.

[Nam]

does that sound about right?

[Mario Carneiro]

I'm not sure what you mean by "you can't get the final value"

[Mario Carneiro]

you can always get the value if you know what type it is; it's just that the monad / applicative operations don't give you a way to exit the monad generically

[Mario Carneiro]

most monads will have a run function which extracts the data from the monad. It's just that the type signature of this function varies a lot depending on the monad

[Nam]

by "final value" i mean the same as "final function result" in that paragraph

[Nam]

"""With applicatives, you can't get the final function result without evaluating everything,"""

[Mario Carneiro]

Stated that way, it's true for monads too

[Mario Carneiro]

or functions in general

[Mario Carneiro]

you don't get the result until everything is evaluated

[Nam]

damn. then i don't know what that paragraph means.

[Kyle Miller]

@Nam I think that paragraph is getting at the fact that applicatives have more restrictive control flow than monads. Roughly speaking, with applicatives you can figure out what the control flow is going to be even without evaluating anything, but with monads the control flow can depend on the specific values involved. (@Chris Lovett The sentence in the monad docs might be clearer as "With applicatives, you can determine the structure of how the operation will take place even before you evaluate everything.")

[Nam]

ah, yes, thank you Kyle. that's roughly what i understand too.

[Nam]

I've another question. the bind operation is defined as bind : {α β : Type u} → f α → (α → f β) → f β. it uses the same type constructor f, which is the monad itself. that means the chain of operations must return the same type of monad. why can't it return a different type of monad?

[Kyle Miller]

@Nam Because then it wouldn't be a monad :wink: That's just the definition.

[Nam]

lol fair enough

[Kyle Miller]

One example of something that's monad-like but not a monad is indexed monads. One version I've seen has a bind operation of type bind : {α β : Type u} → f i j α → (α → f j k β) → f i k β where for each i you have that f i i is a monad.