有（a – > b） – > b`相当于有一个`a`？
在一个纯粹的函数式语言中，你可以用一个值做的唯一事情就是对它应用一个函数。
换句话说，如果你想用typesa的值做任何有趣的事情，你需要一个types为f :: a -> b的函数，然后应用它。 如果有人用(a -> b) -> b给你(flip apply) a (a -> b) -> b ，那么是否适合replace？
你会用types(a -> b) -> b调用什么？ 看来，这似乎是一个a的替身，我很想把它称为代理，或从http://www.thesaurus.com/browse/proxy 。
luqui的回答非常好，但是我会给出另一个解释forall b. (a -> b) -> b === a forall b. (a -> b) -> b === a有几个原因：首先，因为我认为Codensity的泛化有点过分。 第二，因为这是一个把一堆有趣的事情联系在一起的机会。 向前！
z5h的魔术盒
想象一下，有人翻了一个硬币，然后把它放在一个魔术盒里。 你看不到盒子里面的内容，但是如果你select一个typesb并且把一个types为Bool -> b的函数传递给这个盒子，那么这个盒子就会吐出一个b 。 我们可以从里面看到这个盒子，我们可以学到什么？ 我们可以知道硬币的状态是什么吗？ 我们可以知道盒子用来产生b吗？ 事实certificate，我们可以做到这一点。
我们可以将Box Bool定义为Box Booltypes的2级函数
type Box a = forall b. (a -> b) -> b
（在这里，等级2types意味着制造商selecta和盒子用户selectb 。
我们把a放在盒子里，然后closures盒子，创build一个闭包 。
-- Put the a in the box. box :: a -> Box a box af = fa
例如， box True 。 部分应用程序只是一个聪明的方法来创build闭包！
现在，硬币头还是尾巴？ 由于我，盒子用户，我可以selectb ，我可以selectBool并通过一个函数Bool -> Bool 。 如果我selectid :: Bool -> Bool那么问题是：盒子会吐出它包含的值吗？ 答案是盒子会吐出它所包含的值，或者它会吐出无意义的东西（底部值如undefined ）。 换句话说，如果你得到答案，那么答案必须是正确的。
-- Get the a out of the box. unbox :: Box a -> a unbox f = f id
因为我们不能在Haskell中生成任意值，所以这个盒子唯一能做的就是将给定的函数应用到它隐藏的值。 这是参数多态性的结果，也称为参数性 。
现在，为了certificateBox a同构于a ，我们需要certificate两件关于装箱和拆箱的事情。 我们需要certificate你放弃了你放入的东西，并且可以放入你的东西。
unbox . box = id box . unbox = id
我会做第一个，把第二个作为练习给读者。
unbox . box = {- definition of (.) -} \b -> unbox (box b) = {- definition of unbox and (fa) b = fab -} \b -> box b id = {- definition of box -} \b -> id b = {- definition of id -} \b -> b = {- definition of id, backwards -} id
（如果这些certificate看起来相当微不足道，那是因为Haskell中所有（全部）多态函数都是自然变换，我们在这里certificate的是自然性。参数性再一次为我们提供了价格低，价格低的定理！
作为读者的另一个练习，为什么我实际上rebox用(.)定义rebox ？
rebox = box . unbox
为什么我要把(.)自己的定义像某种洞穴人一样？
rebox :: Box a -> Box a rebox f = box (unbox f)
（提示： box ， unbox和(.)是什么types？）
身份和密码和Yoneda，哦，我的！
现在，我们如何推广Box ？ luqui使用Codensity ：两个b都被一个任意types的构造函数推广，我们将其称为f 。 这是fa的密度转换 。
type CodenseBox fa = forall b. (a -> fb) -> fb
如果我们修正f ~ Identity那么我们回到Box 。 不过，还有另一种select：我们只能用f返回types：
type YonedaBox fa = forall b. (a -> b) -> fb
（我已经把这个名字给了这个游戏，但是我们会回到这个）。我们也可以在这里修复f ~ Identity来恢复Box ，但是我们让Box用户通过一个普通的函数而不是Kleisli箭头。 为了理解我们正在推广的内容，我们再来看一下box的定义：
box af = fa
那么，这只是flip ($) ，不是吗？ 事实certificate，我们的另外两个框是通过泛化($)构build的： CodenseBox是一个部分应用的翻转YonedaBox绑定， YonedaBox是部分应用的flip fmap 。 （这也解释了为什么Codensity f是Monad和Yoneda f是Yoneda f的任何select的Functor ：创build一个的唯一方法是分别closuresbind或fmap。）另外，这两个深奥的范畴理论概念都是真正概括了许多工作程序员所熟悉的概念：CPS转换！
换句话说， YonedaBox是Yoneda的embedded， YonedaBox的正确抽象的box / unbox规则是Yoneda引理的certificate！
TL; DR：
forall b. (a -> b) -> b === a forall b. (a -> b) -> b === a是Yoneda引理的一个实例。
这个问题是一个更深入的概念的窗口。
首先，请注意，这个问题存在一个模棱两可的问题。 我们的意思是所有的typesforall b. (a -> b) -> b forall b. (a -> b) -> b ，这样我们可以用任何types的实例化b ，或者我们的意思是(a -> b) -> b对于某些我们不能select的具体b 。
我们可以在Haskell中正式确定这个区别：
newtype Cont ba = Cont ((a -> b) -> b) newtype Cod a = Cod (forall b. (a -> b) -> b)
这里我们看到一些词汇。 第一种是Cont monad，第二种是Codensity Identity ，尽pipe我对后一个词的熟悉程度还不足以说明你应该用英语说什么。
除非a -> b至less可以包含尽可能多的信息（参见下面的Dan Robertson的评论），否则不能等同于a 。 因此，例如，请注意，您无法从Cont Void a获取任何内容。
Cod a相当于a 。 看到这个就足以见证同构：
toCod :: a -> Cod a fromCod :: Cod a -> a
我将作为练习离开。 如果你想真正做到这一点，你可以试着certificate这一对真的是一个同构。 fromCod . toCod = id fromCod . toCod = id很容易，但toCod . fromCod = id toCod . fromCod = id需要Cod的自由定理 。
其他答案在描述types(a -> b) -> b和a之间的关系方面做了很大的工作，但是我想指出一个警告，因为它会导致我一直在研究的一些有趣的开放性问题。
从技术上讲， (a -> b) -> b和a在Haskell这样a中不是同构的，它允许你写一个不终止的expression式，（2）是按值（strict）或包含seq 。 我的观点不是挑剔的，也不是说Haskell中的参数性被削弱（众所周知），但是可能有一些很好的方法来加强它，从某种意义上说，像这样的一个同构就是回收。
有一些术语(a -> b) -> b不能表示为a 。 为了明白为什么，让我们先看看Rein留下的作为练习的框架box . unbox = id box . unbox = id 。 事实certificate，这个certificate实际上比他的答案更有趣，因为它以关键的方式依赖于参数。
box . unbox = {- definition of (.) -} \m -> box (unbox m) = {- definition of box -} \mf -> f (unbox m) = {- definition of unbox -} \mf -> f (m id) = {- free theorem: f (m id) = mf -} \mf -> mf = {- eta: (\f -> mf) = m -} \m -> m = {- definition of id, backwards -} id
参数性起作用的有趣步骤是应用自由定理 f (m id) = mf 。 这个属性是(a -> b) -> b ， m的types。 如果我们把m看作一个内部types为a的基础值的盒子，那么m可以用它的参数做的唯一的事情就是将它应用到这个基础值并返回结果。 在左边，这意味着f (m id)从框中提取基础值，并将其传递给f 。 在右边，这意味着m将f直接应用于基础值。
不幸的是，当我们有像下面的m和f这样的术语时，这个推理并不成立。
m :: (Bool -> b) -> b mk = seq (k true) (k false) f :: Bool -> Int fx = if x then ⊥ else 2`
回想一下，我们想显示f (m id) = mf
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 mf = {- 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用true和false调用input的事实。
问题是三件事情之间的相互作用的结果：
- 非终止的存在
- seq的存在。
- types
(a -> b) -> b术语可以多次应用它们的input。
没有太多的希望得到点1或2. 线性types可能会给我们一个机会来解决第三个问题，但是。 typesa ⊸ b 线性函数是从a到b的函数，它必须使用其input一次。 如果我们要求m有types(a -> b) ⊸ b ，那么这就排除了我们对自由定理的反例，并且应该让我们展示a和(a -> b) ⊸ b之间的同构， 即使在非终止和seq 。
这真的很酷！ 它表明，线性有能力通过驯服效应来“拯救”有趣的属性，使真正的等式推理变得困难。
但是，一个大问题仍然存在。 我们还没有技术来certificate我们需要的自由定理(a -> b) ⊸ b 。 事实certificate，当前的逻辑关系（我们通常用来做这种certificate的工具）并没有被devise成以所需的方式考虑线性。 这个问题对build立CPS翻译的编译器的正确性有影响。
