对类型进行加减乘除运算! -- 为什么 Ocaml 中元组是 int * int 而不是 (int, int)

•
ML类型系统范畴论编程语言设计

最近了解了一下 Ocaml 这门语言, 感觉没什么特别的, 但是在看它的类型系统的时候, 发现了一个有趣的现象: 在 Ocaml 中, 元组是用 * 来表示的, 而不是用逗号 , 来表示的. 也就是说, 在 Ocaml 中, 一个元组 (int, int) 是写成 int * int 的.

Why ? 于是我去了解了他们的设计, 读了一本叫做 Thinking with Types 的书, 发现了一个有趣的观点: 在 Ocaml 中, 类型是可以进行加减乘除运算的! 也就是说, 在 Ocaml 中, int * int 可以看作是 int 和 int 的乘积类型, 而不是一个单纯的元组类型.

接着读下去, 发现 Enum, Struct, Function, Trait(在C++中叫做 Concept) 都是对类型的某种运算!

让我们先把类型(Types)用集合的视角来看待

每个类型都可以看作是一个集合, 这个集合包含了所有属于这个类型的值. 例如, int 类型可以看作是一个包含了所有整数的集合, bool 类型可以看作是一个包含了 true 和 false 的集合.

而 Type 中的元素, 我们叫做 Value, 也就是这个集合中的元素. 例如, 0, 1, -1 等等都是 Value, 他们属于 int Type, 而 true 和 false 是 bool 类型的值.

既然是一个集合, 那么它就会有对应的基数(Cardinality), 也就是这个集合中元素的数量. 例如, bool 类型的基数是 2, 因为它只有两个值: true 和 false. int 类型的基数是无穷大, 因为它包含了所有整数(但是实际上, 在计算机中, int 类型的基数是有限的, 因为它有一个固定的位数, 例如 32 位或 64 位).

在此基础上, 就可以推导出编程语言中各种概念在类型系统中的对应关系了!

别担心, 下面我们会通过一些例子来说明这些概念是如何对应的. 并且使用更为熟悉的各种语言来说明!

先打地基: 0 和 1 类型

在讲加法和乘法之前, 先认识两个“单位元”角色:

  • 0 类型: 这个集合里一个值都没有
  • 1 类型: 这个集合里恰好只有一个值

它们在类型代数里非常关键, 因为很多式子都靠它们成立.

1 类型最直观, 基本每门语言都有:

rust
let u: () = ();
ocaml
let u : unit = ()
haskell
u :: ()
u = ()

0 类型则表示“不可能有值”. 在 Rust 里是 !(never type), 在 Haskell 里常用 Void 来表达.

有了这两个地基, 我们可以先记住三条最常用恒等式:

A+0≅AA + 0 \cong A A×1≅AA \times 1 \cong A A×0≅0A \times 0 \cong 0

直觉上也很好理解:

  • 和“不可能发生”的情况做 sum, 不会增加新值
  • 和“只有一种可能”的情况做 product, 不会增加新信息
  • 只要有一边“不可能发生”, 整个组合也不可能发生

Struct/Tuple 复合类型(Product Type)

这是我们最熟悉的一种类型, 把元组看作是没有标签的结构体, 不同的元素, 只有位置来标记他们

cpp
struct Person {
    int height;
    bool isMale;
};
using PersonT = std::tuple<int, bool>;
PersonT person = std::make_tuple(170, true);
rust
struct Person {
    height: i32,
    isMale: bool,
}
struct PersonT(i32, bool);
ocaml
type person = {
  height: int;
  is_male: bool;
}
type personT = int * bool
haskell
data Person = Person { height :: Int, isMale :: Bool }
type PersonT = (Int, Bool)

对于 struct/tuple 复合类型, 它的基数是所有元素的基数的乘积. 例如, Person 类型的基数是 int 的基数和 bool 的基数的乘积, 因为它包含了所有可能的 height 和 isMale 的组合. 同样地, PersonT 类型的基数也是 int 的基数和 bool 的基数的乘积.

我们这个时候可以把 Person 看作是一个新的类型, 它由两个集合 int 和 bool 通过乘积运算得到的. 而 PersonT 也是一个新的类型, 它由两个集合 int 和 bool 通过乘积运算得到的. 这就是为什么在 Ocaml 中, 元组是用 * 来表示的, 因为它表示了类型之间的乘积关系.

同时, 另一个层面, 我们也可以把 Person 看作是一个函数, 它接受一个 int value 和一个 bool value, 返回一个 Person 类型的值

这样可能会很混淆, 但是别担心, 他们两个出现的场景是不同的

对于语义1, Person 是一个类型, 它包含了所有可能的 height 和 isMale 的组合. 如此以来, 便定义了这个 Type 的所有 value 的范围, 同时由于它是一个类型, 因此他也可以作为其他类型的元素, 例如我们可以定义一个 struct Couple, 它包含了两个 Person 类型的元素:

