有一个`（a - > b） - > b`相当于有`a`？ [英] Is having a `(a -> b) -> b` equivalent to having an `a`?
问题描述
在纯粹的函数式语言中，你可以用值做的唯一事情就是对它应用一个函数。换句话说，如果你想做任何事情有趣的是 a 类型的值，您需要一个类型为 f :: a - >的函数（例如） b 然后应用它。如果有人用（a - > b） - >类型给您< b ，是否可以替代 a ？
你会用（a - > b） - > B'/ code>？看起来它似乎是 a 的替身，我很想将它称为代理，或者来自 http://www.thesaurus.com/browse/proxy 。
luqui的答案非常好，但我会提供 forall b的另一个解释。 （a - > b） - > b === a 出于几个原因：首先，因为我认为Codensity的泛化有点过分。其次，因为这是一个把一些有趣的事情联系在一起的机会。向前！
z5h的魔术盒
想象一下，有人翻转一枚硬币然后放入魔术盒。你不能在箱子里面看到，但是如果你选择一个类型 b 并且传入一个函数，其类型为 Bool - > b ，该盒子会吐出一个 b 。我们可以了解一下这个盒子，而不是在里面看一看？我们可以知道硬币的状态是什么吗？我们可以了解该盒子用于生成 b 的机制吗？事实证明，我们可以做到这一点。
我们可以将该框定义为类型的一个 rank 2 函数， Box Bool 其中
type Box a = forall b。 （a - > b） - > b
（这里，等级2类型意味着制造商选择 a 和框用户选择 b 。）
我们把 a ，然后关闭该框，创建... 闭包。
- 将a放入框中。
box :: a - > Box a
box af = fa
例如， box True 。部分应用程序只是一个聪明的方法来创建闭包！
现在，硬币正面还是反面？因为我允许box用户选择 b ，所以我可以选择 Bool 并传入一个函数 Bool - >布尔。如果我选择 id :: Bool - > Bool 然后问题是：盒子会吐出它包含的值吗？答案是盒子会吐出它所包含的值，或者它会吐出无意义的东西（底部值如 undefined ）。换句话说，如果你得到了答案，那么答案必须是正确的。
- 获取开箱即用。
unbox :: Box a - > a
unbox f = f id
因为我们不能在Haskell中生成任意值，盒子可以做的唯一有意义的事情是将给定的函数应用到它隐藏的值。这是参数多态性的结果，也称为 parametricity 。
现在，为了显示
Box a 同构于 a ，我们需要证明有关装箱和拆箱的两件事情。我们需要证明你放弃了你放入的东西，并且你可以放入你的东西。 unbox。 box = id
box。 unbox = id
我会做第一个，然后把第二个作为练习给读者。
unbox。 box
= { - （。） - 的定义}
\ b - > unbox（box b）
= { - unbox的定义和（f a）b = f a b - }
\ b - > box b id
= { - box的定义 - }
\b - > id b
= { - id的定义 - }
\b - > b
= { - id的定义，向后 - }
id
（如果这些证明看起来相当微不足道，那是因为Haskell中所有（全部）多态函数都是自然变换，我们在这里证明的是自然。参数性再次为我们提供了价格低，价格低的定理！ ）
作为读者的另一个练习，为什么我不能用<$实际定义 rebox c $ c>（。）
？ rebox =框。 unbox
为什么我必须内联定义（。）我自己喜欢某种洞穴人？
rebox :: Box a - > Box a
rebox f = box（unbox f）
（提示：什么类型 box ， unbox 和（。）？）
身份和Codensity和Yoneda，哦我的！
现在，我们如何概括箱？ luqui使用 Codensity ：均 b s被任意类型的构造函数推广，我们将称之为 f 。这是 fa 的Codensity 转换。 / code>。
type CodenseBox fa = forall b。 （a - > f b） - > fb
如果我们修正 f〜Identity ，那么我们得到 Box 。但是，还有另外一种选择：我们只能用 f 命中返回类型：
输入YonedaBox fa = forall b。 （a - > b） - > fb
（我用这个名字在这里给出了一些游戏，但我们会回来）我们也可以在这里修复 f〜Identity 来恢复 Box ，但我们让box用户通过一个正常的功能，而不是一个Kleisli箭头。要理解我们概括的是什么，我们再来看看框的定义：
box af = fa
好的，这只是 flip（$），不是吗？事实证明，我们的其他两个盒子是通过概括（$）： CodenseBox 是部分应用的，翻转monadic bind和 YonedaBox 是部分应用的 flip fmap 。 （这也解释了为什么 Codensity f 是 Monad 和 Yoneda f 是 Functor 用于 f 的任何选择：创建一个通过分别关闭bind或fmap）。另外，这两个深奥的范畴理论概念实际上是许多工作程序员熟悉的概念的概括：CPS变换！
换句话说， YonedaBox 是Yoneda嵌入和正确抽象的框 / unbox YonedaBox
的法则是Yoneda引理的证明！ TL; DR：
forall b。 （a - > b） - > b === a 是Yoneda引理的一个实例。
In a pure functional language, the only thing you can do with a value is apply a function to it.
In other words, if you want to do anything interesting with a value of type a you need a function (for example) with type f :: a -> b and then apply it. If someone hands you (flip apply) a with type (a -> b) -> b, is that a suitable replacement for a?
And what would you call something with type (a -> b) -> b? Seeing as it appears to be a stand-in for an a, I'd be tempted to call it a proxy, or something from http://www.thesaurus.com/browse/proxy.
luqui's answer is excellent but I'm going to offer another explanation of forall b. (a -> b) -> b === a for a couple reasons: First, because I think the generalization to Codensity is a bit overenthusiastic. And second, because it's an opportunity to tie a bunch of interesting things together. Onwards!
z5h's Magic Box
Imagine that someone flipped a coin and then put it in a magic box. You can't see inside the box but if you choose a type b and pass the box a function with the type Bool -> b, the box will spit out a b. What can we learn about this box without looking inside it? Can we learn what the state of the coin is? Can we learn what mechanism the box uses to produce the b? As it turns out, we can do both.
We can define the box as a rank 2 function of type Box Bool where
type Box a = forall b. (a -> b) -> b
(Here, the rank 2 type means that the box maker chooses a and the box user chooses b.)
We put the a in the box and then we close the box, creating... a closure.
-- Put the a in the box.
box :: a -> Box a
box a f = f a
For example, box True. Partial application is just a clever way to create closures!
Now, is the coin heads or tails? Since I, the box user, am allowed to choose b, I can choose Bool and pass in a function Bool -> Bool. If I choose id :: Bool -> Bool then the question is: will the box spit out the value it contains? The answer is that the box will either spit out the value it contains or it will spit out nonsense (a bottom value like undefined). In other words, if you get an answer then that answer must be correct.
-- Get the a out of the box.
unbox :: Box a -> a
unbox f = f id
Because we can't generate arbitrary values in Haskell, the only sensical thing the box can do is apply the given function to the value it is hiding. This is a consequence of parametric polymorphism, also known as parametricity.
Now, to show that Box a is isomorphic to a, we need to prove two things about boxing and unboxing. We need to prove that you get out what you put in and that you can put in what you get out.
unbox . box = id
box . unbox = id
I'll do the first one and leave the second as an exercise for the reader.
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
(If these proofs seem rather trivial, that's because all (total) polymorphic functions in Haskell are natural transformations and what we're proving here is naturality. Parametricity once again provides us with theorems for low, low prices!)
As an aside and another exercise for the reader, why can't I actually define rebox with (.)?
rebox = box . unbox
Why do I have to inline the definition of (.) myself like some sort of cave person?
rebox :: Box a -> Box a
rebox f = box (unbox f)
(Hint: what are the types of box, unbox, and (.)?)
Identity and Codensity and Yoneda, Oh My!
Now, how can we generalize Box? luqui uses Codensity: both bs are generalized by an arbitrary type constructor which we will call f. This is the Codensity transform of f a.
type CodenseBox f a = forall b. (a -> f b) -> f b
If we fix f ~ Identity then we get back Box. However, there's another option: we can hit only the return type with f:
type YonedaBox f a = forall b. (a -> b) -> f b
(I've sort of given away the game here with this name but we'll come back to that.) We can also fix f ~ Identity here to recover Box, but we let the box user pass in a normal function rather than a Kleisli arrow. To understand what we're generalizing, let's look again at the definition of box:
box a f = f a
Well, this is just flip ($), isn't it? And it turns out that our other two boxes are built by generalizing ($): CodenseBox is a partially applied, flipped monadic bind and YonedaBox is a partially applied flip fmap. (This also explains why Codensity f is a Monad and Yoneda f is a Functor for any choice of f: The only way to create one is by closing over a bind or fmap, respectively.) Furthermore, both of these esoteric category theory concepts are really generalizations of a concept that is familiar to many working programmers: the CPS transform!
In other words, YonedaBox is the Yoneda Embedding and the properly abstracted box/unbox laws for YonedaBox are the proof of the Yoneda Lemma!
TL;DR:
forall b. (a -> b) -> b === a is an instance of the Yoneda Lemma.
这篇关于有一个`（a - > b） - > b`相当于有`a`？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！
