sara :: forall a. a @MxLambda [they/them] Software engineer at Klarna I tweet about pure FP, type theory, categories, and whatever is currently on my mind! [trans,ace,vegan,autistic] Oct. 18, 2019 1 min read

Here we go!! ^^

Lawvere is on the menu!

Starting out by laying some ground work: what is a category, according to a mathematician?

Composition and identity of arrows (which generalize functions!)

As fp:ers we all learn to love composition, but why do we care about enforcing identity?

It lets us define isomorphisms!

Introducing the notion of a "T-program" which given any sort of "computation" (List, Maybe, State, etc) is a program of type A -> T(B)

eg Int -> Maybe String is a Maybe-program from Int to String!

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!)

How do we make such a category? How do we define composition of functions

f : A -> T(B)
g : B -> T(C)

This is where the bind function comes in! (>>= in haskell)

Example showing the category of List-programs!

Audience question:

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!

Time for part 2, lawvere theories!

Arrows from singleton types to lists

Defining a List-theory

We get a lawvere theory by considering the opposite category of a T-program category

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)

Resources for learning more!

Thank you so much to @emilyriehl!


You can follow @MxLambda.



Bookmark

____
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.