Skip to content

Category Theory for Programmers 第一部分

Posted on:2021.08.25

TOC

Open TOC

Preface

听说代码主要是 Haskell,但也有 C++,另见 从零开始的简单函数式 C++

这里有一份参考答案:My solutions to Bartosz Milewski’s “Category Theory for Programmers”

WHF 推荐视频:“Categories for the Working Hacker” by Philip Wadler

Category: The Essence of Composition

A category consists of objects and arrows (morphisms).

Arrows can be composed.

Properties of Composition

Neutral values like zero or id are extremely useful when working with symbolic variables. That’s why Romans were not very good at algebra, whereas the Arabs and the Persians, who were familiar with the concept of zero, were. So the identity function becomes very handy as an argument to, or a return from, a higher-order function. Higher order functions are what make symbolic manipulation of functions possible. They are the algebra of functions.

Haskell

.

id

C++

#include<iostream>
template<class T> T id(T x) { return x; }
int add(int i) {
return i + 1;
}
int main() {
int ans = id(add)(3);
std::cout << ans;
}

对于函数组合,不太会 🤣

Composition is the Essence of Programming

Types and Functions

Types

类型是值的集合。集合可以是有限集,也可以是无限集。

The great thing is that there is a category of sets, which is called 𝐒𝐞𝐭 , and we’ll just work with it. In 𝐒𝐞𝐭 , objects are sets and morphisms (arrows) are functions.

理想情况下,Haskell 的类型就是集合,Haskell 的函数就是集合之间的数学函数。然而,有些 Haskell 的函数无法在有限步骤内计算出结果,为此我们用 表示。

The special value called the bottom.

所以,函数 f :: Bool -> Bool 可能会返回 TrueFalse

我们还可以显式地返回 ,例如在 Haskell 中使用 undefined

这样会返回 的函数也被称为偏函数。

Because of the bottom, you’ll see the category of Haskell types and functions referred to as Hask rather than 𝐒𝐞𝐭.

Examples of Types

空集对应的类型为 Void,注意这不是 C++ 中的 void

absurd :: Void -> a

As for what this function can return, there are no restrictions whatsoever. It can return any type (although it never will, because it can’t be called).

单元集对应的类型为 void,在 Haskell 中记作 ()。若该类型作为参数类型:

int f44() { return 44; }

Haskell 中:

f44 :: () -> Integer
f44 () = 44

Functions from unit to any type 𝐴 are in one-to-one correspondence with the elements of that set 𝐴.

若该类型作为返回值类型,我们让参数成为多态类型:

template<class T>
void unit(T) {}

In C++ such functions are used for side effects, but we know that these are not real functions in the mathematical sense of the word. A pure function that returns unit does nothing: it discards its argument.

Haskell 中:

unit :: a -> ()
unit _ = ()

双元集对应的类型为 bool,在 Haskell 中可以这样实现:

data Bool = True | False

对于 C++,考虑使用枚举类

Functions

函数有纯与不纯之分。没有副作用的函数被称为纯函数。

通过引入数学模型,我们可以用数学对象来形式化程序的语义,给出程序的正确性证明

Denotational semantics - Wikipedia

由于数学函数都是纯函数,在这样的程序中,我们无法表达副作用。

然而,范畴论指出计算效应(副作用)可以通过映射到单子上实现。

Ex

bool f() {
std::cout << "Hello!" << std::endl;
return true;
}
int g(int x) {
static int y = 0;
y += x;
return y;
}

Categories Great and Small

No Objects

没有对象,没有态射。

It’s a very sad category by itself, but it may be important in the context of other categories, for instance, in the category of all categories (yes, there is one).

Simple Graphs

自反闭包和传递闭包。

Such a category is called a free category generated by a given graph. It’s an example of a free construction, a process of completing a given structure by extending it with a minimum number of items to satisfy its laws (here, the laws of a category).

Orders

Let’s characterize these ordered sets as categories. A preorder is a category where there is at most one morphism going from any object 𝑎 to any object 𝑏. Another name for such a category is “thin.” A preorder is a thin category.

A set of morphisms from object 𝑎 to object 𝑏 in a category 𝐂 is called a homset and is written as 𝐂(𝑎 , 𝑏).So every hom-set in a preorder is either empty or a singleton.

Monoid as Set

幺半群。

Monoids are ubiquitous in programming. They show up as strings, lists, foldable data structures, futures in concurrent programming, events in functional reactive programming, and so on.

Haskell 中可以这样实现:

class Monoid m where
mempty :: m
mappend :: m -> m -> m

幺半群的实例:

instance Monoid String where
mempty = ""
mappend = (++)

对这里的 mappend = (++),书中给出了解释:

The latter is called extensional equality, and states the fact that for any two input strings, the outputs of mappend and (++) are the same. Since the values of arguments are sometimes called points (as in: the value of 𝑓 at point 𝑥), this is called point-wise equality. Function equality without specifying the arguments is described as point-free. (Incidentally, point-free equations often involve composition of functions, which is symbolized by a point, so this might be a little confusing to the beginner.)

C++ 的实现不太懂,略去。

Monoid as Category

关键是我们要将之前的集合看作一个整体的对象。

a17d743156834dd486e7e12fd4220698.jpg

Elements of a hom-set can be seen both as morphisms, which follow the rules of composition, and as points in a set. Here, composition of morphisms in 𝐌 translates into monoidal product in the set 𝐌(𝑚 , 𝑚).

幺半群的二元运算通过部分应用成为这种范畴的态射,例如习题第四题:

Represent the Bool monoid with the AND operator as a category: List the morphisms and their rules of composition.

这个范畴中只有一个对象 Bool 类型,态射有两种,一种是 AND True,也是恒等态射,一种是 AND False,它们的组合是 AND False

Kleisli Categories

Writer monad

It’s an example of the so called Kleisli category — a category based on a monad.

For our limited purposes, a Kleisli category has, as objects, the types of the underlying programming language. Morphisms from type 𝐴 to type 𝐵 are functions that go from 𝐴 to a type derived from 𝐵 using the particular embellishment.

