代数解释多态性

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引理。

请查看这篇文章以获得可读的介绍，并查看任何类别理论教科书以获得更多。

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

由于函数在所有参数上都相等时也是相等的，所以让我们以X::a->R为例，并展示

($(f id））x==f x即。

x（f id）==f x。

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