cpp
struct Couple {
    Person person1;
    Person person2;
};

对于语义2, Person 是一个函数, 它接受一个 int value 和一个 bool value, 返回一个 Person 类型的值.

cpp
int main() {
    auto person1 = Person{170, true};
    // 可以把这里的 Person 看作是一个函数, 它接受一个 int value 和一个 bool value, 返回一个 Person 类型的值
    // 注意, 应该和编程语言中的函数区分开, 我们这里说的函数是一个数学意义上的函数, 它接受一些输入, 返回一个输出, 这个输出的类型就是 Person 类型
    return 0;
}
rust
fn main() {
    let person1 = Person {
        height: 170,
        isMale: true,
    };
    // 这里的 Person { ... } 也可以看成把字段值映射到 Person value 的构造过程
    let _ = person1;
}
ocaml
let person1 = { height = 170; is_male = true }
(* 在值构造语境里, 这里也是把 int 和 bool 组合成 person value *)

简而言之, 语义1一般出现于定义 Type 的时候, 包括定义自己和作为其他 Type 的元素

语义2一般出现在产生 Value 的时候. 他们两个虽然看起来很混淆, 但是他们的出现场景是不同的, 因此我们可以通过上下文来区分他们.

在其他语言中可能区分的不太清楚, 但是在 Haskell 中, 他们的区分是非常清楚的. 在 Haskell 中, 语义1 出现于定义 Type 的时候, 例如:

haskell
makePerson :: Int -> Bool -> Person
makePerson = Person
-- 我们定义了一个函数 makePerson, 它接受一个 Int value 和一个 Bool value, 返回一个 Person 类型的值
-- 但是在定义的时候, 我们直接把 makePerson = Person, 也就是说, Person 在这里是一个函数, 它接受一个 Int value 和一个 Bool value, 返回一个 Person 类型的值
-- 如果在 repl 中, 执行 :t Person, 会发现 Person 的类型是 Int -> Bool -> Person, 也就是说, Person 在这里是一个函数, 它接受一个 Int value 和一个 Bool value, 返回一个 Person 类型的值

Enum 离散类型(Sum Type)

Enum 类型是一种离散类型, 它包含了一组有限的值. 例如, bool 类型就是一个 Enum 类型, 因为它只有两个值: true 和 false.

我们也可以定义一个新的 Enum 类型, 例如: 例如一个只有 RED, GREEN, BLUE 三个值的 Color 类型: 即, Color这个集合只有三个元素Value, 分别是 RED, GREEN, BLUE. 因此, Color 类型的基数是 3.

cpp
enum Color {
    RED,
    GREEN,
    BLUE
};
rust
enum Color {
    Red,
    Green,
    Blue,
}
ocaml
type color = Red | Green | Blue
haskell
data Color = Red | Green | Blue

这也是一种定义 Type 的方式, 我们直接确定一个集合, 这个集合中有哪些元素, 这些元素就是这个 Type 的值. 这种方式定义的 Type 就是 Enum 类型, 因为它包含了一组有限的值.

同理这里也有两个语义, 语义1, Enum 类型是一个类型, 它包含了一组有限的值. 例如 Color 类型是一个类型, 因为它只有三个值: RED, GREEN, BLUE.

语义2, Enum 类型也是一个函数, 它不接收值, 返回一个 Enum 类型的值. Color::Red 是一个函数, 它不接收值, 返回一个 Color 类型的值. 同样地, Color::Green 和 Color::Blue 也是一个函数, 它们不接收值, 返回一个 Color 类型的值.

但是注意, 对于 Rust 来说, 这里的 Color::Red, Color::Green, Color::Blue 才是一个 function, 不接收值, 返回一个 Color 类型的值, 而不是 Color 这个函数. 同样地, 在 Haskell 和 Ocaml 中也是一样的, 他们也把这个 function 分成了三个 function, 一个接收 RED 类型的 Value, 一个接收 GREEN 类型的 Value, 一个接收 BLUE 类型的 Value.

cpp
int main() {
    auto value = Color::RED;
    // 可以把这里的 Color::RED 看作是一个函数, 它不接受值, 返回一个 Color 类型的值
    // 注意, 应该和编程语言中的函数区分开, 我们这里说的函数是一个数学意义上的函数, 它接受一些输入, 返回一个输出, 这个输出的类型就是 Color 类型
    return 0;
}
rust
fn main() {
    let value = Color::Red;
    // Color::Red 是 0 参数构造器, 可以理解成 () -> Color
    let _ = value;
}
ocaml
let value = Red
(* Red 是一个常量构造器, 类型是 color *)

Variant/Union 选择类型(Sum Type)

Variant/Union 类型是一种选择类型, 它包含了多个不同的类型, 例如 Shape 类型, 它可以是 Circle, Rectangle 中的任意一个. 也就是说, Shape 类型的值可以是 Circle 类型的值, 也可以是 Square 类型的值, 也可以是 Rectangle 类型的值.

