如何在 CPS 中构造更高级别的 Coyoneda 类型的值？

Posted 2023-05-08

【中文标题】如何在 CPS 中构造更高级别的 Coyoneda 类型的值？

【英文标题】：How to construct values of a higher-rank Coyoneda type in CPS?

【发布时间】：2021-10-12 09:53:49

【问题描述】：

-# 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。有可能吗？

【参考方案1】：

类型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，您需要对 existential 类型进行建模：

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 定义中使用的正确编码。

【讨论】：

感谢您的编辑，现在很有意义。

【参考方案2】：

newtype 不太正确。以下作品：

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


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

【讨论】：

我自己在阅读HaskellWiki时发现了这一点