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
- Composition is associative.
- For every object 𝐴 there is an arrow which is a unit 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++
对于函数组合,不太会 🤣
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
可能会返回 True
、False
或 ⊥
。
我们还可以显式地返回 ⊥
,例如在 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
。
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
中记作 ()
。若该类型作为参数类型:
在 Haskell
中:
Functions from unit to any type 𝐴 are in one-to-one correspondence with the elements of that set 𝐴.
若该类型作为返回值类型,我们让参数成为多态类型:
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
中:
双元集对应的类型为 bool
,在 Haskell
中可以这样实现:
对于
C++
,考虑使用枚举类
- Pure functions from Bool just pick two values from the target type, one corresponding to True and another to False.
- Functions to Bool are called predicates.
Functions
函数有纯与不纯之分。没有副作用的函数被称为纯函数。
通过引入数学模型,我们可以用数学对象来形式化程序的语义,给出程序的正确性证明。
由于数学函数都是纯函数,在这样的程序中,我们无法表达副作用。
然而,范畴论指出计算效应(副作用)可以通过映射到单子上实现。
Ex
- 纯函数与记忆化(遇到相同参数直接返回存储的值),下面是两个非纯函数,也就不能被记忆化:
- Draw a picture of a category whose only objects are the types Void, () (unit), and Bool; with arrows corresponding to all possible functions between these types. Label the arrows with the names of the functions.
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
中可以这样实现:
幺半群的实例:
对这里的 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
关键是我们要将之前的集合看作一个整体的对象。
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
可以换成任意满足幺半群性质的类型。
对应的恒等态射为:
注:书上
compose
的另一种实现似乎行不通。
Haskell
对应的恒等态射为:
注:另见 Haskell 趣学指南第二部分中
Writer monad
部分。
Ex
取倒数,开平方
简单来说,态射的组合就是标志位取与,函数组合。恒等态射就是标志位为 true
,函数为恒等函数。
另见 Fast Inverse Square Root — A Quake III Algorithm:
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.
容易证明上面的两个初始对象是 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.
- pattern
- ranking
举个例子,考虑 Int
和 Bool
的积,Int
是一个候选,因为它满足 pattern
:
我们发现存在从 Int
(图中的 c'
)到 (Int, Bool)
(图中的 c
)的态射,使得:
可以认为
m
为p'
和q'
的公因式。
这样的态射为:
然而,我们可以证明不存在从 (Int, Bool)
到 Int
的态射,满足上述条件。
There is no way to factorize
fst
andsnd
.
另一个候选是 (Int, Int, Bool)
,满足 pattern
:
存在从 (Int, Int, Bool)
(图中的 c'
)到 (Int, Bool)
(图中的 c
)的态射:
反过来,我们发现存在不止一种从 (Int, Bool)
到 Int
的态射,满足上述条件。
There is more than one way to factorize
fst
andsnd
.
总结一下,积的定义为:
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:
余积的定义与之完全对偶。
在 Haskell
中,积为序对,余积为 Either
:
对应的 factorizer 为:
Asymmetry
The category of sets is not symmetric with respect to the inversion of arrows.
- Notice that while the empty set has a unique morphism to any set (the absurd function), it has no morphisms coming back.
- The singleton set has a unique morphism coming to it from any set, but it also has outgoing morphisms to every set (except for the empty one). As we’ve seen before, these outgoing morphisms from the terminal object play a very important role of picking elements of other sets (the empty set has no elements, so there’s nothing to pick).
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
关于余积的一些练习:
- Show that
Either
is a “better” coproduct thanint
equipped with two injections:
使用 Haskell
:
- Continuing the previous problem: How would you argue that
int
with the two injections i and j cannot be “better” thanEither
?
取 a
为 1
,b
为 false
,此时 c
为 1
,而 c'
可能为 Left 1
,也可能为 RIght false
,这与函数的定义矛盾。
- Still continuing: What about these injections?
考虑整数的溢出即可。
- Come up with an inferior candidate for a coproduct of int and bool that cannot be better than Either because it allows multiple acceptable morphisms from it to Either.
Consider some type SuperEither
defined as:
We can define injections into this type from int
and bool
of the forms:
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):
将序对嵌套在序对里就构成了多元组。
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.
在同构意义下,我们可以将序对运算视为一个幺半群:
其单位元为
()
,因为在同构意义下,(a, ())
与a
等价:
总结来说:
𝐒𝐞𝐭 (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
中,积也可以这样表示:
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
:
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 Void
与 a
同构。
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++.
等价于:
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:
等价于:
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
中:
在 C++
中:
由于 Haskell
的数据结构是不可变的,所以这种构造是可逆的:
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
将积和余积组合,一图胜千言:
满足分配律,也就是说 (a, Either b c)
与 Either (a, b) (a, c)
同构。这表明这是一个半环。
回到列表数据类型:
我们使用代数表示:,不断替换 可得:,这描述了列表自身。
注意到积对应了 and
,而余积对应了 or
,所以我们还有下面的映射关系:
This is the basis of the Curry-Howard isomorphism between logic and type theory.
Ex
Here’s a sum type defined in Haskell:
When we want to define a function like area that acts on a Shape
, we do it by pattern matching on the two constructors:
Implement Shape
in C++ or Java as an interface and create two classes: Circle
and Rect
. Implement area as a virtual function.
C++
添加一个新的方法(难),添加一个新的类型(易)。
Haskell
添加一个新的方法(易),添加一个新的类型(难)。
Functors
函子是范畴之间的映射:
- 对象
- 态射
函子保持了范畴的内在结构(态射):
- 组合:若
ℎ = 𝑔.𝑓
,则𝐹 ℎ = 𝐹 𝑔 . 𝐹 𝑓
- 恒等:
𝐹 id 𝑎 = id 𝐹𝑎
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.
- 源范畴中只有一个对象:select
- 目标范畴中只有一个对象:black hole
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
类型构造器 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.
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
进一步抽象为:
让 Maybe
类型构造器成为其实例:
对应在 C++
中的实现为 optional
:
然而在 C++
中 fmap
的进一步抽象比较困难。
The List Functor
Haskell
C++
考虑列表为 vector
:
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.
So here’s the implementation of our 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
其中 fmap
的类型为:
C++
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.
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
- Can we turn the
Maybe
type constructor into a functor by defining:fmap _ _ = Nothing
which ignores both of its arguments? (Hint: Check the functor laws.)
考虑 fmap id (Just x) = Nothing ≠ id (Just xx)
即可。
- Prove functor laws for the reader functor. (Hint: it’s really simple.)
- Prove the functor laws for the list functor. Assume that the laws are true for the tail part of the list you’re applying it to (in other words, use induction).
归纳法证明即可。
Functoriality
Bifunctors
二元函子:
- 对象:mapping a pair of objects, one from category 𝐂 , and one from category 𝐃 , to an object in category 𝐄.
- 态射:mapping a pair of morphisms, one from 𝐂 and one from 𝐃 , to a morphism in 𝐄.
A pair of morphisms is just a single morphism in the product category 𝐂 × 𝐃 to 𝐄.
- 组合:
(𝑓, 𝑔) ∘ (𝑓′, 𝑔′) = (𝑓 ∘ 𝑓′, 𝑔 ∘ 𝑔′)
- 恒等:
(id, id)
在类型范畴上定义二元函子,使用 bimap
对两个参数综合考虑:
另一种思考方式是固定一个参数分别考虑,如上面的 first
和 second
。
In general, separate functoriality is not enough to prove joint functoriality. Categories in which joint functoriality fails are called premonoidal.
当我们声明该类型类的实例时,我们可以实现 bimap
并使用默认的 first
和 second
,或实现 first
和 second
并使用默认的 bimap
。
Product and Coproduct Bifunctors
让积成为 Bifunctor
类型类的实例:
让余积成为 Bifunctor
类型类的实例:
对 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
为例:
原来的定义中是一个类型和一个多态类型。
考虑 Nothing
,在同构意义上,它等价于 Const ()
。可以证明 Const
是二元函子,回顾一下定义:
这里我们将其部分应用了。
考虑 Just
,在同构意义上,它等价于 Identity
,其定义如下:
这是 𝐂𝐚𝐭 范畴中的恒等态射。
于是,在同构意义上,Maybe
可以定义为:
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.
将这一过程抽象化,可以得到:
其中 bf
为二元函子,fu
和 gu
为一元函子,a
和 b
为类型。
我们加上类型限制,让其成为 Bifunctor
类型类的实例:
其中 x
的类型为 bf (fu a) (gu b)
,若 f1
和 f2
的类型分别为:
那么最终结果的类型为 bf (fu a') (gu b')
。
这里有点费解。
为了使实例化的过程自动化,我们可以在脚本中加入 {-# LANGUAGE DeriveFunctor #-}
,让编译器自动生成 bimap
或 fmap
:
编译器会生成:
在 C++
中,可以这样实现:
此处的 fmap
是非泛型的,其中使用了 dynamic_cast
进行模式匹配。
The Writer Functor
回顾:
(>=>)
表示了态射的组合,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
类型类的实例。
我们尝试固定返回参数:
此时 fmap
的类型为:
显然这是不可能实现的。但是若能让 a -> b
变为 b -> a
,这就容易实现了。
为此,我们考虑源范畴的对偶范畴与目标范畴之间的态射(函子),𝐹 ∷ 𝐂𝑜𝑝 → 𝐃
。
函子 𝐹
将源范畴的对偶范畴中的态射 𝑓𝑜𝑝 ∷ 𝑎 → 𝑏
映射到目标范畴中的态射 𝐹𝑓𝑜𝑝 ∷ 𝐹 𝑎 → 𝐹 𝑏
。
注意到对偶范畴中的态射 𝑓𝑜𝑝 ∷ 𝑎 → 𝑏
对应了源范畴的中态射 𝑓 ∷ 𝑏 → 𝑎
。
现在我们考虑从源范畴到目标范畴之间的态射(函子),𝐺 ∷ 𝐂 → 𝐃
。
函子 𝐺
将源范畴的中态射 𝑓 ∷ 𝑏 → 𝑎
映射到目标范畴中的态射 𝐺𝑓 ∷ 𝐹 𝑎 → 𝐹 𝑏
。
我们称函子 𝐺
为 contravariant functor,函子 𝐹
为 covariant functor。
在 Haskell
中,可以这样抽象 contravariant functor:
contravariant endofunctor
我们让 Op
成为其实例:
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
中的定义:
我们让 Reader
成为其实例:
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 𝐂:
𝑓 ∷ 𝑎′ → 𝑎
𝑔 ∷ 𝑏 → 𝑏′
ℎ ∈ 𝐂(𝑎 , 𝑏)
𝑔 ∘ ℎ ∘ 𝑓 ∈ 𝐂(𝑎′ , 𝑏′)
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。
不失一般性,我们固定 b
为 const
,构造 fmap
为:
验证满足 functor laws:
additional credit:
之后只需要证明如下等式即可:
2
Show the isomorphism between the standard definition of
Maybe
and this desugaring:Hint: Define two mappings between the two implementations.
For additional credit, show that they are the inverse of each other using equational reasoning.
注意这里
Const ()
不能 写成Const () a
,前者是值构造器,后者是类型构造器。
之后证明 from ∘ to = id
和 to ∘ 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 parameterb
:data PreList a b = Nil | Cons a b
. You could recover our earlier definition of aList
by recursively applyingPreList
to itself (we’ll see how it’s done when we talk about fixed points). Show thatPreList
is an instance ofBifunctor
.
类似第一题,只不过多了一种模式匹配的讨论。
4
Show that the following data types define bifunctors in
a
andb
:For additional credit, check your solutions against Conor McBride’s paper Clowns to the Left of me, Jokers to the Right.
K2
:- Without loss of generality, if we hold
b
constant, thenK2
becomesConst
, which is a functor
- Without loss of generality, if we hold
Fst
:- If we hold
a
constant, thenFst
becomesConst
, which is a functor - If we hold
b
constant, thenFst
becomesIdentity
, which is a functor
- If we hold
Snd
:- If we hold
a
constant, thenSnd
becomesIdentity
, which is a functor - If we hold
b
constant, thenSnd
becomesConst
, which is a functor
- If we hold
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 argumentsKey
andT
? How would you redesign this data type to make it so?
应该为 profunctor
。直观上,对键映射应该是先作用后 map
,对值映射应该是先 map
后作用:
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
- pattern
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 𝑔.
There is no function type, if there is no product type.
- ranking
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)
.
注:
- 并不保证函数对象一定存在
- 在 𝐒𝐞𝐭 范畴中,函数对象与 hom-set 同构
Currying
由函数对象的定义可知,对任意对象 𝑧
和态射 𝑔 ∷ 𝑧 × 𝑎 → 𝑏
,总存在唯一的态射 ℎ ∷ 𝑧 → (𝑎 ⇒ 𝑏)
,使得可以通过 𝑒𝑣𝑎𝑙
分解 𝑔
。
在 𝐒𝐞𝐭 范畴中,这意味着每个二元函数都对应着接受一个参数返回一个函数的函数,这种一一对应被称为 currying:
ℎ
为𝑔
的柯里化版本𝑔
为ℎ
的反柯里化版本
在 Haskell
中,柯里化可以表示为:
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:
(As a reminder: A factorizer produces the factorizing function from a candidate.)
在 C++
中,我们可以使用 std::bind
:
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
- The terminal object
- A product of any pair of objects
- An exponential for any pair of objects
- the initial object
- A coproduct of any pair of objects
- 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 中,我们如下的一一对应:
algebra | category theory |
---|---|
zero | initial objects |
one | final objects |
sums | coproducts |
products | products |
exponentials | exponentials |
现在我们还无法证明这一点,但是我们可以在 𝐒𝐞𝐭 范畴中理解这种对应:
证明可参见 Reason Isomorphically!
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
。
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 -> ()
。
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
。
The exponential from a coproduct of two objects is isomorphic to a product of two exponentials.
在 Haskell
中,对应了在余积上进行模式匹配(一对函数):
A function returning a function is equivalent to a function from a product (a two-argument function).
在 Haskell
中,对应了柯里化。
In Haskell: A function returning a pair is equivalent to a pair of functions, each producing one element of the pair.
Curry-Howard Isomorphism
函数对象对应逻辑中的 。
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
来看几个例子:
- modus ponens
((𝑎 ⇒ 𝑏) ∧ 𝑎) ⇒ 𝑏
我们可以通过实现 𝑒𝑣𝑎𝑙
方法来证明:
- false statement
𝑎 ∨ 𝑏 ⇒ 𝑎
我们无法实现以 Either a b -> a
为函数签名的函数,因为在 Right
中我们无法产生 a
。
- ex falso quodlibet
𝑓𝑎𝑙𝑠𝑒 ⇒ 𝑎
下面是一种实现:
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.