cpp
struct Circle {
    double radius;
};
 
struct Rectangle {
    double width;
    double height;
};
 
// 古法 CPP
enum ShapeType {
    CIRCLE,
    RECTANGLE
};
struct Shape {
    union {
        Circle circle;
        Rectangle rectangle;
    };
    ShapeType type;
};
 
// 现代 CPP, 但是垃圾人体工学版本
using ShapeT = std::variant<Circle, Rectangle>;
rust
struct Circle {
    radius: f64,
}
 
struct Rectangle {
    width: f64,
    height: f64,
}
 
enum Shape {
    CircleArea(Circle),
    RectangleArea(Rectangle),
}
ocaml
type circle = { radius: float }
type rectangle = { width: float; height: float }
type shape = CircleArea of circle | RectangleArea of rectangle
haskell
data Circle = Circle { radius :: Double }
data Rectangle = Rectangle { width :: Double, height :: Double }
data Shape = CircleArea Circle | RectangleArea Rectangle

把 Shape 看作一个集合, Shape 类型的基数是 Circle 类型的基数加上 Rectangle 类型的基数. 例如, 如果 Circle 类型的基数是A, Rectangle 类型的基数是B, 那么 Shape 类型的基数就是 A + B.

也就是说一个 Type A = B | C, 这个 Type A 的基数是 B 的基数加上 C 的基数. 因此, 选择类型的基数是所有选项的基数之和.

其中, 我喜欢把这里 B 和 C 叫做两个域, 表示 A 这个集合可以分成两个域, 一个域是 B 的值, 另一个域是 C 的值. 例如, Shape 类型可以分成两个域, 一个域是 Circle 类型的值, 另一个域是 Rectangle 类型的值.

而且你可能注意到了, Rust/Ocaml/Haskell 还能对这个域进行命名, 例如, 在 Rust 中, 我们把 Circle 类型的域叫做 CircleArea, 把 Rectangle 类型的域叫做 RectangleArea. 但是 CPP 不行, 这两个域是没有名字的

BTW, Cpp的union 和其他这些语言的定义有一些区别, 原因是 Cpp 在运行时的时候, 对于一个 Shape Value, 我们并不能知道这个 Value 具体是Shape 哪个域的元素, 只能通过一个额外的 ShapeType 来标记这个 Value 是哪个域的元素. 原因是 CPP 本来也不是一门类型系统很复杂的语言, 所以还是主要看 std::variant 的定义, std::variant 就是一个真正的 Variant/Union 类型, 它在运行时会记录这个 Value 是哪个域的元素, 因此我们可以直接通过 std::get 来获取这个 Value 的具体类型.

同理他也有两个语义, 语义1, Variant/Union 类型是一个类型, 它包含了多个不同的类型. 例如 Shape 类型是一个类型, 因为它可以是 Circle 类型的值, 也可以是 Rectangle 类型的值.

语义2, Variant/Union 类型也是一个函数, 它接受一个值, 返回一个 Variant/Union 类型的值. Shape 类型是一个函数, 它接受一个值, 返回一个 Shape 类型的值.

但是注意, 对于语义2, 不同的语言是有点区别的

C++中, 我们认为这个 Shape 函数, 接受一个 value, 但是这个 value 必须属于 Circle 或者 Rectangle 集合, 同时这个 Circle, Rectangle 也是一个函数

cpp
int main() {
    auto value = ShapeT{Circle{1}};
}

其实C++那个理解是不准确的, 因为C++语法的限制, 我才这么说

Rust 中, Shple::CircleArea 才是一个 function, 接收一个属于 Circle 的 Value

和 CPP 的区别是, 这里变成了两个 function, 只接收那个特定的 Type Value, 同理 Haskell 和 Ocaml 也是一样的, 他们也把这个 function 分成了两个 function, 一个接收 Circle 类型的 Value, 另一个接收 Rectangle 类型的 Value

rust
fn main() {
    let cir = Circle { radius: 1.0 };
    let value = Shape::CircleArea(cir);
}

其中 Ocaml/Haskell 的 function name 直接就是那个域的名字, 而 Rust 的 function name 是 Shape::CircleArea, 但是他们的语义是一样的, 都是一个 function, 接收一个属于 Circle 的 Value, 返回一个 Shape 类型的 Value. 也就是说, 这个 function 的类型是 Circle -> Shape. 而第二个 function 的类型是 Rectangle -> Shape.

ocaml
let cir = { radius = 1.0 } in
let value = CircleArea cir
haskell
let cir = Circle { radius = 1.0 } in
let value = CircleArea cir

Good Candy

前面说过 Rust/Ocaml/Haskell 还能对这个域进行命名, 例如, 在 Rust 中, 我们把 Circle 类型的域叫做 CircleArea, 把 Rectangle 类型的域叫做 RectangleArea.

