如何理解Yoneda的自然同构中的普遍量化？

Question

在学习Yoneda引理时，我遇到了Haskell中基本自然同构的以下编码：

forward  :: Functor f => (forall r . (a -> r) -> f r) -> f a
forward  f = f id

backward  :: Functor f => f a -> (forall r. (a -> r) -> f r)
backward  x f = fmap f x

我试图简化向后 to flip fmap的实现，但失败了后者具有类型fa-＆gt; （a - ＆gt; r） - ＆gt; f r。

从这里开始，我被困在指出两个实现之间的差异是什么。更重要的是，将任何一个函数应用于混凝土函子都会产生相同的结果类型：

ghci> :t bw (Just "") 
bw (Just "") :: (String -> r) -> Maybe r

ghci> :t (flip fmap)  (Just "") 
(flip fmap)  (Just "") :: (String -> r) -> Maybe r

问题：

• 两者之间的差异到底是什么？
• 我可以用一个不能与另一个做些什么？
• 为什么向后完全需要通用量化？

Answer 1

在Haskell中，我们为我们传达的值编写lambdas：

id :: forall a . a->a
id = \x -> x

但是，当我们编译为封闭于系统F的低级核心语言时，我们还会看到 type lambdas 。代码变得更像

id = \ @a (x :: @a) -> x

是：呼叫者应选择并传递类型@A，然后是该类型的值x :: @a，最后回到X。

现在，您的问题来自

forall a . T -> U a
--  vs
T -> forall a . U a

此处的两种（同构）类型，t不取决于a。这两种类型确实是同构的，在较低的层面上，这只是用类型lambda“翻转”术语的问题：

\ @a (x :: T) -> ...  -- has the former type
-- vs
\ (x :: T) @a -> ...  -- has the latter

由于在Haskell中，我们通常不会写或看到类型 - lambdas，因此很难区分在这之间。此外，当编译器执行类型推理时，它将（据我所知）推断出第一个类型的推断，其中类型 - lambdas都是开始的。

两者到底有什么区别？

不多。毕竟，它们具有同构类型。一个在最高级别上具有forall a，而另一个则位于另一个位置。

一旦您像以前一样应用对参数，GHC将自动选择添加推断@A参数的正确位置，因此您不会轻易注意到差异。这两个呼叫是这些形式的：

f @r x
-- vs
f x @r

最重要的是，GHC可以重新将类型重新化，因此我们获得了

(\@r -> f @r x) :: forall r . ....
(\@r -> f x @r) :: forall r . ....

我可以用一个不能用另一个做的事情吗？

并不真地。

为什么完全需要通用量化才能向后？

通常，当定义a和b之间的同构时，我们想要

forw :: A -> B
back :: B -> A

任何一种类型都有forall（例如，a = forallr。vr）然后，我们在该职位上得到一个福特。请注意，在这种情况下，back的类型也是异摩式，

forall r . B -> V r

如果我们省略了量词，我们将获得的类型（并让Haskell重新添加它在顶级级别上）。

（相比之下，forw ::（Forallr。vr）类型中的量词无法移动到顶级。