Comonads

Stream: general

[Wrenna Robson]

Hi all.

I was wondering how one might go about defining comonads in Lean, in a way compatible with/analogous to how monads are defined. Any thoughts?

[Jason Rute]

When you say, "how monads are defined", do you mean docs#monad as a programming language concept, that is a type class which may or may not be lawful (obey the monad axioms), such as the tactic and io monads? Or monads as a mathematical definition in category theory, i.e. docs#category_theory.monad?

[Adam Topaz]

docs#category_theory.comonad (if you want the categorical def)

[Jason Rute]

I assume you mean the category theory definition, but if you want comonads as a programming language concept, here is an article on how to do it in Haskell: https://bartoszmilewski.com/2017/01/02/comonads/

[Jason Rute]

(It would be a fun project for someone to translate the code in that book, Category Theory for Programmers, from Haskell to Lean(4). There already is a Scala translation.)

[Wrenna Robson]

Yeah, I meant the programming language concept!

[Kevin Buzzard]

Is the tactic monad not lawful? My opinion of it just diminished a little

[Kevin Buzzard]

It is a shame that there are these words like monad and topos and ring which mean different things to different communities. It impairs communication.

[Mario Carneiro]

I think the tactic monad is lawful, if you ignore things like tactic.unsafe_run_io which allow for tactics that are not pure-functional

[Mario Carneiro]

well, equality of haskell functions is always a bit of sleight of hand since there are plenty of effects in functional programs like allocation

[Mario Carneiro]

and you can't really take back a RealWorld token in an IO computation once you've used it in an IO function to change the state of the world

[Jireh Loreaux]

Kevin, I think you parsed Jason's comment in a way different than what was intended: "programming language concept ... such as the tactic and io monads", but I could be wrong.

[Jason Rute]

Yes. It was ambiguous. I didn’t mean to pick on the tactic monad. Nonetheless, the first time I saw the monad class and it’s description in Programming in Lean, I was very confused because there was no mention of the axioms. I think the reality is that one wants monads to be as close to lawful as possible, but in real programming edge cases do come through sometimes. One example in the more mathematical side of Lean is the Giry monad which is only lawful if you consider measurable functions.

[Wrenna Robson]

Jason Rute said:

(It would be a fun project for someone to translate the code in that book, Category Theory for Programmers, from Haskell to Lean(4). There already is a Scala translation.)

I was reading this. The tricky thing I found is that in Lean, (programming) monads are defined in terms of extending applicative functors. But it's not clear to me what a "coapplicative" functor would be or how that should be defined, or even if it's right to do it that way.

[Wrenna Robson]

(Also: this is more of a general category-theory question, but in that, fmap in the comonad is just, well, fmap. But I was wondering - how come it doesn't become covariant, so that you don't have fmap : (a -> b) -> f b -> f a?

[Reid Barton]

Wrenna Robson said:

I was reading this. The tricky thing I found is that in Lean, (programming) monads are defined in terms of extending applicative functors. But it's not clear to me what a "coapplicative" functor would be or how that should be defined, or even if it's right to do it that way.

This is a feature of the category of sets--a general monad isn't applicative (= lax monoidal).

[Reid Barton]

Wrenna Robson said:

(Also: this is more of a general category-theory question, but in that, fmap in the comonad is just, well, fmap. But I was wondering - how come it doesn't become covariant, so that you don't have fmap : (a -> b) -> f b -> f a?

A comonad is a monad on the opposite category, so both source and target are reversed = it's still a functor on the original category.

[Wrenna Robson]

Aha, right.

[Wrenna Robson]

Reid Barton said:

Wrenna Robson said:

I was reading this. The tricky thing I found is that in Lean, (programming) monads are defined in terms of extending applicative functors. But it's not clear to me what a "coapplicative" functor would be or how that should be defined, or even if it's right to do it that way.

This is a feature of the category of sets--a general monad isn't applicative (= lax monoidal).

Right, but "monad" in the programming sense in Lean is always applicative?

[Reid Barton]

because monad there is specialized to Type (= Set)

[Reid Barton]

comonads are also specialized, but they are monads on Set^op--and Set^op behaves very differently from Set

[Wrenna Robson]

Aha - thank you.

[Wrenna Robson]

Control.Monad is Haskell appears to have some sort of ComonadApply class, but in light of what you've said I'm sceptical of it. https://hackage.haskell.org/package/comonad-5.0.8/docs/Control-Comonad.html#t:ComonadApply

[Reid Barton]

So, you should not in general expect comonads (in the programming sense) to be formally dual to monads (in the programming sense)

[Wrenna Robson]

right

[Wrenna Robson]

That is confusing!