那我们直接把这个域的名字叫做 Circle, Rectangle, 并且把这两个具体的 struct 也不要了, 这个域直接接受一个 tuple 就好了, 例如:

rust
enum Shape {
    Circle(f64),
    Rectangle(f64, f64),
}
ocaml
type shape = Circle of float | Rectangle of float * float
haskell
data Shape = Circle Float | Rectangle Float Float

这里和之前也是一样的, Shape 这个集合分成两个区域, 区别就是, 之前的那种, 每个域的 value 都是来自一个 product type, 这个 type 是有名字的, 例如 Circle 类型的值是来自 Circle 这个 struct, Rectangle 类型的值是来自 Rectangle 这个 struct.

而现在这种, 每个域的 value 虽然也是来自一个 product type, 但是这个 type 没有名字

这样就更简洁了, 但是我们失去了对这个域的具体类型的定义, 例如, Circle 这个域接受一个 float value, 但是我们并没有定义一个 Circle 类型, 因此我们也无法定义一个 Circle 类型的值. 同样地, Rectangle 这个域接受两个 float value, 但是我们也没有定义一个 Rectangle 类型, 因此我们也无法定义一个 Rectangle 类型的值.

因此, 对于那些不会被复用的类型, 例如 Circle 和 Rectangle 这两个类型, 我们可以直接把他们的定义放在 Shape 这个 type 的定义中, 这样就更简洁了

Function 函数类型(Function Type)

函数类型是一种特殊的类型, 它表示一个函数的输入和输出.

例如 int -> int 表示一个类型集合, 它里面的元素是函数, 这些函数接受一个 int 类型的值, 返回一个 int 类型的值. 例如, f(x) = x + 1 就是一个 int -> int 类型的函数, 因为它接受一个 int 类型的值, 返回一个 int 类型的值.

我这里定义两个类型, 分别是 Color 和 Gender

cpp
enum Color {
    RED,
    GREEN,
    BLUE
};
enum Gender {
    MALE,
    FEMALE
};
auto f1(Color color) -> Gender {
    if (color == RED) {
        return Gender::MALE;
    } else {
        return Gender::FEMALE;
    }
}
auto f2(Color color) -> Gender {
    if (color == GREEN) {
        return Gender::MALE;
    } else {
        return Gender::FEMALE;
    }
}
rust
enum Color {
    Red,
    Green,
    Blue,
}
 
enum Gender {
    Male,
    Female,
}
 
fn f1(color: Color) -> Gender {
    match color {
        Color::Red => Gender::Male,
        _ => Gender::Female,
    }
}
 
fn f2(color: Color) -> Gender {
    match color {
        Color::Green => Gender::Male,
        _ => Gender::Female,
    }
}
haskell
data Color = Red | Green | Blue deriving (Eq, Show)
data Gender = Male | Female deriving (Eq, Show)
 
f1 :: Color -> Gender
f1 Red = Male
f1 _ = Female
 
f2 :: Color -> Gender
f2 Green = Male
f2 _ = Female

有多少种这种函数呢? 也就是说, 这个函数的输入是 Color 类型的值, 输出是 Gender, 这种映射能有多少种呢 由于 Color 类型的基数是 3, Gender 类型的基数是 2, 因此, 这个函数的基数是 2 的 3 次方, 也就是 8. 因为对于每个 Color 类型的值, 我们都有两种选择, 例如, 对于 RED, 我们可以选择 MALE 或者 FEMALE, 对于 GREEN, 其他元素同理, 因此, 这个函数的基数是 2 的 3 次方, 也就是 8.

同理, 如果这个时候有一个类型是 Gender -> Color, 这个函数的基数是 3 的 2 次方, 也就是 9. 因为对于每个 Gender 类型的值, 我们都有三种选择

注意不要和 product type 的基数搞混了, product type 的基数这些子类型的基数之积, 而 function type 的基数是输出类型的基数的输入类型的基数次方. 也就是说, 如果有一个函数类型是 A -> B, 这个函数类型的基数是 B 的 A 次方. 因为对于每个 A 类型的值, 我们都有 B 的选择, 因此, 这个函数类型的基数是 B 的 A 次方.

example
对于 Gender -> Color
f1 : Male -> Red, Female -> Red
f2 : Male -> Red, Female -> Green
f3 : Male -> Red, Female -> Blue
f4 : Male -> Green, Female -> Red
f5 : Male -> Green, Female -> Green
f6 : Male -> Green, Female -> Blue
f7 : Male -> Blue, Female -> Red
f8 : Male -> Blue, Female -> Green
f9 : Male -> Blue, Female -> Blue
但是如果是 (Color, Gender) 这个 produce type, 有几种呢
v1: (Red, Male)
v2: (Red, Female)
v3: (Green, Male)
v4: (Green, Female)
v5: (Blue, Male)
v6: (Blue, Female)

