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++
#include<iostream>
template<classT> Tid(Tx) { return x; }
intadd(inti) {
return i +1;
}
intmain() {
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.
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 中记作 ()。若该类型作为参数类型:
intf44() { return44; }
在 Haskell 中:
f44 :: () -> Integer
f44 () = 44
Functions from unit to any type 𝐴 are in one-to-one correspondence with the elements of that set 𝐴.
若该类型作为返回值类型,我们让参数成为多态类型:
template<classT>
voidunit(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 中可以这样实现:
dataBool = True | False
对于 C++,考虑使用枚举类
Pure functions from Bool just pick two values from the target type, one corresponding to True and another to False.
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 中可以这样实现:
classMonoidmwhere
mempty :: m
mappend :: m -> m -> m
幺半群的实例:
instanceMonoidStringwhere
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
关键是我们要将之前的集合看作一个整体的对象。
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.)
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
容易证明上面的两个初始对象是 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.
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)
余积的定义与之完全对偶。
在 Haskell 中,积为序对,余积为 Either:
dataEitherab = Lefta | Rightb
对应的 factorizer 为:
factorizer :: (a -> c) -> (b -> c) -> Eitherab -> 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.
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 than int equipped with two injections:
inti(intn) { return n; }
intj(boolb) { return b ?0:1; }
使用 Haskell:
i :: Int -> Int
i n = n
j :: Bool -> Int
j b = if b then0else1
m :: EitherIntBool -> Int
m (Left x) = x
m (Right y) = if y then0else1
Continuing the previous problem: How would you argue that int with the two injections i and j cannot be “better” than Either?
取 a 为 1,b 为 false,此时 c 为 1,而 c' 可能为 Left 1,也可能为 RIght false,这与函数的定义矛盾。
Still continuing: What about these injections?
inti(intn) {
if (n <0) return n;
return n +2;
}
intj(boolb) { return b ?0:1; }
考虑整数的溢出即可。
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.
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 中,积也可以这样表示:
dataPairab = Pairab
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:
dataEitherab = Lefta | Rightb
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++.
dataColor = 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:
dataMaybea = Nothing | Justa
等价于:
dataMaybea = 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 中:
dataLista = Nil | Consa (Lista)
在 C++ 中:
template<classA>
classList {
Node<A>* _head;
public:
List() : _head(nullptr) {} // Nil
List(Aa, List<A> l) // Cons
: _head(newNode<A>(a, l))
{}
};
由于 Haskell 的数据结构是不可变的,所以这种构造是可逆的:
maybeTail :: Lista -> Maybe (Lista)
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
将积和余积组合,一图胜千言:
满足分配律,也就是说 (a, Either b c) 与 Either (a, b) (a, c) 同构。这表明这是一个半环。
回到列表数据类型:
dataLista = Nil | Consa (Lista)
我们使用代数表示:x=1+a∗x,不断替换 x 可得:x=1+a+a∗a+a∗a∗a+...,这描述了列表自身。
注意到积对应了 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:
dataShape = CircleFloat | RectFloatFloat
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>
usingnamespacestd;
classShape {
public:
virtualdoublearea() =0;
};
classCircle : publicShape {
private:
double r;
public:
Circle(double_r) :r(_r) {}
doublearea() {
return M_PI * r * r;
}
};
classRect : publicShape {
private:
double d;
double h;
public:
Rect(double_d, double_h) :d(_d), h(_h) {}
doublearea() {
return d * h;
}
};
intmain() {
unique_ptr<Shape> p =make_unique<Circle>(1);
cout <<p->area() << endl;
p =make_unique<Rect>(1, 2);
cout <<p->area() << endl;
}
添加一个新的方法(难),添加一个新的类型(易)。
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
dataMaybea = Nothing | Justa
类型构造器 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) -> Maybea -> Maybeb
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.
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:
instanceFunctor ((->) 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
dataConstca = Constc
instanceFunctor (Constc) where
fmap _ (Const v) = Const v
其中 fmap 的类型为:
fmap :: (a -> b) -> Constca -> Constcb
C++
#include<iostream>
#include<functional>
usingnamespacestd;
template<classC, classA>
structConst {
Const(Cv) : _v(v) {}
C _v;
};
template<classC, classA, classB>
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
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.)
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)
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 对两个参数综合考虑:
classBifunctorfwhere
bimap :: (a -> c) -> (b -> d) -> fab -> fcd
bimap g h = first g . second h
first :: (a -> c) -> fab -> fcb
first g = bimap g id
second :: (b -> d) -> fab -> fad
second = bimap id
另一种思考方式是固定一个参数分别考虑,如上面的 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 类型类的实例:
instanceBifunctor (,) where
bimap f g (x, y) = (f x, g y)
让余积成为 Bifunctor 类型类的实例:
instanceBifunctorEitherwhere
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.
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.
将这一过程抽象化,可以得到:
newtypeBiCompbffuguab = BiComp (bf (fua) (gub))
其中 bf 为二元函子,fu 和 gu 为一元函子,a 和 b 为类型。
我们加上类型限制,让其成为 Bifunctor 类型类的实例:
instance (Bifunctorbf, Functorfu, Functorgu) => Bifunctor (BiCompbffugu) where
(>=>) :: (a -> Writerb) -> (b -> Writerc) -> (a -> Writerc)
m1 >=> m2 = \x ->
let (y, s1) = m1 x
(z, s2) = m2 y
in (z, s1 ++ s2)
return :: a -> Writera
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.
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 中的定义:
classProfunctorpwhere
dimap :: (a -> b) -> (c -> d) -> pbc -> pad
dimap f g = lmap f . rmap g
lmap :: (a -> b) -> pbc -> pac
lmap f = dimap f id
rmap :: (b -> c) -> pab -> pac
rmap = dimap id
我们让 Reader 成为其实例:
instanceProfunctor (->) 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 𝐂:
𝑓 ∷ 𝑎′ → 𝑎
𝑔 ∷ 𝑏 → 𝑏′
ℎ ∈ 𝐂(𝑎 , 𝑏)⟹𝑔 ∘ ℎ ∘ 𝑓 ∈ 𝐂(𝑎′ , 𝑏′)
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.
Show the isomorphism between the standard definition of Maybe and this desugaring:
typeMaybe'a = Either (Const () a) (Identitya)
Hint: Define two mappings between the two implementations.
For additional credit, show that they are the inverse of each other using equational reasoning.
dataConstca = Constc
dataIdentitya = Identitya
dataMaybea = Nothing | Justa
typeMaybe'a = Either (Const () a) (Identitya)
to :: Maybe'a -> Maybea
to (Left (Const())) = Nothing
to (Right (Identity a)) = Just a
from :: Maybea -> Maybe'a
from Nothing = Left (Const())
from (Just a) = Right (Identity a)
注意这里 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 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:
Without loss of generality, if we hold b constant, then K2 becomes Const, which is a functor
Fst:
If we hold a constant, then Fst becomes Const, which is a functor
If we hold b constant, then Fst becomes Identity, which is a functor
Snd:
If we hold a constant, then Snd becomes Identity, which is a functor
If we hold b constant, then Snd becomes Const, which is a functor
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?
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 𝑎.
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).
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>
usingnamespace std::placeholders;
std::stringcatstr(std::strings1, std::strings2) {
return s1 + s2;
}
intmain() {
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 ba.
对于在有限集上的函数而言,理论上我们可以将函数转换为一种数据结构,即函数对象。
This is the essence of the equivalence between functions, which are morphisms, and function types, which are objects.
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.
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=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=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×ac
The exponential from a coproduct of two objects is isomorphic to a product of two exponentials.
在 Haskell 中,对应了在余积上进行模式匹配(一对函数):
f :: EitherIntDouble -> String
f (Left n) = if n < 0then"Negative int"else"Positive int"
f (Right x) = if x < 0.0then"Negative double"else"Positive double"
(ab)c=ab×c
A function returning a function is equivalent to a function from a product (a two-argument function).
在 Haskell 中,对应了柯里化。
(a×b)c=ac×bc
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
((𝑎 ⇒ 𝑏) ∧ 𝑎) ⇒ 𝑏
我们可以通过实现 𝑒𝑣𝑎𝑙 方法来证明:
eval :: ((a -> b), a) -> b
eval (f, x) = f x
false statement
𝑎 ∨ 𝑏 ⇒ 𝑎
我们无法实现以 Either a b -> a 为函数签名的函数,因为在 Right 中我们无法产生 a。
ex falso quodlibet
𝑓𝑎𝑙𝑠𝑒 ⇒ 𝑎
下面是一种实现:
newtypeVoid = VoidVoid
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.