Each Kleisli category defines its own way of composing such morphisms, as well as the identity morphisms with respect to that composition. (Later we’ll see that the imprecise term “embellishment” corresponds to the notion of an endofunctor in a category.)

C++

这里的类型 string 可以换成任意满足幺半群性质的类型。

#include<iostream>
#include<algorithm>
#include<vector>
using namespace std;
template<class A>
using Writer = pair<A, string>;
vector<string> words(string s) {
vector<string> result{ "" };
for (auto i = begin(s); i != end(s); ++i)
{
if (isspace(*i))
result.push_back("");
else
result.back() += *i;
}
return result;
}
Writer<string> toUpper(string s) {
string result;
int (*toupperp)(int) = &toupper;
transform(begin(s), end(s), back_inserter(result), toupperp);
return make_pair(result, "toUpper ");
}
Writer<vector<string>> toWords(string s) {
return make_pair(words(s), "toWords ");
}
auto const compose = [](auto m1, auto m2) {
return [m1, m2](auto x) {
auto p1 = m1(x);
auto p2 = m2(p1.first);
return make_pair(p2.first, p1.second + p2.second);
};
};
Writer<vector<string>> process(string s) {
return compose(toUpper, toWords)(s);
}
int main() {
string s = "abc cba";
auto ans = process(s);
cout << ans.second << endl;
for (string i : ans.first) {
cout << i << endl;
}
}

对应的恒等态射为:

Writer<string> _identity(string s) {
return make_pair(s, "");
}

注:书上 compose 的另一种实现似乎行不通。

Haskell

import Data.Char
type Writer a = (a, String)
(>=>) :: (a -> Writer b) -> (b -> Writer c) -> (a -> Writer c)
m1 >=> m2 = \x ->
let (y, s1) = m1 x
(z, s2) = m2 y
in (z, s1 ++ s2)
upCase :: String -> Writer String
upCase s = (map toUpper s, "upCase ")
toWords :: String -> Writer [String]
toWords s = (words s, "toWords ")
process :: String -> Writer [String]
process = (>=>) upCase toWords

对应的恒等态射为:

return :: a -> Writer a
return x = (x, "")

注:另见 Haskell 趣学指南第二部分中 Writer monad 部分。

Ex

取倒数,开平方

#include<iostream>
using namespace std;
template<class A> class optional {
bool _isValid;
A _value;
public:
optional() : _isValid(false) {}
optional(A v) : _isValid(true), _value(v) {}
bool isValid() const { return _isValid; }
A value() const { return _value; }
};
optional<double> safe_root(double x) {
if (x >= 0) return optional<double>{sqrt(x)};
else return optional<double>{};
}
optional<double> safe_reciprocal(double x) {
if (x != 0) return optional<double>{1 / x};
else return optional<double>{};
}
auto const compose = [](auto m1, auto m2) {
return [m1, m2](auto x) {
auto p1 = m1(x);
if (p1.isValid()) {
auto p2 = m2(p1.value());
if (p2.isValid()) {
return optional<double>{p2.value()};
}
else {
return optional<double>{};
}
}
else {
return optional<double>{};
}
};
};
optional<double> process(double x) {
return compose(safe_reciprocal, safe_root)(x);
}
int main() {
double x;
cin >> x;
auto ans = process(x);
if (ans.isValid()) {
cout << ans.value();
}
else {
cout << "Invalid!";
}
}

简单来说,态射的组合就是标志位取与,函数组合。恒等态射就是标志位为 true,函数为恒等函数。

另见 Fast Inverse Square Root — A Quake III Algorithm

#include<iostream>
using namespace std;
float Q_rsqrt(float number) {
union { float f; uint32_t i; } conv;
float x2 = number * 0.5F;
conv.f = number;
conv.i = 0x5f3759df - (conv.i >> 1); // ???
conv.f = conv.f * (1.5F - (x2 * conv.f * conv.f));
return conv.f;
}
int main() {
float x;
cin >> x;
cout << Q_rsqrt(x);
}

Summary

We have one more degree of freedom to play with: the composition itself. It turns out that this is exactly the degree of freedom which makes it possible to give simple denotational semantics to programs that in imperative languages are traditionally implemented using side effects.

Products and Coproducts

There is a common construction in category theory called the universal construction for defining objects in terms of their relationships. One way of doing this is to pick a pattern, a particular shape constructed from objects and morphisms, and look for all its occurrences in the category. If it’s a common enough pattern, and the category is large, chances are you’ll have lots and lots of hits. The trick is to establish some kind of ranking among those hits, and pick what could be considered the best fit.

Initial Object and Terminal Object

The initial object is the object that has one and only one morphism going to any object in the category.

在 𝐒𝐞𝐭 范畴中,初始对象为 Void,其态射为 absurd(一组函数)。

The terminal object is the object with one and only one morphism coming to it from any object in the category.

在 𝐒𝐞𝐭 范畴中,终止对象为 void,其态射为 unit(一组函数)。

初始对象和终止对象是对偶的,也就是说终止对象是其对偶范畴(态射反向)中的初始对象。

Isomorphisms

An isomorphism is an invertible morphism; or a pair of morphisms, one being the inverse of the other.

f . g = id
g . f = id

37b3ab9c6c7a4417a153b25e986df014.png

容易证明上面的两个初始对象是 unique up to isomorphism,又因为初始对象的定义中 one and only one,这说明任两个初始对象是 unique up to unique isomorphism

对终止对象也有同样的结论。

This “uniqueness up to unique isomorphism” is the important property of all universal constructions.

Product and Coproduct

The next universal construction is that of a product.

p :: c -> a
q :: c -> b

8aa58bca6a8e495e9adf850f2fd56d67.jpg

举个例子,考虑 IntBool 的积,Int 是一个候选,因为它满足 pattern

p' :: Int -> Int
p' x = x
q' :: Int -> Bool
q' _ = True