如果函数有多个参数...

但如果有一个函数类型是 Color -> Color -> Gender, 这个函数类型的基数是是什么呢?

cpp
auto f(Color color1, Color color2) -> Gender {
    if (color1 == RED && color2 == RED) {
        return  Gender::MALE;
    } else {
        return Gender::FEMALE;
    }
}
auto f_tuple(std::tuple<Color, Color> colors) -> auto {
    auto [color1, color2] = colors;
    if (color1 == RED && color2 == RED) {
        return Gender::MALE;
    } else {
        return Gender::FEMALE;
    }
}
rust
fn f(color1: Color, color2: Color) -> Gender {
    match (color1, color2) {
        (Color::Red, Color::Red) => Gender::Male,
        _ => Gender::Female,
    }
}
 
fn f_tuple(colors: (Color, Color)) -> Gender {
    let (color1, color2) = colors;
    match (color1, color2) {
        (Color::Red, Color::Red) => Gender::Male,
        _ => Gender::Female,
    }
}
ocaml
let f color1 color2 =
  if color1 = Red && color2 = Red then Male else Female
 
let f_tuple (color1, color2) =
  if color1 = Red && color2 = Red then Male else Female

对于每个上面f的函数, 我们都能改写成一个类似下面的函数, 这个函数接受一个 tuple, 而不是两个参数

因此, 要计算 Color -> Color -> Gender 的基数, 我们计算 (Color, Color) -> Gender 的基数就好了

  • (Color, Color) -> Gender 的基数 输入类型是 (Color, Color)，基数是 3 × 3 = 9 输出类型是 Gender，基数是 2 因此，(Color, Color) -> Gender 的基数是 2 的 9 次方，也就是 512。

神奇的相等! Currying 柯里化!

再次回忆上面的问题, 如果有一个函数类型是 Color -> Color -> Gender, 这个函数类型的基数是是什么呢?

如果我们把Color -> Color -> Gender 理解为 Color -> (Color -> Gender)： 也就是说，这是一个函数，它接受一个 Color 类型的值，返回一个 Color -> Gender 类型的函数 让我们来计算一下Color -> (Color -> Gender) 这个类型的基数:

  • 内层 Color -> Gender 的基数是 2 的 3 次方，即 8
  • 外层 Color -> (Color -> Gender) 的基数是 8 的 3 次方，即 512

简单的数学道理, 对于 A -> B -> C CB×A=(CB)AC^{B \times A} = (C^{B})^A

既然基数一样, 会不会这两个类型也是相等的呢?

我们知道, 类型在我们这里被理解为一个集合, 如何判断两个集合是否相等呢? 也就是说, 如何判断两个类型是否同构呢?

对于集合来说, 他们同构的条件是, 存在一个双射(bijection)函数, 也就是一个既单射又满射的函数, 这个函数把集合 A 中的每个元素都映射到集合 B 中的一个元素, 同时这个函数也是可逆的, 也就是说, 存在一个反函数, 把集合 B 中的每个元素都映射回集合 A 中的元素.

cpp
auto f1(Color color1, Color color2) -> Gender {
    if (color1 == RED && color2 == RED) {
        return  Gender::MALE;
    } else {
        return Gender::FEMALE;
    }
}
 
auto g1(Color color) -> auto {
    // 这里使用自动推导返回类型, 由于 C++ 并不支持高阶函数, 因此我们只能使用 auto 来推导返回类型, 其实返回的是一个仿函数, 不过不必那么认真
    return [color](Color color2) -> Gender {
        if (color == RED && color2 == RED) {
            return Gender::MALE;
        } else {
            return Gender::FEMALE;
        }
    };
}
rust
fn f1(color1: Color, color2: Color) -> Gender {
    match (color1, color2) {
        (Color::Red, Color::Red) => Gender::Male,
        _ => Gender::Female,
    }
}
 
fn g1(color: Color) -> impl Fn(Color) -> Gender {
    move |color2| match (color, color2) {
        (Color::Red, Color::Red) => Gender::Male,
        _ => Gender::Female,
    }
}
ocaml
let f1 color1 color2 =
  if color1 = Red && color2 = Red then Male else Female
 
let g1 color =
  fun color2 ->
    if color = Red && color2 = Red then Male else Female

可以看到, 对于任何一个 fx 函数, 我们都有一个 gx 函数对应, 反之亦然, 因此, 这两个类型是同构的

对于 haskell/ocaml 这种函数式语言来说, Color -> Color -> Gender, 这个类型本来就是 Color -> (Color -> Gender) 的简便写法, 也就是说 haskell 本来是不存在接收多个参数的函数的, 他们所有的函数都是接收一个参数, 返回一个函数, 这个函数又接收一个参数, 返回一个函数, 以此类推, 直到最后一个函数返回一个值.

