sara :: forall a. a+ Your Authors @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 + Your Authors

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.

Since you’re here...

... we’re asking visitors like you to make a contribution to support this independent project. In these uncertain times, access to information is vital. Threader gets 1,000,000+ visits a month and our iOS Twitter client was featured as an App of the Day by Apple. Your financial support will help two developers to keep working on this app. Everyone’s contribution, big or small, is so valuable. Support Threader by becoming premium or by donating on PayPal. Thank you.


Follow Threader