证明在Haskell镜头库中断言的类型等价性

Question

根据镜头教程:

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引理的一个特例.

同构见证了

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