于是在 haskell/ocaml 中, 我们可以看到这样的操作

haskell
data Color = Red | Green | Blue deriving (Eq, Show)
data Gender = Male | Female deriving (Eq, Show)
 
f :: Color -> Color -> Gender
f color1 color2 = if color1 == Red && color2 == Red then Male else Female
 
main :: IO ()
main = do
    let g = f Red -- 这里的 g 的类型是 Color -> Gender
    print $ g Red -- 调用 g 这个函数, 得到一个 Gender value
    -- 当然也可以直接调用到底
    print $ f Red Red
    -- 因为 haskell 的求值顺序是从左到右, 所以是 (f Red) Red, 也就是说, 先调用 f 这个函数, 得到一个 Color -> Gender 类型的函数, 然后再调用这个函数, 得到一个 Gender value

递归类型与不动点(Fixpoint)

前面讲的 Sum/Product/Function 都是在“有限展开”里做运算, 但是实际编程里我们最常见的数据结构之一是 List/Tree, 他们本质上是递归定义出来的.

让我们看一个 IntList.

IntList 的直觉定义是:

  • 要么是空列表
  • 要么是一个元素 int 加上一个更小的 IntList

把这个定义翻译成类型代数, 就是:

IntList≅1+Int×IntListIntList \cong 1 + Int \times IntList

其中 1 表示只有一个值的类型(比如 unit), 对应“空列表”这个分支.

这个式子在代码里长什么样

rust
enum IntList {
        Nil,
        Cons(i32, Box<IntList>),
}
ocaml
type int_list =
    | Nil
    | Cons of int * int_list
haskell
data IntList = Nil | Cons Int IntList

看 Rust 的定义最明显:

  • Nil 对应 1
  • Cons(int, IntList) 对应 Int × IntList
  • enum 的两个分支合起来对应 1 + Int × IntList

为什么说是“不动点”

先别急着上定义, 先想象一个“类型模板机”:

  • 你给它一个类型 X
  • 它吐出来一个新类型 1 + Int × X

这个模板机就叫 F, 也就是:

F(X) = 1 + Int × X

现在关键来了: 如果我把 IntList 自己塞进去, 得到的还是和 IntList 同构的东西:

IntList≅F(IntList)IntList \cong F(IntList)

这句话翻成大白话就是: 这个类型再过一遍这台“模板机”, 形状没变.

“塞进去前后都一样(同构)”的那个点, 就叫不动点(fixpoint).

所以递归类型可以这么理解:

  • 先写一个模板 F(X)
  • 再找一个类型 T, 让 T ≅ F(T)
  • 找到的这个 T, 就是递归数据结构本体

同理, 二叉树也能这样写:

IntTree≅1+Int×IntTree×IntTreeIntTree \cong 1 + Int \times IntTree \times IntTree

Trait/Concept/Typeclass -- 谓词

什么是谓词呢? 根据维基百科的定义, P 是一个谓词, 作用在个体元素 a 上, 因此 P(a) 是一个命题, 这个命题要么为真, 要么为假. 例如, P(x) = "x is a prime number", 这个谓词作用在一个整数 x 上, 如果 x 是一个质数, 那么 P(x) 就为真, 否则 P(x) 就为假.

对于 Trait 这种谓词来说, 他作用的个体元素就是 Type

cpp
template <typename T>
concept Eq = requires(T a, T b) {
    { a == b } -> std::convertible_to<bool>;
};
 
struct Person {
    std::string name;
    int age;
    double height;
};
// 在 C++ 中, 我们不能主动去证明一个类型在 concept 谓词下为真
// 在 C++ 中, 只能去隐式的表达: 当前这个 Type 满足谓词concept的要求
// 因此, 这里我们只能通过定义一个 operator== 来表达 Person 这个类型满足 Eq 这个 concept 的要求
bool operator==(Person a, Person b) {
    // ....
}
rust
pub trait Eq {
    fn eq(&self);
}
 
struct Person {
    name: String,
    age: i32,
    height: f64,
}
 
// 在 Rust 中, 我们可以通过 impl 来证明一个类型满足一个 trait 的要求
// 即证明 某个 Type 在某个 Trait 这个谓词下为真
impl Eq for Person {
    fn eq(&self) {
        // ....
    }
}
haskell
class Eq a where
  (==) :: a -> a -> Bool
 
data Person = Person { name :: String, age :: Int, height :: Double }
 
-- Haskell 和 Rust 一样, 也可以通过实例化 typeclass 来证明一个类型满足一个 typeclass 的要求
instance Eq Person where
  (==) (Person name1 age1 height1) (Person name2 age2 height2) =
    name1 == name2 && age1 == age2 && height1 == height2

上面的Eq 谓词翻译过来就是:

∀a∈Type  T,b∈Type  T,∃P∈Bool,P=(a==b)\forall a \in Type \; T, b \in Type \; T, \exists P \in Bool, P = (a == b)

