代数解释多态性
所以我理解types的基本代数解释：
Either ab ~ a + b (a, b) ~ a * b a -> b ~ b^a () ~ 1 Void ~ 0 -- from Data.Void …这些关系对于具体types是正确的，比如Bool ，而不是像a这样a多态types。 我也知道如何将多态types的types签名转换成具体的types表示，只需要按照下面的同构翻译教会编码：
(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
对于每个具体types的同构我可以指向一个等价的代数规则，例如：
(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
这是身份函数的着名的Yoneda引理 。
检查这篇文章的可读介绍，以及任何类别理论教科书更多。
简而言之，给定f :: forall r. (a -> r) -> r f :: forall r. (a -> r) -> r你可以使用f id来得到一个a ，反之，给定x :: a你可以拿($x)来得到全部forall r. (a -> r) -> r forall r. (a -> r) -> r 。
这些操作是相反的。 certificate：
显然($x) id == x 。 我会certificate这一点
($(f id)) == f ，
因为函数在所有参数相等的情况下都是相等的，所以让我们把x :: a -> r并显示出来
($(f id)) x == fx ie
x (f id) == fx 。
由于f是多态的，所以它作为一个自然的转换。 这是f的自然图：
f_A Hom(A, A) → A (x.) ↓ ↓ x Hom(A, R) → R f_R
所以x . f == f . (x.) x . f == f . (x.) x . f == f . (x.) 。
堵住身份， (x . f) id == fx x。f (x . f) id == fx 。 QED
（为了清楚而重写）
你的问题似乎有两个部分。 一个是暗示的，是在问什么是代数的解释是什么，另一个是问关于继续/ Yoneda转换，这sdcvvc的答案已经很好地覆盖。
我会尽力为你解决所有的代数解释。 你提到A -> B是B^A但是我想进一步把它扩展到B * B * B * ... * B （ |A|次）。 尽pipe我们把幂运算作为重复乘法的符号，但是还有更灵活的符号∏ （大写Pi）代表任意索引的乘积。 Pi有两个组成部分：我们想要乘以的值的范围，以及我们所乘的expression式。 例如，在价值层面上，你可以将阶乘函数expression为fact i = ∏ [1..i] (λx -> x) 。
回到types的世界，我们可以把A -> B ~ B^A对应中的指数运算符看作Pi： B^A ~ ∏ A (λ_ -> B) 。 这就是说，我们正在定义B的一个A -ary积，所以B不能依赖于我们select的特定的A 当然，这相当于简单的求幂，但它可以让我们转向依赖的情况。
在最一般的情况下，我们得到依赖types，就像你在Agda或Coq中看到的那样：在Agda语法中， replicate : Bool -> ((n : Nat) -> Vec Bool n)是Pitypes的一个可能的应用，这可以更明确地表示为replicate : Bool -> ∏ Nat (Vec Bool) ，或者进一步作为replicate : ∏ Bool (λ_ -> ∏ Nat (Vec Bool)) 。
请注意，正如您可能从底层代数中所期望的那样，您可以将上面replicate的定义中的两个∏都融合成一个单独的∏ ，这个∏范围超出了域的笛卡尔乘积： ∏ Bool (\_ -> ∏ Nat (Vec Bool))相当于∏ (Bool, Nat) (λ(_, n) -> Vec Bool n) ，就像在“价值层面”一样。 这只是从types理论的angular度来看，
我确实意识到你的问题是关于多态的，所以我将停止讨论依赖types，但是它们是相关的：Haskell中的forall大致相当于具有types（种类） *上的域的∏ 。 事实上，多态性的类似function的行为可以直接在GHC核心中观察到，将其归类为资本lambda（Λ）。 就像这样，一个多态的types如forall a. a -> a forall a. a -> a实际上只是∏ * (Λ a -> (a -> a)) （现在用Λ表示我们区分types和值），它可以扩展到无限乘积(Bool -> Bool, Int -> Int, () -> (), (Int -> Bool) -> (Int -> Bool), ...) 。 typesvariables的实例化只是从* -ary产品（或应用types函数）中推出适当的元素。
现在，我在这个答案的原始版本中错过了一大块：parametricity。 参数性可以用几种不同的方式来描述，但是我所知道的（参见types为关系，或（分类）理论中的（di）自然性）都没有真正的代数解释。 然而，就我们的目的而言，它归结为相当简单的事情：你不能在*上进行模式匹配。 我知道，GHC可以让你在types族的types层次上做到这一点，但是当你这样做的时候，你只能覆盖有限的一部分* ，所以总是有一些你的types族未定义的点。
从多态性的angular度来看，这意味着我们在∏ * F写的任何types函数F必须是常量（即完全忽略它是多态的types），或者通过不变的types传递。 因此， ∏ * (Λ _ -> B)是有效的，因为它忽略了它的参数，并对应于所有的forall a. B forall a. B 另一种情况就像∏ * (Λ x -> Maybe x) ，它对应于forall a. Maybe a forall a. Maybe a不会忽略types参数，但只是“传递”。 因此，具有不相关域A （例如当A = * ） A ΠA可以被看作是更多的A -ary索引交集 （在索引的所有实例化中挑选公共元素），而不是产品。
至关重要的是，在价值层面上，参数性规则可以防止任何有趣的行为，这些行为可能表明types比实际大。 因为我们没有typecase，所以我们不能构造一个types的值forall a. B forall a. B根据实例化的内容做了一些不同的事情。 因此，尽pipe这种types在技术上是一个函数* -> B ，它总是一个常数函数，因此相当于B的单个值。 使用∏解释，它确实等价于B s的无限*积，但这些B值必须始终相同，所以无限乘积有效地与单个B一样大。
类似地，尽pipe∏ * (Λ x -> (x -> x)) （aka， forall a. a -> a ）在技术上等价于函数的无穷乘积，但是这些函数都不能检查types，被限制只返回他们的input值，而不是做任何有趣的事情，如(+1) : Int -> Int当实例化为Int 。 因为只有一个（假定是全语言的）函数不能检查它的参数的types，但是必须返回一个相同types的值，所以无限乘积就像单个值一样大。
现在，关于你的直接问题(forall r . (a -> r) -> r) ~ a 。 首先，让我们更正式地expression你的操作符。 这是真的同构，所以我们需要两个函数来回运动，并且有一个论点是他们是逆向的。
data Iso ab = Iso { to :: a -> b , from :: b -> a -- proof1 :: forall x. to (from x) == x -- proof2 :: forall x. from (to x) == x }
现在我们用更正式的话来expression你原来的问题。 你的问题相当于构build一个以下的术语（impredicative，所以GHC有麻烦，但我们将生存）types：
forall a. Iso (forall r. (a -> r) -> r) a
其中使用了我以前的术语，它等于∏ * (Λ a -> Iso (∏ * (Λ r -> ((a -> r) -> r))) a) 。 我们再次拥有一个无法检查其types参数的无限产品。 通过handwaving，我们可以争辩说，唯一可能的价值考虑参数性规则（其他两个certificate是自动尊重）是和($ id)和flip id 。
如果这感觉不令人满意的话，那可能是因为代数的解释并没有给certificate添加任何东西。 这实际上只是简单的旧式理论，但是我希望能够提供一些比Yonedaforms更小的分类。 值得注意的是，尽pipe我们实际上并不需要使用参数来编写proof1和proof2 。 当我们想要说明($ id)和flip id是我们唯一的selectfrom （我们无法在Agda或Coq中certificate的($ id)时，参数只会进入图片。
为了（试图）回答实际问题（这比所提出的更广泛的问题的答案更有趣），由于“types错误”
Either ~ (+) (,) ~ (*) (->) b ~ flip (^) () ~ 1 Void ~ 0
这些将所有types映射到整数，并在自然方法上构造函数types。 从某种意义上说，你有一个从types到自然类别的函子。 在另一个方向，你“忘记”的东西，因为types保持代数结构，而自然把它扔掉。 即给Either () ()你可以得到一个独特的自然，但鉴于这种自然，你可以得到很多types。
但是这是不同的：
(forall r . (a -> r) -> r) ~ a
它将一个types映射到另一个types！ 这不是上述函子的一部分。 这只是types范畴内的一个同构。 所以让我们给出一个不同的符号， <=>
现在我们有了
(forall r . (a -> r) -> r) <=> a
现在你注意到，我们不仅可以将箭头types发送到箭头，而且还可以与其他同构types同构：
(a, (b, c)) <=> ((a, b), c) ~ a * (b * c) = (a * b) * c
但是，这里正在发生一些微妙的事情。 从某种意义上说，后者的同构是真实的， 因为代数的同一性是正确的。 这就是说后者中的“同构”只是意味着这两种types在我们函子的形象下是等价的。
前一个同构我们需要直接certificate，这是我们开始接触到潜在问题的地方 – 赋予了nats的函子， forall r. 地图？ 但答案是，所有的forall r. 既不是types，也不是types之间的有意义的箭头。
通过引入福利，我们已经摆脱了第一类订单。 没有理由期待所有的函数都适合我们上面的函子，事实上并不是这样。
所以我们可以像上面其他人一样探索为什么同构（为了解决这个问题本身就很有趣），但是这样做却放弃了这个问题的代数核心。 我想，可以回答的一个问题是，由于高阶types和构造函数是箭头之间的箭头，那么Functor有什么意义呢？
编辑 ：所以现在我有另一种方法，显示为什么添加多态性使事情变得疯狂。 我们首先提出一个更简单的问题 – 一个给定的多态types是否有零个或多于零的居民？ 这是types居住问题 ，通过库里 – 霍华德（Curry-Howard），这是一个修改后的可实现性的问题，因为和问一个逻辑中的公式是否可以在适当的计算模型中实现是一回事。 现在正如该页面所解释的那样，这在简单types的lambda演算中是可以确定的，但是是PSPACE完成的。 但是，一旦我们转向更复杂的东西，例如添加多态性并进入系统F，那么就会变成不可判定的！
所以，如果我们不能决定是否有任意types的居民，那么我们显然不能确定它有多less居民！
这是一个有趣的问题。 我没有一个完整的答案，但这太长了评论。
types签名(forall r. (a -> r) -> r)可以表示为我所说的
对于任何你喜欢命名的types，如果你给我一个函数来
a一个r，那么我会给你一个r。
现在，这必须适用于任何types的r ，但它可以是一个特定的typesa 。 所以我拉这个巧妙的诀窍的方法是坐在某个地方，我喂养function（为我产生一个r ），然后把这个r交给你。
但如果我坐下来，我可以把它给你：
如果你给我一个1，我会给你
a。
这对应于types签名1 -> a或简单的a 。 通过我们这个非正式的论点
(forall r. (a -> r) -> r) ~ a
下一步将是生成相应的代数expression式，但我不清楚代数量如何与通用量化相互作用。 我们可能需要等待专家！
几个链接到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 |
¹）在适当的类别中 – Haskell（ 链接 ）的总和非多态子集的CCC ，Haskell（ 链接 ）的非全特性的CPO，依赖types语言的LCCC 。
²）全量化是依赖产品的特例：
∀(x :: *). y[x] ~ ∏(x : Set)y[x]
其中Set是所有小types的宇宙 。
