forall b. (a -> b) -> b === a。首先，因为我认为推广到Codensity有点过于狂热。其次，这是将一堆有趣的事情联系在一起的机会。继续阅读！b并向盒子传递一个类型为Bool -> b的函数，盒子就会吐出一个b。我们可以在不看盒子内部的情况下了解这个盒子的特性吗？我们能否知道硬币的状态？我们能否知道盒子用什么机制产生b？事实证明，我们两者都可以做到。Box Bool的等级2函数。type Box a = forall b. (a -> b) -> b
这里的第二类类型表示盒子制造者选择a，盒子使用者选择b。
我们把a放进盒子里，然后关闭盒子，创建了一个闭包。
-- Put the a in the box.
box :: a -> Box a
box a f = f a
box True。部分应用程序只是创建闭包的巧妙方法！b，我可以选择Bool并传递一个函数Bool -> Bool。如果我选择id :: Bool -> Bool，那么问题是：盒子是否会吐出它包含的值？答案是盒子要么会吐出它包含的值，要么会吐出无意义的结果（类似于undefined的底部值）。换句话说，如果你得到了一个答案，那么这个答案必须是正确的。-- Get the a out of the box.
unbox :: Box a -> a
unbox f = f id
unbox . box = id
box . unbox = id
unbox . box
= {- definition of (.) -}
\b -> unbox (box b)
= {- definition of unbox and (f a) b = f a b -}
\b -> box b id
= {- definition of box -}
\b -> id b
= {- definition of id -}
\b -> b
= {- definition of id, backwards -}
id
如果这些证明看起来相当琐碎，那是因为Haskell中所有（总）多态函数都是自然变换，而我们在这里证明的就是自然性。参数性再次为我们提供了低廉的定理！
另外，对于读者来说，为什么我不能使用(.)定义rebox呢？
rebox = box . unbox
为什么我要像穴居人一样手动内联定义(.)？
rebox :: Box a -> Box a
rebox f = box (unbox f)
提示：什么是box、unbox和(.)的类型？
现在，我们如何将Box泛化？luqui使用Codensity：两个b都被任意类型构造器泛化，我们将其称为f。这是f a的Codensity变换。
type CodenseBox f a = forall b. (a -> f b) -> f b
f ~ Identity进行修复，那么我们会得到Box。但是，还有另一种选择：我们只需使用f作用于返回类型即可。type YonedaBox f a = forall b. (a -> b) -> f b
（我在这里暴露了游戏的名字，但我们会回到那里。）我们也可以在此处修复f〜Identity以恢复Box，但我们让盒子用户传入一个普通函数而不是Kleisli箭头。为了理解我们正在泛化的内容，让我们再次看一下box的定义：
box a f = f a
嗯，这只是flip($)，对吧？而我们的另外两个盒子是通过泛化($)构建的：CodenseBox是一个部分应用的、翻转的单子绑定，而YonedaBox则是一个部分应用的flip fmap。（这也解释了为什么对于任何选择的f，Codensity f是一个Monad，而Yoneda f是一个Functor：创建它们的唯一方法是通过闭包绑定或fmap）。此外，这两个奇特的范畴论概念都是一个概念的普遍化，这个概念对许多工作程序员来说是熟悉的：CPS变换！
换句话说，YonedaBox是Yoneda嵌入，而适当抽象的box/unbox法则对于YonedaBox是Yoneda引理的证明！
简而言之：
forall b. (a -> b) -> b === a是Yoneda引理的一个实例。
type ApplicativeBox f a = forall b. f (a -> b) -> f b 是什么。 - minimalisa ~ Bool。因此，我们有forall b.（Bool-> b）-> b。我没有看到这如何在a和forall b.中是参数化的。您说“盒子制造者选择a，盒子使用者选择b。”盒子使用者必须事先知道盒子制造者为a选择了什么。然后，我们必须重载函数（或其他东西）以依赖于对a的选择。 - AntCa选择了什么，因为盒子制造者在制作盒子时已经选择了a。无论如何，争论这个问题没有意义，当你可以在GHCi中花30秒来自我说服。 - Rein Henrichsunbox . box = id 这个证明是比较简单的。box . unbox = id 需要一个参数性假设，因此不是一个同样简单的证明。 - luqui这个问题窥视了一些更深层次的概念。
首先，注意这个问题存在歧义。我们是指forall b. (a -> b) -> b类型，以便我们可以将b实例化为任何我们喜欢的类型，还是指对于某些特定的b，我们无法选择(a -> b) -> b。
我们可以在Haskell中这样形式化这种区别：
newtype Cont b a = Cont ((a -> b) -> b)
newtype Cod a = Cod (forall b. (a -> b) -> b)
这里我们看到一些术语。第一种类型是Cont单子，第二种是CodensityIdentity，尽管我对后者的熟悉程度不足以确定你应该用什么英文词来称呼它。
除非 a -> b 至少可以容纳与 a 相同的信息量（见Dan Robertson的评论），否则 Cont b a 不能等价于 a。例如，请注意您永远无法从 ContVoida 中获取任何内容。
Cod a 等同于 a。为了证明这一点，我们只需证明以下同构关系即可：
toCod :: a -> Cod a
fromCod :: Cod a -> a
实现可以留作练习。如果你想深入研究，可以尝试证明这对的确是同构。 fromCod . toCod = id 很容易证明，但要证明 toCod . fromCod = id 则需要使用 Cod 的自由定理。
b包含的信息比a少，cont b a也可能等同于a。重要的是b^a可以容纳多少信息。例如，任何可数和递归可枚举类型a都等同于cont a Bool，如果一个类型是有界的并支持区间二分（例如将自然数映射到${0,1}$的函数，即在[0,1]中的可计算实数（粗略地）），那么它就是同构于Cont a Ord。 - Dan Robertsonforall b . (a -> b) -> b 和 a 之间的关系，但我想指出一个注意点，因为它引发了一些有趣的开放性问题，而我一直在研究这个问题。forall b . (a -> b) -> b 和 a 在某种程度上并不是同构的，因为该语言（1）允许你编写不终止的表达式，并且（2）要么是按值调用（严格），要么包含 seq。我的观点并不是为了挑剔或展示 Haskell 中参数化被削弱了（众所周知），而是可能有巧妙的方法来加强它，在某种意义上重新获得像这样的同构。forall b . (a -> b) -> b 的术语不能表示为 a。为了看清原因，让我们从 Rein 留作练习的证明 box . unbox = id 开始。事实证明，这个证明比他的回答更有趣，因为它在关键的方式上依赖于参数化。box . unbox
= {- definition of (.) -}
\m -> box (unbox m)
= {- definition of box -}
\m f -> f (unbox m)
= {- definition of unbox -}
\m f -> f (m id)
= {- free theorem: f (m id) = m f -}
\m f -> m f
= {- eta: (\f -> m f) = m -}
\m -> m
= {- definition of id, backwards -}
id
m :: (Bool -> b) -> b
m k = seq (k true) (k false)
f :: Bool -> Int
f x = if x then ⊥ else 2`
回想一下，我们想要展示f (m id) = m f
f (m id)
= {- definition f -}
if (m id) then ⊥ else 2
= {- definition of m -}
if (seq (id true) (id false)) then ⊥ else 2
= {- definition of id -}
if (seq true (id false)) then ⊥ else 2
= {- definition of seq -}
if (id false) then ⊥ else 2
= {- definition of id -}
if false then ⊥ else 2
= {- definition of if -}
2
m f
= {- definition of m -}
seq (f true) (f false)
= {- definition of f -}
seq (if true then ⊥ else 2) (f false)
= {- definition of if -}
seq ⊥ (f false)
= {- definition of seq -}
⊥
2不等于⊥，所以我们失去了自由定理和a与(a -> b) -> b之间的同构性。但是，到底发生了什么？基本上，m不仅仅是一个行为良好的盒子，因为它将其参数应用于两个不同的基础值（并使用seq确保这两个应用实际上被评估），我们可以通过传递在其中一个基础值上终止的连续函数来观察到这一点，但不是另一个基础值。换句话说，m id = false并不是m作为Bool的一个忠实表示，因为它“遗忘”了m调用其输入时使用bothtrue和false这一事实。
这个问题是三个因素相互作用的结果：
seq的存在。forall b . (a -> b) -> b的术语可能多次应用其输入。很难摆脱第1点或第2点。然而，线性类型可以让我们有机会解决第三个问题。类型为a ⊸ b的线性函数是从类型a到类型b的函数，它必须恰好使用其输入一次。如果我们要求m具有类型forall b . (a -> b) ⊸ b，那么这将排除我们反例自由定理，并应该让我们在存在非终止和seq的情况下展示a与forall b . (a -> b) ⊸ b之间的同构性。
这真的很酷！它表明线性具有通过驯服可能使真正等式推理困难的效果来“拯救”有趣的特性的能力。
然而，仍然存在一个重大问题。我们还没有证明需要类型forall b . (a -> b) ⊸ b的自由定理的技术。事实证明，当前的逻辑关系（我们通常用来做这样的证明的工具）还没有被设计成考虑到所需的线性。这个问题对于建立执行CPS转换的编译器的正确性具有影响。
f = id，并获取实际的a实例，或者我有什么遗漏。 - harold(a -> b) -> b同构于a。 - Mark Bolusmjakforall b. (a -> b) -> b，还是针对特定的b指(a -> b) -> b？ - luquiF = Id带入 Yoneda 引理 可得 Cf. Yoneda 引理。 - gallaisa可能在地球的另一端，被锁在笼子里，钥匙在井里，由老人保管等等。 - nicolas(a -> b) -> b的东西？”-- 顺便说一句，我喜欢“挂起计算”或“挂起”，这是从这个经典答案中得到的启示。 - duplode