也就是对于所有a, b(属于 Type T), 存在 (a == b), 这个表达式的值属于 bool type

泛型 function, 用 trait 约束它!

cpp
template<typename T>
auto plus(T a, T b) -> T {
    return a + b;
}
 
template<typename T>
requires Eq<T>
auto not_equal(T a, T b) -> bool {
    return !(a == b);
}
fn plus<T>(a: T, b: T) -> T {
    return a + b;
}
 
fn not_equal<T>(a: T, b: T)
-> bool
where
    T: Eq
{
    !(a == b)
}
plus :: a -> a -> a
plus a b = a + b
 
not_equal :: Eq a => a -> a -> Bool
not_equal a b = !(a == b)

对于没有约束的泛型函数, 如 plus, 则是一个 ∀\forall 证明, 表达对于所有 Type, 都存在一个 plus, 他接收两个 value from Type A, 返回的 Value 也是 Type A 其实有约束的泛型函数也是一个 ∀\forall 证明, 表达对于所有 Trait(Type) => true的 Type, 都存在这么一个function

实际上, 上述的 Rust plus 函数是无法编译的, 因为 Rust 会在定义函数的时候就对函数进行谓词的检查, 函数体中出现了 a + b 这个表达式, 这个时候, Rust 就会去看 T 是否满足 Add 这个谓词

但是 C++ 和 Haskell 是不一样的, 他们在定义一个函数的时候并不会进行这样的检查, 而是在具体调用这个函数的时候才会进行检查, 也就是说, 他们的 plus 函数是可以编译的, 但是如果我们在调用这个函数的时候, 传入了一个不满足 Add 这个谓词的 Type, 那么就会编译失败

参数多态的“免费定理”(Free Theorems)

前面说泛型 function 本质上是一个 ∀\forall 证明, 这里还有一个很神奇的结论:

只要你给我一个足够“纯”的类型签名, 就算你不看函数体, 也能推导出它必须满足的一些性质.

这就是 free theorem, 叫“免费”是因为这些性质几乎是白送的, 只由类型签名决定.

最经典例子:

haskell
id :: a -> a

这个签名约束力极强. 因为参数类型是任意 a, 返回值也必须是同一个 a, 那你几乎没得选: 对于这个 Type a, 我们实际上没有给任何信息, 或者说, 信息为零

没有信息, 或者说不暴露任何信息, 意味着什么呢

  • 你不能凭空造一个 a
  • 你也不能“检查” a 的内部结构(因为你不知道它是什么)
  • 你唯一稳妥的做法, 就是把输入原样还回去

这里说的“约束”, 不是指 Trait bound, 而是指: 在函数体里, 你能对 a 类型值做的操作被压到很少. 可做操作越少, 实现空间越小, 越容易推理正确性.

所以 id 的行为其实被类型签名钉死了.

再看一个:

haskell
headOption :: [a] -> Maybe a

你同样不能凭空造 a, 只能从输入列表里拿一个 a 出来(或者返回 Nothing).

再比如:

haskell
map :: (a -> b) -> [a] -> [b]

它的 free theorem 直觉是: map 不能“偷窥” a 或 b 的具体内容, 它只能老老实实按你给的函数逐个搬运结构.

这也是为什么我们在函数式编程里常说: 类型签名不只是“注释”, 它本身就在限制实现空间, 甚至直接给出一部分正确性保证.

如果把它和上文的 ∀\forall 连起来看, 逻辑就更清楚了:

  • f :: forall a. a -> a 的意思是: 对所有类型 a, 你都得给出同一个规律的实现
  • 既然要对“所有 a”成立, 就不能偷偷依赖某个具体类型的特性
  • 所以, forall 越“纯”, 你能写的行为就越少, 免费定理就越强

Rust 里也有同样的味道:

rust
fn id<T>(x: T) -> T {
    x
}
 
fn first<T>(xs: Vec<T>) -> Option<T> {
    xs.into_iter().next()
}

id<T> 基本只能把 x 还回去; first<T> 也不能凭空造一个 T, 只能从输入 Vec<T> 里拿.

上面这层逻辑的关键词是: 对 a 信息越少, 对实现者限制越强.

那如果你给 a 增加 Trait/Typeclass 约束呢? 这是另一条轴: 显式“给了额外信息”.

比如:

haskell
notEqual :: Eq a => a -> a -> Bool
rust
fn not_equal<T: PartialEq>(a: T, b: T) -> bool {
    a != b
}

这里的 a 已经不是“完全未知”了, 你至少知道它支持比较操作. 所以实现空间会变大: 你可以合法地调用 == / !=.

从 free theorem 视角看, 就是:

  • a 的信息越少(函数体可操作越少), 定理越强(行为越被钉死)
  • a 的信息越多(函数体可操作越多), 定理越弱(可做的事越多)

