有一个`(a - > b) - > b`等同于'a`？

Question

在纯函数式语言中,您可以对值执行的唯一操作是对其应用函数.

换句话说,如果你想用类型值做任何有趣的事情,a你需要一个带有类型的函数(例如),f :: a -> b然后应用它.如果有人用你(flip apply) a的类型交给你(a -> b) -> b,那是否适合替代a？

什么叫做类型的东西(a -> b) -> b？看起来它似乎是一个替身a,我很想把它称为代理,或来自http://www.thesaurus.com/browse/proxy的东西.

Answer 1

luqui的回答非常好,但我会提出另外一个解释,forall b. (a -> b) -> b === a原因有几个:第一,因为我认为对Codensity的概括有点过于热情.第二,因为这是将一堆有趣的东西联系在一起的机会.向前!

z5h的魔盒

想象一下,有人翻了一个硬币然后把它放在一个魔术盒里.你不能在盒子里面看到,但是如果你选择一种类型b并且在盒子中传递一个带有该类型的函数Bool -> b,那么盒子就会吐出一个b.如果不深入了解这个盒子我们能学到什么？我们可以了解硬币的状态吗？我们可以了解盒子用来制作的机制b吗？事实证明,我们可以做到这两点.

我们可以将框定义为类型where的2级函数Box Bool

type Box a = forall b. (a -> b) -> b

(此处,等级2类型表示盒子制造商选择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

因为我们不能在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中的所有(全部)多态函数都是自然变换,我们在这里证明的是自然性.参数化再一次为我们提供了低价,低价的定理!)

顺便说一句,另一个读者练习,我为什么不能实际上定义rebox有(.)？

rebox = box . unbox

为什么我必须(.)像某种洞穴人一样内联自己的定义？

rebox :: Box a -> Box a
rebox f = box (unbox f)

(提示:是什么类型的box,unbox和(.)？)

身份和密度和Yoneda,哦,我的!

现在,我们如何概括Box？luqui使用Codensity:两个bs都由我们将调用的任意类型构造函数推广f.这是Codensity 变换的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箭头.要了解什么,我们正在推广,让我们再次定义一下box:

box a f = f a

嗯,这只是flip ($),不是吗？事实证明,我们的另外两个盒子是通过推广构建的($):CodenseBox是部分应用的,翻转的monadic绑定并且YonedaBox是部分应用的flip fmap.(这也解释了为什么Codensity fa Monad和Yoneda fa Functor是任意选择f:创建一个的唯一方法是分别关闭一个bind或fmap.)此外,这两个深奥的类别理论概念都是一个概念的概括,许多工作程序员都熟悉:CPS转换!

换句话说,YonedaBoxYoneda嵌入和正确抽象box/ unbox法律YonedaBox是Yoneda引理的证明!

TL; DR:

forall b. (a -> b) -> b === a 是Yoneda引理的一个例子.

Answer 2

这个问题是一个了解更多深层概念的窗口.

首先,请注意这个问题存在歧义.我们是指类型forall b. (a -> b) -> b,以便我们可以b使用我们喜欢的任何类型进行实例化,或者我们是指(a -> b) -> b某些b我们无法选择的特定类型.

我们可以在Haskell中形式化这种区别:

newtype Cont b a = Cont ((a -> b) -> b)
newtype Cod a    = Cod (forall b. (a -> b) -> b)

在这里我们看到一些词汇.第一种是Contmonad,第二种是,虽然我对后一种术语的熟悉程度不够强,无法用英语说出你应该称之为什么.CodensityIdentity

Cont b a不能等同于a除非a -> b能够保存至少尽可能多的信息a(参见Dan Robertson在下面的评论).因此,例如,请注意,您永远无法获得任何东西.ContVoida

Cod a相当于a.要看到这一点就足以见证同构:

toCod :: a -> Cod a
fromCod :: Cod a -> a

我将作为练习留下的实现.如果你想真正做到这一点,你可以尝试证明这对真的是一个同构. fromCod . toCod = id很容易,但toCod . fromCod = id需要自由定理的Cod.

Answer 3

其他答案在描述类型之间的关系方面做得很好forall b . (a -> b) -> b,a但我想指出一个警告,因为它会导致我一直在研究的一些有趣的开放式问题.

从技术上讲,forall b . (a -> b) -> b并且a是不同构在象Haskell一个的langauge其中(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

参数化发挥作用的有趣步骤是应用自由定理 f (m id) = m f.这个属性的后果forall b . (a -> b) -> b是m.如果我们认为m是一个a内部类型为底层值的框,那么唯一m可以用它的参数做的就是将它应用于这个底层值并返回结果.在左侧,这意味着f (m id)从框中提取基础值,并将其传递给f.在右侧,这意味着直接m应用于f基础值.

不幸的是,这种推理并不完全当我们有像条款任职m及f以下.

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调用它的输入都 true和false.

问题是三件事之间相互作用的结果:

1. 不确定的存在.
2. seq的存在.
3. 类型条款forall b . (a -> b) -> b可以多次应用其输入的事实.

没有太多的希望绕过第1或第2点.线性类型可能会给我们一个机会来解决第三个问题.类型的线性函数a ? b是从类型a到类型的函数,b它必须使用其输入一次.如果我们需要m有型forall b . (a -> b) ? b,那么这个规则我们反到免费的定理和应该让我们展示之间的同构a和forall b . (a -> b) ? b 甚至在nontermination的存在和seq.

这真的很酷!它表明,线性有能力通过驯服效应来"拯救"有趣的属性,这种效应可以使真正的等式推理变得困难.

但是,一个大问题仍然存在.我们还没有技术来证明我们需要的自由定理forall b . (a -> b) ? b.事实证明,当前的逻辑关系(我们通常用来做这种证明的工具)并没有被设计成以所需的方式考虑线性.此问题对于为执行CPS转换的编译器建立正确性有影响.