has_bind.bind

Stream: new members

[Bjørn Kjos-Hanssen]

I'm looking at
https://cs.brown.edu/courses/cs1951x/docs/computability/NFA.html#NFA.step_set
In

M.step_set = λ (Ss : set σ) (a : α), Ss >>= λ (S : σ), M.step S a

I understand all the symbols except >>=. What is it for?

[Johan Commelin]

That's the bind operator for monads, right?

[Bjørn Kjos-Hanssen]

Hmm... what's the bind operator for monads and why do we need it to form a union?

[Bjørn Kjos-Hanssen]

I guess I can read about it here https://stackoverflow.com/questions/62308355/why-is-the-bind-operator-defined-as-it-is

[Kyle Miller]

Here's the definition of the set monad's bind operator: https://github.com/leanprover-community/mathlib/blob/48104c3a22ae4b35d92b8ad30831eb1591049958/src/data/set/lattice.lean#L1138

[Kyle Miller]

It's just bounded union

[Kyle Miller]

I expect the reason M.step_set is defined that way is that CS people are familiar with bind.

[Johan Commelin]

@Bjørn Kjos-Hanssen It's probably nice to work out bind for some of the basic monads like list and option.

[Kyle Miller]

(At a high level, monads are a way to work with data structures with variables/holes, where you can splice data structures of that type into those variables. The bind operator is, essentially, "treat all the elements of this data structure as if they were variable names and use this function as a map from variable names -> data to splice in." For set, you're splicing in another set for each element of the set, using the union to do the splicing. I got this point of view from stumbling across the correspondence between Lawvere theories and finitary monads.)

[Kevin Buzzard]

I always just look at the type and guess what's going on.

[Matt Diamond]

Kyle Miller said:

I expect the reason M.step_set is defined that way is that CS people are familiar with bind.

It looks like the latest version of step_set just uses the bounded union directly: https://github.com/leanprover-community/mathlib/blob/861589f224456f278c61596c0ee8a1ba449a6e8b/src/computability/NFA.lean#L40

[Matt Diamond]

My own understanding of monads, coming from a software engineering background, is that they allow you to map over a structure in a nested way. A normal map over a structure m a looks like m a -> (a -> b) -> m b: a simple transformation of the data from a to b. Monadic bind, on the other hand, is m a -> (a -> m b) -> m b. The transformation creates new structures which are then joined together into a single result. For example, bind on a list is just flatMap: list a -> (a -> list b) -> list b. Each individual element of the list is transformed into a new list, and this list of lists is then flattened into a single list.

This is why bind is bounded union in the realm of sets: Set a -> (a -> Set b) -> Set b. Monads are useful in functional programming because they allow you to map over the result of a computation while producing a new computation in the process.

[Kyle Miller]

@Matt Diamond That's the same idea -- it's just a matter of whether you happen to to think about applying a function as being substitution or evaluation.

For example, if you have [tt, tt, ff] and a function where tt -> [1,2] and ff -> [3], then bind is as-if you're substituting these lists in for the "variables" tt and ff to get [1,2,1,2,3] (with an intermediate [[1,2],[1,2],[3]] before flattening). It's like the list is a pasting diagram for lists. (I'm not meaning to explain the list monad to you here, just the point of view. I myself learned about monads from the programming side of things, and I came across this substitution idea from the pure math side much more recently.)

[Matt Diamond]

That's certainly true! Though map is also a kind of substitution, right? It seems like the key aspect of bind isn't the substituting but what you're substituting the "variables" with.

[Matt Diamond]

In fact, bind is literally just map with the addition of join. It's the joining that makes bind unique.

[Kyle Miller]

This is a substitution where you splice in with respect to the structure, which is what differentiates it from map (and pure is the key thing that lets you use bind as if it were map).

[Kyle Miller]

But, yeah, both map and bind are kinds of substitutions from this point of view, but bind is more general in that you can use pure to locally decide whether you're going to splice or not.

[Matt Diamond]

I'm not completely sure what you mean by "with respect to the structure". You don't mean ordering, right?

[Kevin Buzzard]

The thing I find difficult about all of this is understanding what the point is. As I say, if I hover over bind or pure or seq or return or whatever, I can see the type of what the corresponding funny monadic word means, and then I just look at list or option or set or whatever I'm working with and figure out what this map must be (because it's always pretty obvious) and then I move on, still none the wiser as to why computer scientists even care! For me this is just an obstruction to finding the right term, I look for bUnion or whatever and then I find that it's a monaddy word and I think "well fair enough",

[Kyle Miller]

By "structure" I'm being loose with terminology and I mean the functor under consideration.

[Matt Diamond]

@Kevin Buzzard That's fair... I'll admit it doesn't matter that much within a math context. It's more of a functional programming thing where you have to worry about managing state and side effects and all that.

[Eric Wieser]

(an aside; the link at the top of this thread is not canonical, those docs are @Rob Lewis' version generated from an old (>1 year) version of mathlib)

[Eric Wieser]

(unfortunately the fix to point non-canonical doc pages at the canonical one was added more recently than that page was built)

[Bjørn Kjos-Hanssen]

Matt Diamond said:

Kyle Miller said:

I expect the reason M.step_set is defined that way is that CS people are familiar with bind.

It looks like the latest version of step_set just uses the bounded union directly: https://github.com/leanprover-community/mathlib/blob/861589f224456f278c61596c0ee8a1ba449a6e8b/src/computability/NFA.lean#L40

Great, then I don't need bind after all.

[Kyle Miller]

@Kevin Buzzard If you're in the business of constructing specific discrete objects piece by piece by a sequence of transformations and substitutions (you could think about pasting diagrams for categories if you want) then monads seem to be a useful general algebraic structure to know about. But if not, I agree it can all be obscure. (I have to admit I can't remember off the top of my head what seq is. Oh, it's <*>, which I remember being useful in Haskell.)

[Kevin Buzzard]

Yeah most of them look like fish but seq looks like a space invader.

[Kevin Buzzard]

if the computer games you were brought up playing were made in the 1980s at least...

[Kevin Buzzard]

I guess that's another question: is there any logic to the >>= >=> stuff? I mean, am I supposed to be able to guess the function from the fish, or is it just something I should learn one by one?

[Kyle Miller]

I don't know if there's any logic to them, but the only reason I know about <*> is that you can, for example, write f <$> x <*> y <*> z to apply a 3-ary function across multiple pieces of monadic data, where <$> is fmap.

[Bjørn Kjos-Hanssen]

Matt Diamond said:

It looks like the latest version of step_set just uses the bounded union directly: https://github.com/leanprover-community/mathlib/blob/861589f224456f278c61596c0ee8a1ba449a6e8b/src/computability/NFA.lean#L40

What's the recommended command line one-liner to update mathlib again? It's been a while...

[Bjørn Kjos-Hanssen]

It looks like the two definitions of step_set, with and without the bind magic, are somehow equivalent in the end, since Lean accepts the following:

    show S ∈ list.foldl M.step_set ((
      λ (Ss : set σ) (a : α), Ss >>= λ (S : σ), M.step S a
    ) M.start z) [w], from
    show S ∈ list.foldl M.step_set (
      ⋃ s ∈ M.start, M.step s z
    ) [w], from
    sorry

[Kyle Miller]

Yes, bind for set is definitionally equal to a bounded union:

example {α β : Type} (s : set α) (f : α → set β) :
  s >>= f = ⋃ (x ∈ s), f x :=
rfl

[Mario Carneiro]

Kevin Buzzard said:

The thing I find difficult about all of this is understanding what the point is. As I say, if I hover over bind or pure or seq or return or whatever, I can see the type of what the corresponding funny monadic word means, and then I just look at list or option or set or whatever I'm working with and figure out what this map must be (because it's always pretty obvious) and then I move on, still none the wiser as to why computer scientists even care! For me this is just an obstruction to finding the right term, I look for bUnion or whatever and then I find that it's a monaddy word and I think "well fair enough",

To be fair, I feel the same way about writing stuff in category theory terminology like colimits and representable functors. I can only make sense of these terms by unfolding them in the context of specific categories of interest

[Anne Baanen]

Bjørn Kjos-Hanssen said:

Matt Diamond said:

It looks like the latest version of step_set just uses the bounded union directly: https://github.com/leanprover-community/mathlib/blob/861589f224456f278c61596c0ee8a1ba449a6e8b/src/computability/NFA.lean#L40

What's the recommended command line one-liner to update mathlib again? It's been a while...

I believe leanproject upgrade-mathlib should do that (don't recall using it myself before).