我们发现存在从 Int(图中的 c')到 (Int, Bool)(图中的 c)的态射,使得:

p' = p . m
q' = q . m

可以认为 mp'q' 的公因式。

这样的态射为:

m :: Int -> (Int, Bool)
m x = (x, True)

然而,我们可以证明不存在从 (Int, Bool)Int 的态射,满足上述条件。

There is no way to factorize fst and snd.

另一个候选是 (Int, Int, Bool),满足 pattern

p :: (Int, Int, Bool) -> Int
p (x, _, _) = x
q :: (Int, Int, Bool) -> Bool
q (_, _, b) = b

存在从 (Int, Int, Bool)(图中的 c')到 (Int, Bool)(图中的 c)的态射:

m (x, _, b) = (x, b)

反过来,我们发现存在不止一种从 (Int, Bool)Int 的态射,满足上述条件。

There is more than one way to factorize fst and snd.

总结一下,积的定义为:

A product of two objects 𝑎 and 𝑏 is the object 𝑐 equipped with two projections such that for any other object 𝑐′ equipped with two projections there is a unique morphism 𝑚 from 𝑐′ to 𝑐 that factorizes those projections.

Such a product doesn’t always exist, but when it does, it is unique up to a unique isomorphism.

A (higher order) function that produces the factorizing function m from two candidates is sometimes called the factorizer. In our case, it would be the function:

factorizer :: (c -> a) -> (c -> b) -> (c -> (a, b))
factorizer p q = \x -> (p x, q x)

余积的定义与之完全对偶。

0f7dcb90b0874077bdabd6744fb08cec.jpg

Haskell 中,积为序对,余积为 Either

data Either a b = Left a | Right b

对应的 factorizer 为:

factorizer :: (a -> c) -> (b -> c) -> Either a b -> c
factorizer i j (Left a) = i a
factorizer i j (Right b) = j b

Asymmetry

The category of sets is not symmetric with respect to the inversion of arrows.

This is not an intrinsic property of sets, it’s a property of functions, which we use as morphisms in 𝐒𝐞𝐭. Functions are, in general, asymmetric.

  • surjective & embedding
  • injective & collapsing

In the category of sets, an isomorphism is the same as a bijection.

Ex

关于余积的一些练习:

int i(int n) { return n; }
int j(bool b) { return b ? 0: 1; }

使用 Haskell

i :: Int -> Int
i n = n
j :: Bool -> Int
j b = if b then 0 else 1
m :: Either Int Bool -> Int
m (Left x) = x
m (Right y) = if y then 0 else 1

a1bfalse,此时 c1,而 c' 可能为 Left 1,也可能为 RIght false,这与函数的定义矛盾。

int i(int n) {
if (n < 0) return n;
return n + 2;
}
int j(bool b) { return b ? 0: 1; }

考虑整数的溢出即可。

Consider some type SuperEither defined as:

data SuperEither = IntIntTuple (Int, Int) | BoolBoolTuple (Bool, Bool)

We can define injections into this type from int and bool of the forms:

intint :: Int -> SuperEither
intint x = IntIntTuple (x, x)
boolbool :: Bool -> SuperEither
boolbool x = BoolBoolTuple (x, x)

Then we can define multiple morphisms from SuperEither into Either that take either the first or second element.

Simple Algebraic Data Types

Product Types

Haskell 中,积为序对。

Pairs are not strictly commutative: a pair (Int, Bool) cannot be substituted for a pair (Bool, Int), even though they carry the same information. They are, however, commutative up to isomorphism — the isomorphism being given by the swap function (which is its own inverse):

swap :: (a, b) -> (b, a)
swap (x, y) = (y, x)

将序对嵌套在序对里就构成了多元组。

You can combine an arbitrary number of types into a product by nesting pairs inside pairs, but there is an easier way: nested pairs are equivalent to tuples.

alpha :: ((a, b), c) -> (a, (b, c))
alpha ((x, y), z) = (x, (y, z))
alpha_inv :: (a, (b, c)) -> ((a, b), c)
alpha_inv (x, (y, z)) = ((x, y), z)

在同构意义下,我们可以将序对运算视为一个幺半群:

Prelude> :t (,)
(,) :: a -> b -> (a, b)

其单位元为 (),因为在同构意义下,(a, ())a 等价:

rho :: (a, ()) -> a
rho (x, ()) = x
rho_inv :: a -> (a, ())
rho_inv x = (x, ())

总结来说:

𝐒𝐞𝐭 (the category of sets) is a monoidal category. It’s a category that’s also a monoid, in the sense that you can multiply objects (here, take their Cartesian product).

当然在 Haskell 中,积也可以这样表示:

data Pair a b = Pair a b

Type constructors are used to construct types; data constructors, to construct values.

为了使元组中的各个分量更加清晰,我们可以使用记录语法。

A product type with named fields is called a record in Haskell, and a struct in C.

Sum Types

Haskell 中,余积为 Either

data Either a b = Left a | Right b

And like pairs, Eithers are commutative (up to isomorphism), can be nested, and the nesting order is irrelevant (up to isomorphism).

It turns out that 𝐒𝐞𝐭 is also a (symmetric) monoidal category with respect to coproduct. The role of the binary operation is played by the disjoint sum, and the role of the unit element is played by the initial object.

也就是说,Either a Voida 同构。

Sum types are pretty common in Haskell, but their C++ equivalents, unions or variants, are much less common. There are several reasons for that.

First of all, the simplest sum types are just enumerations and are implemented using enum in C++.

data Color = Red | Green | Blue

等价于:

enum { Red, Green, Blue };

Simple sum types that encode the presence or absence of a value are variously implemented in C++ using special tricks and “impossible” values, like empty strings, negative numbers, null pointers, etc. This kind of optionality, if deliberate, is expressed in Haskell using the Maybe type:

data Maybe a = Nothing | Just a

等价于:

data Maybe a = Either () a

More complex sum types are often faked in C++ using pointers. A pointer can be either null, or point to a value of specific type.

以列表为例,在 Haskell 中:

data List a = Nil | Cons a (List a)

C++ 中:

template<class A>
class List {
Node<A>* _head;
public:
List() : _head(nullptr) {} // Nil
List(A a, List<A> l) // Cons
: _head(new Node<A>(a, l))
{}
};

由于 Haskell 的数据结构是不可变的,所以这种构造是可逆的:

maybeTail :: List a -> Maybe (List a)
maybeTail Nil = Nothing
maybeTail (Cons _ t) = Just t

Even more elaborate sum types are implemented in C++ using polymorphic class hierarchies. A family of classes with a common ancestor may be understood as one variant type, in which the vtable serves as a hidden tag. What in Haskell would be done by pattern matching on the constructor, and by calling specialized code, in C++ is accomplished by dispatching a call to a virtual function based on the vtable pointer.

Ex 部分。

You will rarely see union used as a sum type in C++ because of severe limitations on what can go into a union.

Algebra of Types

将积和余积组合,一图胜千言:

64d76e7856384563bbed76ba569562e3.jpg

满足分配律,也就是说 (a, Either b c)Either (a, b) (a, c) 同构。这表明这是一个半环

回到列表数据类型:

data List a = Nil | Cons a (List a)

我们使用代数表示:x=1+axx=1+a*x,不断替换 xx 可得:x=1+a+aa+aaa+...x=1+a+a*a+a*a*a+...,这描述了列表自身。

注意到积对应了 and,而余积对应了 or,所以我们还有下面的映射关系:

6f9367dd4e8e4e79813a296f83b8a305.jpg

This is the basis of the Curry-Howard isomorphism between logic and type theory.

Ex

Here’s a sum type defined in Haskell:

data Shape = Circle Float | Rect Float Float

When we want to define a function like area that acts on a Shape, we do it by pattern matching on the two constructors:

area :: Shape -> Float
area (Circle r) = pi * r * r
area (Rect d h) = d * h

Implement Shape in C++ or Java as an interface and create two classes: Circle and Rect. Implement area as a virtual function.

C++

#define _USE_MATH_DEFINES
#include <iostream>
#include <cmath>
using namespace std;
class Shape {
public:
virtual double area() = 0;
};
class Circle : public Shape {
private:
double r;
public:
Circle(double _r) :r(_r) {}
double area() {
return M_PI * r * r;
}
};
class Rect : public Shape {
private:
double d;
double h;
public:
Rect(double _d, double _h) :d(_d), h(_h) {}
double area() {
return d * h;
}
};
int main() {
unique_ptr<Shape> p = make_unique<Circle>(1);
cout << p->area() << endl;
p = make_unique<Rect>(1, 2);
cout << p->area() << endl;
}

添加一个新的方法(难),添加一个新的类型(易)。

Haskell

添加一个新的方法(易),添加一个新的类型(难)。

Functors

函子是范畴之间的映射:

091db909c4e34a8db0c5bb0382df7667.jpg

函子保持了范畴的内在结构(态射):

In this sense functors are “continuous” (although there exists an even more restrictive notion of continuity for functors).

Just like functions, functors may do both collapsing and embedding.

The maximally collapsing functor is called the constant functor Δ𝑐. It maps every object in the source category to one selected object 𝑐 in the target category.

Functors in Programming

在类型范畴上的自函子。

The Maybe Functor

data Maybe a = Nothing | Just a

类型构造器 Maybe,将类型 a 映射到类型 Maybe a

Maybe without any argument represents a function on types. But can we turn Maybe into a functor? (From now on, when I speak of functors in the context of programming, I will almost always mean endofunctors.) A functor is not only a mapping of objects (here, types) but also a mapping of morphisms (here, functions).

In Haskell, we implement the morphismmapping part of a functor as a higher order function called fmap.

fmap :: (a -> b) -> Maybe a -> Maybe b
fmap _ Nothing = Nothing
fmap f (Just x) = Just (f x)

We often say that fmap lifts a function.

To show that the type constructor Maybe together with the function fmap form a functor, we have to prove that fmap preserves identity and composition.

To prove the functor laws, using equational reasoning.

fmap id = id
fmap (g . f) = fmap g . fmap f

我们可以使用类型类,将 fmap 进一步抽象为:

class Functor f where
fmap :: (a -> b) -> f a -> f b

Maybe 类型构造器成为其实例:

instance Functor Maybe where
fmap _ Nothing = Nothing
fmap f (Just x) = Just (f x)

对应在 C++ 中的实现为 optional

#include <iostream>
#include <functional>
using namespace std;
template<class T>
class optional {
bool _isValid; // the tag
T _v;
public:
optional() : _isValid(false) {} // Nothing
optional(T x) : _isValid(true), _v(x) {} // Just
bool isValid() const { return _isValid; }
T val() const { return _v; }
};
template<class A, class B>
function<optional<B>(optional<A>)>
fmap(function<B(A)> f) {
return [f](optional<A> opt) {
if (!opt.isValid())
return optional<B>{};
else
return optional<B>{ f(opt.val()) };
};
}
template<class A, class B>
optional<B> fmap(function<B(A)> f, optional<A> opt) {
if (!opt.isValid())
return optional<B>{};
else
return optional<B>{ f(opt.val()) };
}
int add(int x) {
return x + 1;
}
int main() {
function<int(int)> f_add = add;
auto src = optional<int>{ 1 };
auto dst = fmap(f_add, src);
if (dst.isValid()) {
cout << dst.val();
}
}

然而在 C++fmap 的进一步抽象比较困难。

The List Functor

Haskell

data List a = Nil | Cons a (List a)
instance Functor List where
fmap _ Nil = Nil
fmap f (Cons x t) = Cons (f x) (fmap f t)

C++

考虑列表为 vector

#include <iostream>
#include <functional>
#include <algorithm>
using namespace std;
template<class A, class B>
vector<B> fmap(function<B(A)> f, vector<A> v) {
vector<B> w;
transform(begin(v), end(v), back_inserter(w), f);
return w;
}
int main() {
vector<int> v{ 1, 2, 3, 4 };
function<int(int)> f_square = [](int i) { return i * i; };
auto w = fmap(f_square, v);
copy(begin(w), end(w), ostream_iterator<int>(cout, ", "));
}

Most C++ containers are functors by virtue of implementing iterators that can be passed to std::transform, which is the more primitive cousin of fmap. Unfortunately, the simplicity of a functor is lost under the usual clutter of iterators and temporaries (see the implementation of fmap above). I’m happy to say that the new proposed C++ range library makes the functorial nature of ranges much more pronounced.

The Reader Functor

Consider a mapping of type a to the type of a function returning a.

fmap :: (a -> b) -> (r -> a) -> (r -> b)

So here’s the implementation of our fmap:

instance Functor ((->) r) where
fmap = (.)

部分应用使其成为类型类的实例。

Functors as Containers

So I like to think of the functor object (an object of the type generated by an endofunctor) as containing a value or values of the type over which it is parameterized, even if these values are not physically present there.

  • C++ std::future
  • Haskell IO object

We are not at all concerned about being able to access the values — that’s totally optional, and outside of the scope of the functor. All we are interested in is to be able to manipulate those values using functions. If the values can be accessed, then we should be able to see the results of this manipulation. If they can’t, then all we care about is that the manipulations compose correctly and that the manipulation with an identity function doesn’t change anything.

Haskell

data Const c a = Const c
instance Functor (Const c) where
fmap _ (Const v) = Const v

其中 fmap 的类型为:

fmap :: (a -> b) -> Const c a -> Const c b

C++

#include <iostream>
#include <functional>
using namespace std;
template<class C, class A>
struct Const {
Const(C v) : _v(v) {}
C _v;
};
template<class C, class A, class B>
Const<C, B> fmap(function<B(A)> f, Const<C, A> c) {
return Const<C, B>{c._v};
}

Despite its weirdness, the Const functor plays an important role in many constructions. In category theory, it’s a special case of the Δ𝑐 functor I mentioned earlier — the endo-functor case of a black hole.

Functor Composition

It’s not hard to convince yourself that functors between categories compose, just like functions between sets compose.

square x = x * x
mis :: Maybe [Int]
mis = Just [1, 2, 3]
mis2 = fmap (fmap square) mis
mis3 = (fmap . fmap) square mis2

It’s pretty obvious that functor composition is associative (the mapping of objects is associative, and the mapping of morphisms is associative). And there is also a trivial identity functor in every category: it maps every object to itself, and every morphism to itself.

在这种范畴中,对象是范畴,而态射是函子。我们称之为 𝐂𝐚𝐭。

A category of all small categories called 𝐂𝐚𝐭 (which is big, so it can’t be a member of itself). A small category is one in which objects form a set, as opposed to something larger than a set.

Ex

考虑 fmap id (Just x) = Nothing ≠ id (Just xx) 即可。

1 fmap id = id
fmap id (r -> a)
= id (r -> a)
2 fmap (g . f) = fmap g . fmap f
fmap ((c -> d) . (b -> c)) (a -> b)
= (c -> d) . (b -> c) . (a -> b)
= (c -> d) . (fmap (b -> c) (a -> b))
= fmap (c -> d) (fmap (b -> c) (a -> b))
= (fmap (c -> d) . fmap (b -> c)) (a -> b)

归纳法证明即可。

Functoriality

Bifunctors

二元函子:

A pair of morphisms is just a single morphism in the product category 𝐂 × 𝐃 to 𝐄.

在类型范畴上定义二元函子,使用 bimap 对两个参数综合考虑:

class Bifunctor f where
bimap :: (a -> c) -> (b -> d) -> f a b -> f c d
bimap g h = first g . second h
first :: (a -> c) -> f a b -> f c b
first g = bimap g id
second :: (b -> d) -> f a b -> f a d
second = bimap id

54af95d663854d99b0023eb9b55cc394.jpg

另一种思考方式是固定一个参数分别考虑,如上面的 firstsecond

In general, separate functoriality is not enough to prove joint functoriality. Categories in which joint functoriality fails are called premonoidal.

当我们声明该类型类的实例时,我们可以实现 bimap 并使用默认的 firstsecond,或实现 firstsecond 并使用默认的 bimap

Product and Coproduct Bifunctors

让积成为 Bifunctor 类型类的实例:

instance Bifunctor (,) where
bimap f g (x, y) = (f x, g y)

让余积成为 Bifunctor 类型类的实例:

instance Bifunctor Either where
bimap f _ (Left x) = Left (f x)
bimap _ g (Right y) = Right (g y)

monoidal category 定义的修正:

I mentioned that 𝐒𝐞𝐭 is a monoidal category with respect to Cartesian product, with the singleton set as a unit. And it’s also a monoidal category with respect to disjoint union, with the empty set as a unit.

What I haven’t mentioned is that one of the requirements for a monoidal category is that the binary operator be a bifunctor.

Functorial Algebraic Data Types

让积和余积的操作数从类型变为函子,以 Maybe 为例:

data Maybe a = Nothing | Just a

原来的定义中是一个类型和一个多态类型。

考虑 Nothing,在同构意义上,它等价于 Const ()。可以证明 Const 是二元函子,回顾一下定义:

data Const c a = Const c
instance Functor (Const c) where
fmap _ (Const v) = Const v

这里我们将其部分应用了。

考虑 Just,在同构意义上,它等价于 Identity,其定义如下:

data Identity a = Identity a
instance Functor Identity where
fmap f (Identity x) = Identity (f x)

这是 𝐂𝐚𝐭 范畴中的恒等态射。

于是,在同构意义上,Maybe 可以定义为:

type Maybe a = Either (Const () a) (Identity a)

So Maybe is the composition of the bifunctor Either with two functors, Const () and Identity.

So it turns out that we didn’t have to prove that Maybe was a functor — this fact followed from the way it was constructed as a sum of two functorial primitives.

将这一过程抽象化,可以得到:

newtype BiComp bf fu gu a b = BiComp (bf (fu a) (gu b))

其中 bf 为二元函子,fugu 为一元函子,ab 为类型。

我们加上类型限制,让其成为 Bifunctor 类型类的实例:

instance (Bifunctor bf, Functor fu, Functor gu) => Bifunctor (BiComp bf fu gu) where
bimap f1 f2 (BiComp x) = BiComp ((bimap (fmap f1) (fmap f2)) x)

其中 x 的类型为 bf (fu a) (gu b),若 f1f2 的类型分别为:

f1 :: a -> a'
f2 :: b -> b'

那么最终结果的类型为 bf (fu a') (gu b')

这里有点费解。

为了使实例化的过程自动化,我们可以在脚本中加入 {-# LANGUAGE DeriveFunctor #-},让编译器自动生成 bimapfmap

{-# LANGUAGE DeriveFunctor #-}
data Tree a = Leaf a | Node (Tree a) (Tree a) deriving Functor

编译器会生成:

instance Functor Tree where
fmap f (Leaf a) = Leaf (f a)
fmap f (Node t t') = Node (fmap f t) (fmap f t')

C++ 中,可以这样实现:

#include <iostream>
#include <functional>
using namespace std;
template<class T>
struct Tree {
virtual ~Tree() {};
};
template<class T>
struct Leaf : public Tree<T> {
T _label;
Leaf(T l) : _label(l) {}
};
template<class T>
struct Node : public Tree<T> {
Tree<T>* _left;
Tree<T>* _right;
Node(Tree<T>* l, Tree<T>* r) : _left(l), _right(r) {}
};
template<class A, class B>
Tree<B>* fmap(function<B(A)> f, Tree<A>* t) {
Leaf<A>* pl = dynamic_cast <Leaf<A>*>(t);
if (pl)
return new Leaf<B>(f(pl->_label));
Node<A>* pn = dynamic_cast <Node<A>*>(t);
if (pn)
return new Node<B>(fmap<A>(f, pn->_left), fmap<A>(f, pn->_right));
return nullptr;
}

此处的 fmap 是非泛型的,其中使用了 dynamic_cast 进行模式匹配。

The Writer Functor

回顾:

type Writer a = (a, String)
(>=>) :: (a -> Writer b) -> (b -> Writer c) -> (a -> Writer c)
m1 >=> m2 = \x ->
let (y, s1) = m1 x
(z, s2) = m2 y
in (z, s1 ++ s2)
return :: a -> Writer a
return x = (x, "")

(>=>) 表示了态射的组合,return 表示了恒等态射。

我们发现 fmap f = id >=> (\x -> return (f x)),这里 id 的类型为 Writer a -> Writer a

Notice that this argument is very general: you can replace Writer with any type constructor. As long as it supports a fish operator and return, you can define fmap as well. So the embellishment in the Kleisli category is always a functor. (Not every functor, though, gives rise to a Kleisli category.)

You might wonder if the fmap we have just defined is the same fmap the compiler would have derived for us with deriving Functor. Interestingly enough, it is. This is due to the way Haskell implements polymorphic functions. It’s called parametric polymorphism, and it’s a source of so called theorems for free. One of those theorems says that, if there is an implementation of fmap for a given type constructor, one that preserves identity, then it must be unique.

The Reader Functor

Reader 有两个类型参数,我们想知道 Reader 的每一个类型参数是否是 functorial 的。

The pair and Either were functorial in both arguments — they were bifunctors.

在上一章的习题中,我们证明了固定 Reader 的参数类型得到的是 Functor 类型类的实例。

我们尝试固定返回参数:

type Op r a = a -> r

此时 fmap 的类型为:

fmap :: (a -> b) -> (a -> r) -> (b -> r)

显然这是不可能实现的。但是若能让 a -> b 变为 b -> a,这就容易实现了。

为此,我们考虑源范畴的对偶范畴与目标范畴之间的态射(函子),𝐹 ∷ 𝐂𝑜𝑝 → 𝐃

e00cc13c036b4241b0b4112723a2fe50.jpg

函子 𝐹 将源范畴的对偶范畴中的态射 𝑓𝑜𝑝 ∷ 𝑎 → 𝑏 映射到目标范畴中的态射 𝐹𝑓𝑜𝑝 ∷ 𝐹 𝑎 → 𝐹 𝑏

注意到对偶范畴中的态射 𝑓𝑜𝑝 ∷ 𝑎 → 𝑏 对应了源范畴的中态射 𝑓 ∷ 𝑏 → 𝑎

现在我们考虑从源范畴到目标范畴之间的态射(函子),𝐺 ∷ 𝐂 → 𝐃

函子 𝐺 将源范畴的中态射 𝑓 ∷ 𝑏 → 𝑎 映射到目标范畴中的态射 𝐺𝑓 ∷ 𝐹 𝑎 → 𝐹 𝑏

我们称函子 𝐺contravariant functor,函子 𝐹covariant functor

Haskell 中,可以这样抽象 contravariant functor

contravariant endofunctor

class Contravariant f where
contramap :: (b -> a) -> (f a -> f b)

我们让 Op 成为其实例:

instance Contravariant (Op r) where
contramap = flip (.)

Profunctors

Reader 而言,第一个参数是逆变的,第二个参数是协变的。

It turns out that, if the target category is 𝐒𝐞𝐭 , such a beast is called a profunctor. Because a contravariant functor is equivalent to a covariant functor from the opposite category, a profunctor is defined as: 𝐂𝑜𝑝 × 𝐃 → 𝐒𝐞𝐭

下面是在 Haskell 中的定义:

class Profunctor p where
dimap :: (a -> b) -> (c -> d) -> p b c -> p a d
dimap f g = lmap f . rmap g
lmap :: (a -> b) -> p b c -> p a c
lmap f = dimap f id
rmap :: (b -> c) -> p a b -> p a c
rmap = dimap id

f776fd5dc5f54de3a10cec0e280e87ec.jpg

我们让 Reader 成为其实例:

instance Profunctor (->) where
dimap ab cd bc = cd . bc . ab
lmap = flip (.)
rmap = (.)

The Hom-Functor

回顾:

A set of morphisms from object 𝑎 to object 𝑏 in a category 𝐂 is called a homset and is written as 𝐂(𝑎 , 𝑏)

𝐂(𝑎 , 𝑏) 是一个函子,𝐂𝑜𝑝 × 𝐂 → 𝐒𝐞𝐭,对范畴中的态射而言:

A morphism in 𝐂𝑜𝑝 × 𝐂 is a pair of morphisms from 𝐂:

ℎ ∈ 𝐂(𝑎 , 𝑏)     \implies 𝑔 ∘ ℎ ∘ 𝑓 ∈ 𝐂(𝑎′ , 𝑏′)

As you can see, the hom-functor is a special case of a profunctor.

这里有点费解。

Ex

1

Show that the data type: data Pair a b = Pair a b is a bifunctor.

For additional credit implement all three methods of Bifunctor and use equational reasoning to show that these definitions are compatible with the default implementations whenever they can be applied.

解读一下题意,我们需要固定一个参数,构造 fmap,并使用 equational reasoning 证明其满足 functor laws

不失一般性,我们固定 bconst,构造 fmap 为:

fmap f (Pair a) const = Pair (f a) const

验证满足 functor laws

1 fmap id = id
fmap id (Pair a) const
= Pair (id a) const
= (Pair a) const
2 fmap (g . f) = fmap g . fmap f
fmap (g . f) (Pair a) const
= Pair ((g . f) a) const
= fmap g (Pair f a) const
= fmap g (fmap f (Pair a) const)
= (fmap g . fmap f) (Pair a) const

additional credit:

data Pair a b = Pair a b
bimap :: (a -> c) -> (b -> d) -> Pair a b -> Pair c d
bimap g h (Pair a b) = Pair (g a) (h b)
first :: (a -> c) -> Pair a b -> Pair c b
first g (Pair a b) = Pair (g a) b
second :: (b -> d) -> Pair a b -> Pair a d
second h (Pair a b) = Pair a (h b)

之后只需要证明如下等式即可:

bimap g h = first g . second h
first g = bimap g id
second = bimap id

2

Show the isomorphism between the standard definition of Maybe and this desugaring:

type Maybe' a = Either (Const () a) (Identity a)

Hint: Define two mappings between the two implementations.

For additional credit, show that they are the inverse of each other using equational reasoning.

data Const c a = Const c
data Identity a = Identity a
data Maybe a = Nothing | Just a
type Maybe' a = Either (Const () a) (Identity a)
to :: Maybe' a -> Maybe a
to (Left (Const ())) = Nothing
to (Right (Identity a)) = Just a
from :: Maybe a -> Maybe' a
from Nothing = Left (Const ())
from (Just a) = Right (Identity a)

注意这里 Const () 不能 写成 Const () a,前者是值构造器,后者是类型构造器。

之后证明 from ∘ to = idto ∘ from = id 即可。

3

Let’s try another data structure. I call it a PreList because it’s a precursor to a List. It replaces recursion with a type parameter b: data PreList a b = Nil | Cons a b. You could recover our earlier definition of a List by recursively applying PreList to itself (we’ll see how it’s done when we talk about fixed points). Show that PreList is an instance of Bifunctor.

类似第一题,只不过多了一种模式匹配的讨论。

4

Show that the following data types define bifunctors in a and b:

data K2 c a b = K2 c
data Fst a b = Fst a
data Snd a b = Snd b

For additional credit, check your solutions against Conor McBride’s paper Clowns to the Left of me, Jokers to the Right.

5

Define a bifunctor in a language other than Haskell. Implement bimap for a generic pair in that language.

不会 C++ 🤣

6

Should std::map be considered a bifunctor or a profunctor in the two template arguments Key and T? How would you redesign this data type to make it so?

应该为 profunctor。直观上,对键映射应该是先作用后 map,对值映射应该是先 map 后作用:

instance Profunctor map where
lmap f map = \x -> map (f x)
rmap g map = \x -> g (map x)

Function Types

在 𝐒𝐞𝐭 范畴中,hom-set 是 𝐒𝐞𝐭 范畴中的对象(自引用)。

而在有些范畴中,hom-set 并非是该范畴中的对象。

They are called external hom-sets.

我们可以通过 universal construction 在范畴中构造 hom-set

Such objects are called internal hom-sets.

Universal Construction

We will need a pattern that involves three objects: the function type that we are constructing, the argument type, and the result type.

记函数对象(候选)为 𝑧,参数对象为 𝑎,返回为 𝑏

若为 𝐒𝐞𝐭 范畴,我们可以取 𝑓∈𝑧𝑥∈𝑎,将 𝑓𝑥 映射到类型 𝑏 中,即 𝑓𝑥∈𝑏

一般的,我们考虑函数对象和参数对象的积:

So that’s the pattern: a product of two objects 𝑧 and 𝑎 connected to another object 𝑏 by a morphism 𝑔.

9f834aaf2fe9436ebb9e2ccda1a392d7.jpg

There is no function type, if there is no product type.

4a32f799b72444a0a590edf811439503.jpg

Given the morphism ℎ ∷ 𝑧′ → 𝑧 , we want to close the diagram that has both 𝑧′ and 𝑧 crossed with 𝑎. What we really need, given the mapping ℎ from 𝑧′ to 𝑧 , is a mapping from 𝑧′ × 𝑎 to 𝑧 × 𝑎. And now, after discussing the functoriality of the product, we know how to do it. Because the product itself is a functor (more precisely an endo-bi-functor), it’s possible to lift pairs of morphisms. In other words, we can define not only products of objects but also products of morphisms.

Since we are not touching the second component of the product 𝑧′ × 𝑎 , we will lift the pair of morphisms (ℎ , id), where id is an identity on 𝑎.

𝑔′ = 𝑔 ∘ (ℎ × id)

我们称在这种 ranking 下最好的 𝑧𝑎 ⇒ 𝑏,对应的态射 𝑔𝑒𝑣𝑎𝑙。正式的定义如下:

A function object from 𝑎 to 𝑏 is an object 𝑎 ⇒ 𝑏 together with the morphism 𝑒𝑣𝑎𝑙 ∷ ((𝑎 ⇒ 𝑏) × 𝑎) → 𝑏 such that for any other object 𝑧 with a morphism 𝑔 ∷ 𝑧 × 𝑎 → 𝑏, there is a unique morphism ℎ ∷ 𝑧 → (𝑎 ⇒ 𝑏) that factors 𝑔 through 𝑒𝑣𝑎𝑙 : 𝑔 = 𝑒𝑣𝑎𝑙 ∘ (ℎ × id).

注:

Currying

由函数对象的定义可知,对任意对象 𝑧 和态射 𝑔 ∷ 𝑧 × 𝑎 → 𝑏,总存在唯一的态射 ℎ ∷ 𝑧 → (𝑎 ⇒ 𝑏),使得可以通过 𝑒𝑣𝑎𝑙 分解 𝑔

在 𝐒𝐞𝐭 范畴中,这意味着每个二元函数都对应着接受一个参数返回一个函数的函数,这种一一对应被称为 currying

Haskell 中,柯里化可以表示为:

curry :: ((a, b) -> c) -> (a -> b -> c)
curry f a b = f (a, b)
uncurry :: (a -> b -> c) -> ((a, b) -> c)
uncurry f (a, b) = f a b

Notice that curry is the factorizer for the universal construction of the function object. This is especially apparent if it’s rewritten in this form:

factorizer :: ((a, b) -> c) -> (a -> (b -> c))
factorizer g = \a -> (\b -> g (a, b))

(As a reminder: A factorizer produces the factorizing function from a candidate.)

C++ 中,我们可以使用 std::bind

#include <iostream>
#include <functional>
using namespace std::placeholders;
std::string catstr(std::string s1, std::string s2) {
return s1 + s2;
}
int main() {
auto greet = std::bind(catstr, "Hello ", _1);
std::cout << greet("Haskell Curry");
}

Exponentials

In mathematical literature, the function object, or the internal hom-object between two objects 𝑎 and 𝑏, is often called the exponential and denoted by 𝑏𝑎𝑏 ^ 𝑎.

对于在有限集上的函数而言,理论上我们可以将函数转换为一种数据结构,即函数对象。

This is the essence of the equivalence between functions, which are morphisms, and function types, which are objects.

Cartesian Closed Categories

  1. The terminal object
  2. A product of any pair of objects
  3. An exponential for any pair of objects
  4. the initial object
  5. A coproduct of any pair of objects
  6. Product can be distributed over coproduct

满足 1-3 的范畴被称为 Cartesian Closed Categories,𝐒𝐞𝐭 范畴便是其中一个例子。

What’s interesting about Cartesian closed categories from the perspective of computer science is that they provide models for the simply typed lambda calculus, which forms the basis of all typed programming languages.

满足 1-6 的范畴被称为 Bicartesian Closed Categories

Bicartesian Closed Categories 中,我们如下的一一对应:

algebracategory theory
zeroinitial objects
onefinal objects
sumscoproducts
productsproducts
exponentialsexponentials

现在我们还无法证明这一点,但是我们可以在 𝐒𝐞𝐭 范畴中理解这种对应:

证明可参见 Reason Isomorphically!

a0=1a^0=1

By the definition of the initial object, there is exactly one such morphism, so the hom-set 𝐂(0, 𝑎) is a singleton set. A singleton set is the terminal object in 𝐒𝐞𝐭.

Haskell 中,对应了 absurd :: Void -> a

1a=11^a = 1

By the definition of the terminal object, there is a unique morphism from any object to the terminal object. In general, the internal hom-object from 𝑎 to the terminal object is isomorphic to the terminal object itself.

Haskell 中,对应了 unit :: a -> ()

a1=aa^1=a

Morphisms from the terminal object can be used to pick “elements” of the object a. The set of such morphisms is isomorphic to the object itself.

Haskell 中,对应了 () -> a

ab+c=ab×aca^{b+c}=a^b×a^c

The exponential from a coproduct of two objects is isomorphic to a product of two exponentials.

Haskell 中,对应了在余积上进行模式匹配(一对函数):

f :: Either Int Double -> String
f (Left n) = if n < 0 then "Negative int" else "Positive int"
f (Right x) = if x < 0.0 then "Negative double" else "Positive double"
(ab)c=ab×c(a^b)^c=a^{b×c}

A function returning a function is equivalent to a function from a product (a two-argument function).

Haskell 中,对应了柯里化。

(a×b)c=ac×bc(a×b)^c=a^c×b^c

In Haskell: A function returning a pair is equivalent to a pair of functions, each producing one element of the pair.

Curry-Howard Isomorphism

函数对象对应逻辑中的     \implies

According to the Curry-Howard isomorphism, every type can be interpreted as a proposition — a statement or a judgment that may be true or false. Such a proposition is considered true if the type is inhabited and false if it isn’t. In particular, a logical implication is true if the function type corresponding to it is inhabited, which means that there exists a function of that type. An implementation of a function is therefore a proof of a theorem. Writing programs is equivalent to proving theorems.

Coq

来看几个例子:

((𝑎 ⇒ 𝑏) ∧ 𝑎) ⇒ 𝑏

我们可以通过实现 𝑒𝑣𝑎𝑙 方法来证明:

eval :: ((a -> b), a) -> b
eval (f, x) = f x

𝑎 ∨ 𝑏 ⇒ 𝑎

我们无法实现以 Either a b -> a 为函数签名的函数,因为在 Right 中我们无法产生 a

𝑓𝑎𝑙𝑠𝑒 ⇒ 𝑎

下面是一种实现:

newtype Void = Void Void
absurd (Void a) = absurd a

As always, the type Void is tricky. This definition makes it impossible to construct a value because in order to construct one, you would need to provide one. Therefore, the function absurd can never be called.