55

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

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
4

5 回答 5

30

这就是恒等函子的著名米田引理。

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

简而言之，假设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 xIE

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。量子点

于 2012-05-05T00:42:42.937 回答
17
于 2012-05-04T22:35:59.517 回答
8

为了（尝试）回答实际问题（这比对所提出的更广泛问题的答案不那么有趣），由于“类型错误”，该问题形成不正确

Either ~ (+) 
(,)    ~ (*)
(->) b ~ flip (^)
()   ~ 1
Void ~ 0

这些都将类型映射到整数，并将类型构造函数映射到自然函数。从某种意义上说，你有一个从类型范畴到自然范畴的函子。在另一个方向上，您“忘记”了东西，因为类型保留了代数结构，而自然则将其丢弃。即给定Either () ()您可以获得独特的自然，但鉴于自然，您可以获得多种类型。

但这是不同的：

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

它将一种类型映射到另一种类型！它不是上述函子的一部分。它只是类型类别中的同构。所以让我们给它一个不同的符号，<=>

现在我们有

(forall r . (a -> r) -> r) <=> a

现在您注意到我们不仅可以将类型发送到 nat 并将箭头发送到箭头，还可以将一些同构发送到其他同构：

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

但是这里正在发生一些微妙的事情。在某种意义上，后一种对的同构是真的，因为代数恒等式是真的。这就是说后者中的“同构”仅仅意味着这两种类型在我们的函子的形象下与 nats 是等价的。

我们需要直接证明的前一个同构，这是我们开始解决潜在问题的地方——将我们的函子赋予 nats，forall r.映射到什么？但答案是forall r.它既不是类型，也不是类型之间的有意义的箭头。

通过引入 forall，我们摆脱了第一订单类型。没有理由期望 forall应该适合我们上面的 Functor，事实上，它不适合。

所以我们可以像上面其他人一样探索为什么同构成立（这本身很有趣）——但这样做我们已经放弃了问题的代数核心。我认为一个可以回答的问题是，考虑到高阶类型和构造函数的类别作为它们之间的箭头，那么有什么有意义的 Functor 呢？

编辑：所以现在我有另一种方法来说明为什么添加多态性会使事情变得疯狂。我们首先问一个更简单的问题——给定的多态类型是否有零个或多于零个居民？这是类型居住问题，并且通过 Curry-Howard 最终成为修改后的可实现性问题，因为这与询问某些逻辑中的公式是否可以在适当的计算模型中实现是一样的。现在正如该页面所解释的，这可以在简单类型的 lambda 演算中确定，但它是 PSPACE 完整的。但是一旦我们转向更复杂的东西，例如通过添加多态性并进入系统 F，那么它就会变得不可判定！

所以，如果我们无法确定一个任意类型是否有人居住，那么我们显然无法确定它有多少居民！

于 2012-05-07T22:38:13.260 回答
4

nLab的一些链接：

因此，在范畴论的设置中：

Type               | Modeled¹ as               | In category
-------------------+---------------------------+-------------
Unit               | Terminal object           | CCC
Bottom             | Initial object            |
Record             | Product                   |
Union              | Sum (coproduct)           |
Function           | Exponential               |
-------------------+---------------------------+-------------
Dependent product² | Right adjoint to pullback | LCCC
Dependent sum      | Left adjoint to pullback  |

¹) 在适当的类别中——CCC代表Haskell 的全部和非多态子集（链接），CPO 代表 Haskell 的非全部特征（链接），LCCC代表依赖类型语言。

²)forall量化是依赖积的一个特例：

∀(x :: *). y[x] ~ ∏(x : Set)y[x]

所有小类型Set的宇宙在哪里。

于 2012-05-06T14:29:44.493 回答
4

这是一个有趣的问题。我没有完整的答案，但这对于评论来说太长了。

类型签名(forall r. (a -> r) -> r)可以表达为我说

对于你想命名的任何类型r，如果你给我一个接受a并产生一个的函数r，那么我会给你一个r.

现在，这必须适用于任何类型r，但它可以是特定类型a。因此，我使用这个巧妙技巧的方法是a坐在某个地方，我将其提供给函数（它r为我生成一个），然后我把它r交给你。

但如果我a有空坐，我可以给你：

如果你给我一个1，我会给你一个a。

它对应于类型签名1 -> a或简单地说a。通过这个非正式的论证，我们有

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

下一步将是生成相应的代数表达式，但我不清楚代数量如何与全称量化相互作用。我们可能需要等待专家！

于 2012-05-04T18:27:28.323 回答