Category Theory in Rust

Get Started

I intend for each minor version to roughly correspond to one added chapter of documentation. I won't bump the major version until I get to the second Milewski course, and later the third, etc.

Note: This crate is more like a journal or notebook than a functional library; Import at your own discretion.

© 2018 Damien Stanton

See LICENSE for details.

lib.rs:

or, an exploration of category theory for systems programmers

What follows in this library is derived from Category Theory for Programmers, a long-running blog series by Bartosz Milewki. A nice "book" created from original blog posts can be found here.

Crate Health

Goals

My intention is simply to share my learning experience with category theory by using the built-in documentation and testing faculties that Rust provides. I will also conduct screen casts to explore each implementation so that I can make sure that what I commit to the crate is logical. I hope that by doing this, others can apply this knowledge to what they do at $WORK in C++, Go, Java, etc.

Table of Contents

Non-code challenge questions:

Chapter 1

Is the world-wide web a category in any sense? Are links morphisms?

I would say yes. We know that web pages have something akin to an identity morphism: its URI/URL. And links between pages may be composable (a link from site A to B can, through the redirect protocol, map to a third side C).

Update: After a conversation with a few people in the #categorytheory channel on FP Slack, care must be taken to specify that we mean the morphism that defines the whole REST or HATEOAS command cycle for a link in this example; not the links themselves. So the correct answer to Bartosz's question depends on what we mean by what links are.

Is Facebook a category, with people as objects and friendships as morphisms?

Not really, because social relationships cannot always compose. Friend C, friend of B, is not necessarily friend of A.

When is a directed graph a category?

A DAG would classify as a category when a graph G has vertices V and edges E such that:

• all paths in the graph can be concatenated
• each V has an E that loops back to itself (so that it satisfies identity)