3 stable releases

Uses old Rust 2015

1.0.2 Jul 23, 2018
1.0.1 Jul 18, 2018

#543 in Science

MIT license

9KB

Category Theory in Rust

Build Status Crates.io Docs.rs

a category ferris

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.

Buy Me A Coffee


lib.rs:

or, an exploration of category theory for systems programmers

a category

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

Build Status

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

CTFP Chapter Topic Articles Lecture Videos Notes
1 Introduction Category: The Essence of Composition Motivation, What is a category? See id and compose

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)

No runtime deps