haskell - 证明 Haskell Lens 库中断言的类型等效性的合理性

Question

根据tutorial on Lenses :

type Getting b a b  = (b -> Const b b) -> (a -> Const b a)

-- ... equivalent to: (b ->       b  ) -> (a ->       b  )

-- ... equivalent to:                     (a ->       b  )

问题:为什么(b -> b) -> (a -> b) 等价于(a -> b) ？

Answer 1

本教程对此不是很精确。这是 Getting 的完整定义:

type Getting r s a = (a -> Const r a) -> s -> Const r s

剥离newtype噪音，

Getting r s a ~= (a -> r) -> s -> r

您应该从中得到的有趣的同构如下:

(forall r. Getting r s a) ~= s -> a

在一条现已删除的评论中，chi 指出这是 Yoneda lemma 的一个特例。 .

同构的见证是

fromGetting :: Getting a s a -> (s -> a)
fromGetting g = getConst . g Const
           -- ~= g id

-- Note that the type of fromGetting is a harmless generalization of
-- fromGetting :: (forall r. Getting r s a) -> (s -> a)

toGetting :: (s -> a) -> Getting r s a
toGetting f g = Const . getConst . g . f
           -- ~= g . f

-- Note that you can read the signature of toGetting as
-- toGetting :: (s -> a) -> (forall r. Getting r s a)

都不是fromGetting也不toGetting具有 2 级类型，但为了描述同构，forall是必不可少的。为什么这是同构？

一方面很简单:忽略Const噪音，

  fromGetting (toGetting f)
= toGetting f id
= id . f
= f

另一面更棘手。

  toGetting (fromGetting f)
= toGetting (f id)
= \g -> toGetting (f id) g
= \g -> g . f id

为什么这相当于 f ？ forall是这里的关键:

f :: forall r. Getting r s a
  -- forall r. (a -> r) -> s -> r

f无法生成r除非将传递的函数(我们称之为 p )应用于 a 类型的值。除了 p 之外什么也没有给出和 s 类型的值。所以f除了提取 a 之外，真的无能为力来自s并申请p到结果。即f p必须将“因子”分解为两个函数的组合:

f p = p . h

所以

g . f id = g . (id . h) = g . h = f g