编程视角下的范畴和函子

函数式编程语言ML

ML的类型系统
- 自定义类型datatype
- 抽象类型abstype
- 高阶函数
- 多态
类型构造
- 并集（|）
- 乘积（*）
- 类型构造器（Type Constructor）
自定义类型datatype
- 常量（Constant）
- 非常量（Non-constant）
- 递归（Recursive）
- 一对（Pair）
  - 类型构造器
  - 实例化
  - 多态
- 线性列表（Linear List）
  - 类似于自由幺半群，0个元素（nil）或者以上（’a :: (‘a list)）

// Constant
datatype Color = red | blue | green

fun warm(red) = true
    | warm(blue) = false
    | warm(green) = false

// Non-constant
datatype Plant = flower of string*int*Color
    | foliage of string*int

fun height(flower(_, n, _)) = n
    | height(foliage(_, n)) = n

// Recursive
datatype Num = zero | succ of Num

fun even(zero) = true
    | even(succ(n)) = not(even(n))

// Pair
// 1. Type constructor
datatype 'a Pair = pair of ('a * 'a)

// 2. Instantiation
pair(3, 4) : int Pair
pair(true, false) : bool Pair

// 3. Polymorphism
fun first(pair(x, y)) = x
first : 'a Pair -> 'a

// Linear list
datatype 'a list = nil | 'a :: ('a list)

fun length nil = 0
    | length (h :: t) = 1 + length(t)

fun member(e, nil) = false
    | member(e, (h :: t)) = if e = h then true else member(e, t)

使用ML表示范畴

关于范畴、函子，可参见范畴的定义
对象、态射
- 对象（Object），比如 $A$
- 箭头（Arrow），比如 $f: A \to B$
四个函数
- 源（Source），比如 $s(f) = A$
- 目的（Target），比如 $t(f) = B$
- 恒等（Identity），比如 $id_A$
- 复合（Composition），比如 $gf$
使用ML表示范畴
- 对象的类型为’o，箭头的类型为’a
- 源、目的 –> 给定箭头，得到对象（’a -> ‘o）
- 恒等 –> 给定对象，得到箭头（’o -> ‘a）
- 复合 –> 给定两个箭头，得到箭头（’a * ‘a -> ‘a）
- 最终，使用类型构造器，得到范畴

// Types of objects and arrows
'o, 'a

// Types of source, target, identity, composition
'a -> 'o, 'a -> 'o, 'o -> 'a, 'a * 'a -> 'a

// Type constructor of category
datatype ('o, 'a) Cat =
    cat of ('a -> 'o) * ('a -> 'o) * ('o -> 'a) * ('a * 'a -> 'a)

范畴的例子——有限集的范畴

有限集的范畴FinSet
- 对象为有限集，通常可以表示为线性列表
  - 类型为’a Set
- 态射为有限集之间的映射，通常可以表示为三元组
  - 类型为’a Set_Arrow
- 四个函数
  - 恒等、复合使用了Lambda演算的记号，比如fn x => f(x)
  - 如果两个映射无法复合，那么抛出异常non_composable_pair
- 最终，使用四个函数进行实例化，得到有限集的范畴FinSet
  - 类型为(‘a Set, ‘a Set_Arrow) Cat

// Type of objects
'a Set

// Type of arrows
datatype 'a Set_Arrow =
    set_arrow of ('a Set) * ('a -> 'a) * ('a Set)

// Source, target, identity, composition
fun set_s(set_arrow(a, _, _)) = a
fun set_t(set_arrow(_, _, b)) = b

fun set_ident(a) = set_arrow(a, fn x => x, a)

fun set_comp(set_arrow(c, g, d), set_arrow(a, f, b)) =
    if seteq(b, c) then
        set_arrow(a, fn x => g(f(x)), d)
    else
        raise non_composable_pair

// FinSet
val FinSet = cat(set_s, set_t, set_ident, set_comp)
FinSet : ('a Set, 'a Set_Arrow) Cat

函数式编程语言ML

使用ML表示范畴

范畴的例子——有限集的范畴

使用ML表示函子