haskell - 代数解释多态性

Question

所以我理解类型的基本代数解释:

Either a b ~ a + b
(a, b) ~ a * b
a -> b ~ b^a
()   ~ 1
Void ~ 0 -- from Data.Void

...并且这些关系对于具体类型(例如 Bool)是正确的，而不是像 a 这样的多态类型。我还知道如何通过根据以下同构转换 Church 编码，将具有多态类型的类型签名转换为其具体类型表示:

(forall r . (a -> r) -> r) ~ a

所以如果我有:

id :: forall a . a -> a

我知道它的意思不是id ~ a^a，但它实际上意味着:

id :: forall a . (() -> a) -> a
id ~ ()
   ~ 1

同样:

pair :: forall r . (a -> b -> r) -> r
pair ~ ((a, b) -> r) - > r
     ~ (a, b)
     ~ a * b

这引出了我的问题。该规则的“代数”解释是什么:

(forall r . (a -> r) -> r) ~ a

对于每个具体类型同构，我都可以指出一个等效的代数规则，例如:

(a, (b, c)) ~ ((a, b), c)
a * (b * c) = (a * b) * c

a -> (b -> c) ~ (a, b) -> c
(c^b)^a = c^(b * a)

但我不明白类似于以下的代数等式:

(forall r . (a -> r) -> r) ~ a

Answer 1

这就是著名的Yoneda lemma为恒等仿函数。

检查this发布一个可读的介绍，以及任何范畴论教科书以获取更多信息。

简单地说，给定f::forall r。 (a -> r) -> r 您可以应用 f id 来获取 a，反之，给定 x::a 你可以使用 ($x) 来获取 forall r. (a -> r) -> r。

这些操作是互逆的。证明:

显然($x) id == x。我会证明这一点

($(f id)) == f,

由于函数在所有参数都相等时相等，所以让我们采用 x::a -> r 并证明这一点

($(f id)) x == f x 即

x (f id) == f x。

由于 f 是多态的，因此它可以作为自然转换；这是 f 的自然图:

               f_A
     Hom(A, A)  →  A
(x.)      ↓        ↓ x
     Hom(A, R)  →  R
               f_R

所以x。 f == f 。 (x.).

插入标识，(x . f) id == f x。量子ED