haskell - 如何在 CPS 中构建更高等级的 Coyoneda 类型的值？

Question

{-# LANGUAGE RankNTypes #-}

newtype Coyoneda f a = Coyoneda {
  uncoyo :: forall b r. ((b -> a) -> f b -> r) -> r
}

coyoneda f tx = Coyoneda (\k -> k f tx)

我想 Coyoneda应该通过模拟更高等级类型的存在来工作，但我无法构造这种类型的值。 coyoneda辅助函数不进行类型检查，因为关于术语 k f tx高阶类型变量 b会脱离它的范围。
但是，我想不出另一种实现方式 coyoneda .有可能吗？

Answer 1

A型T同构于

forall r . (T -> r) -> r

根据米田同构。
在你的情况下，

forall b r. ((b -> a) -> f b -> r) -> r
~=  -- adding explicit parentheses
forall b . (forall r. ((b -> a) -> f b -> r) -> r)
~=  -- uncurrying
forall b . (forall r. ((b -> a, f b) -> r) -> r)
~=  -- Yoneda
forall b . (b -> a, f b)

这不是你想要的。要使用 coyoneda，您需要对存在类型进行建模:

exists b . (b -> a, f b)

所以，让我们把它变成 forall

exists b . (b -> a, f b)
~=  -- Yoneda
forall r . ((exists b . (b -> a, f b)) -> r) -> r
~=  -- exists on the left side of -> becomes a forall
forall r . (forall b . (b -> a, f b) -> r) -> r
~=  -- currying
forall r . (forall b . (b -> a) -> f b -> r) -> r

因此，这是您需要在 Coyoneda 中使用的正确编码。定义。