卢基的回答非常好，但我要提供另一种解释forall b. (a -> b) -> b === a有几个原因：首先，因为我认为对 Co密度的概括有点过于热情。其次，因为这是一个将一堆有趣的事情联系在一起的机会。向前！
z5h的魔盒
想象一下，有人抛了一枚硬币，然后将其放入一个魔法盒中。您看不到盒子内部，但如果您选择一种类型b并向盒子传递一个类型为的函数Bool -> b，盒子会吐出一个b。如果不看盒子内部，我们能了解到什么？我们能知道硬币的状态是什么吗？我们能否了解盒子使用什么机制来产生b？事实证明，我们可以两者兼得。
我们可以将盒子定义为rank 2类型函数Box Bool where
type Box a = forall b. (a -> b) -> b
（这里，等级2类型意味着盒子制造商选择a和盒子用户选择b.)
我们把a放在盒子里，然后我们关闭盒子，创建......closure.
-- 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）。换句话说，如果你得到一个答案，那么这个答案must是正确的。
-- Get the a out of the box.
unbox :: Box a -> a
unbox f = f id
因为我们无法在 Haskell 中生成任意值，所以盒子能做的唯一有意义的事情就是将给定的函数应用于它隐藏的值。这是参数多态性的结果，也称为参数化.
现在，为了表明Box a同构于a，我们需要证明关于装箱和拆箱的两件事。我们需要证明你投入了什么就能得到什么，并且你可以投入你得到的东西。
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 中的所有（全部）多态函数都是自然变换，而我们在这里证明的is自然性。参数化再次为我们提供了极低价格的定理！）
作为读者的旁白和另一个练习，为什么我不能真正定义rebox with (.)?
rebox = box . unbox
为什么我必须内联定义(.)我自己就像某种穴居人吗？
rebox :: Box a -> Box a
rebox f = box (unbox f)
（提示：有哪些类型box, unbox, and (.)?)
身份与密度和米田，天哪！
现在，我们如何概括Box？卢基使用密度 http://hackage.haskell.org/package/kan-extensions-5.0.2/docs/Control-Monad-Codensity.html: both bs 由任意类型构造函数泛化，我们将调用该构造函数f。这是代码密度转换 http://comonad.com/reader/2011/free-monads-for-less/ of f a.
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 箭头。要了解what我们正在概括，让我们再看看它的定义box:
box a f = f a
嗯，这只是flip ($)，不是吗？事实证明，我们的另外两个盒子是通过泛化构建的($): CodenseBox是一个部分应用的、翻转的一元绑定，YonedaBox是部分应用的flip fmap。 （这也解释了为什么Codensity f is a Monad and Yoneda f is a Functor for any的选择f：创建一个的唯一方法是分别关闭绑定或 fmap。）此外，这两个深奥的范畴论概念实际上是许多程序员熟悉的概念的概括：CPS 变换！
换句话说，YonedaBox是米田嵌入和正确抽象的box/unbox法律为YonedaBox是米田引理的证明！
TL;DR:
forall b. (a -> b) -> b === a是米田引理的一个实例。