但这不是坏事, 这是工程上常用的平衡: 我们牺牲一部分“免费保证”, 换来更实用的能力.

当然, 这个结论有前提: 要尽量在纯函数语义下讨论. 如果语言里混入大量副作用、非终止、反射等能力, 这些“免费性质”会被削弱.

泛型 Type

cpp
template<typename T>
struct Option {
    bool is_some;
    T value;
};
rust
enum Option<T> {
    Some(T),
    None,
}
ocaml
type 'a option = Some of 'a | None
haskell
data Option a = Some a | None

泛型 Type 可以看作一个 function, 这个 function 接受一个 Type, 返回一个 Type. 例如, Option<T> 就是一个 function, 它接受一个 Type T, 返回一个 Type Option<T>. 同样地, Option a 也是一个 function, 它接受一个 Type a, 返回一个 Type Option a.

当然, 也可以在这里加上一个 Trait 约束, 例如, Option<T: Eq> 就是一个 function, 它接受一个 Type T, 这个 Type T 必须满足 Eq 这个 Trait 的要求, 返回一个 Type Option<T>.

递归类型与不动点(Fixpoint)

现在已经有了“泛型 Type”这个概念, 我们就可以自然地看递归泛型类型了.

比如 List(A) 的直觉定义是:

  • 要么是空列表
  • 要么是一个元素 A 加上一个更小的 List(A)

把这个定义翻译成类型代数, 就是:

List(A)≅1+A×List(A)List(A) \cong 1 + A \times List(A)

其中 1 表示只有一个值的类型(比如 unit), 对应“空列表”这个分支.

这个式子在代码里长什么样

rust
enum List<A> {
        Nil,
        Cons(A, Box<List<A>>),
}
ocaml
type 'a list =
    | Nil
    | Cons of 'a * 'a list
haskell
data List a = Nil | Cons a (List a)

看 Rust 的定义最明显:

  • Nil 对应 1
  • Cons(A, List<A>) 对应 A × List(A)
  • enum 的两个分支合起来对应 1 + A × List(A)

为什么说是“不动点”

先别急着上定义, 先想象一个“类型模板机”:

  • 你给它一个类型 X
  • 它吐出来一个新类型 1 + A × X

这个模板机就叫 F, 也就是:

F(X) = 1 + A × X

现在关键来了: 如果我把 List(A) 自己塞进去, 得到的还是和 List(A) 同构的东西:

List(A)≅F(List(A))List(A) \cong F(List(A))

这句话翻成大白话就是: 这个类型再过一遍这台“模板机”, 形状没变.

“塞进去前后都一样(同构)”的那个点, 就叫不动点(fixpoint).

所以递归类型可以这么理解:

  • 先写一个模板 F(X)
  • 再找一个类型 T, 让 T ≅ F(T)
  • 找到的这个 T, 就是递归数据结构本体

同理, 二叉树也能这样写:

Tree(A)≅1+A×Tree(A)×Tree(A)Tree(A) \cong 1 + A \times Tree(A) \times Tree(A)

type Item -- 伴随类型(Associated Type)

rust
trait Iterator {
    type Item;
    fn next(&mut self) -> Option<Self::Item>;
}
haskell
class Iterator a where
    type Item a
    next :: a -> Maybe (Item a)

前文提到, trait 是一个谓词, 但是如果 trait 也是动态的呢?

这里的 Iterator 可以理解为一个 function, 这个 function 接收一个 Type, 才能产生真正的 trait 谓词, 例如, Iterator<Item = i32> 就是一个 trait 谓词, 这个 trait 谓词作用在一个 Type 上, 例如 Vec<i32>, 这个 Type 满足 Iterator<Item = i32> 这个 trait 谓词的要求, 因此我们可以说 Vec<i32> 是一个满足 Iterator<Item = i32> 这个 trait 的 Type.

补充: 字典传递 vs 约束求解

前面我们把 Trait/Typeclass 看成“谓词”, 从编译器实现角度, 常见有两步:

  • 约束求解(constraint solving): 编译器先证明当前类型满足哪些约束, 例如 T: Eq、T: Iterator<Item = i32>
  • 字典传递(dictionary passing): 证明完成后, 把对应实现当作“字典”传给函数体(可以理解成一组方法表)

在 Haskell 里, 这个模型通常最直观: Eq a => ... 经常被解释为“隐式多一个 Eq a 字典参数”.

在 Rust 里, 语法上你看到的是 T: Trait, 直觉上也可以这样理解:

  • 先做约束求解(类型检查/trait selection)
  • 再在单态化后选中具体 impl, 让方法调用落到对应实现上

所以这两个词不是互斥关系, 更像一个前后流程:

  • 先解题(有没有证据)
  • 再用证据(把能力带进函数体)

Comments

Loading comments...

    Please complete the verification challenge.

    Back to archive