Starting out by laying some ground work: what is a category, according to a mathematician?
Composition and identity of arrows (which generalize functions!)
Such a T is a monad precisely when these T-programs form a category!
(this is the kleisli based definition of a monad, more popular in fp, whereas mathematicians usually define them as a monoid in a monoidal endofunctor category!)
Can we come up with other ways to define this composition?
Answer: sometimes, yes! For some computations, there are multiple monads/program categories we can come up with! They are not necessarily unique!
What is the point of lawvere theories compared to monads?
Easier to reuse a lawvere theory in other categories
Easier to compose different computational effects (eg for when you want both List- and Maybe-programs)
Thank you so much to @emilyriehl!
You can follow @MxLambda.
Tip: mention @threader_app on a Twitter thread with the keyword “compile” to get a link to it.
Enjoy Threader? Sign up.
Threader is an independent project created by only two developers. The site gets 500,000+ visits a month and our iOS Twitter client was featured as an App of the Day by Apple. Running this space is expensive and time consuming. If you find Threader useful, please consider supporting us to make it a sustainable project.