关于嵌套的 CPS 悬挂类型

Question

让我们从熟悉的 CPS 暂停计算类型开始，(a -> r) -> r，在 mtl-speak 中拼写为 Cont r a。我们知道。如果我们嵌套这个类型，我们得到这个 rank-3 类型：

forall r. ((forall s. (a -> s) -> s) -> r) -> r

（为了方便起见，我可能已经定义了 type Susp a = forall r. (a -> r) -> r，然后开始谈论 Susp (Susp a)，但我担心这会导致分散注意力。）

我们可以通过仅在嵌套之后对结果类型进行通用量化来获得相似的类型，就像我们有 forall r. Cont r (Cont r a):

forall r. (((a -> r) -> r) -> r) -> r

这两种类型之间有什么有意义的区别吗？我说有意义是因为有些事情显然只能用第一个 "SuspSusp" 类型来完成...

GHCi> foo = (\kk -> kk (\k -> k True)) :: forall s. ((forall r. (Bool -> r) -> r) -> s) -> s
GHCi> bar = (\kk -> kk (\k -> k True)) :: forall r. (((Bool -> r) -> r) -> r) -> r
GHCi> foo (\m -> show (m not))
"False"
GHCi> bar (\m -> show (m not))

<interactive>:76:12: error:
    * Couldn't match type `[Char]' with `Bool'
      Expected type: Bool
        Actual type: String
    * In the expression: show (m not)
      In the first argument of `bar', namely `(\ m -> show (m not))'
      In the expression: bar (\ m -> show (m not))

... 也可以通过第二个 "ContCont" 实现，方法是利用 (a -> r) -> r 的自由定理，f (m g) = m (f . g) 对任何 m :: (a -> r) -> r 的自由定理。

GHCi> foo (\m -> m (show . not))
"False"
GHCi> bar (\m -> m (show . not))
"False"

Answer 1

（部分答案）

如果 a 与您建议的类型同构，我不会感到惊讶

forall r. (((a -> r) -> r) -> r) -> r

到目前为止，我只能证明前者嵌入了后者。嵌入也可能是同构，但如果成立，要证明我们可能需要在上面的可怕类型上利用参数化。

这是嵌入：

type YD a = forall r. (((a -> r) -> r) -> r) -> r

ydosi :: a -> YD a
ydosi x = \f -> f (\g -> g x)

ydiso :: YD a -> a
ydiso x = x (\a -> a id)

证明这是一个嵌入很容易，只需要测试步骤：

ydiso (ydosi x)
= ydiso (\f -> f (\g -> g x))
= (\f -> f (\g -> g x)) (\a -> a id)
= (\a -> a id) (\g -> g x)
= (\g -> g x) id
= id x
= x

相反的方向更难，并且（如果可能的话）应该依赖x :: YD a的参数化。完成这将证明想要的同构。

ydosi (ydiso x)
= ydosi (x (\a -> a id))
= \f -> f (\g -> g (x (\a -> a id)))
= ????
= x

Answer 2

我对以下对此事的看法并不完全有信心（感觉好得令人难以置信），但这是迄今为止我所能提供的最好的，所以让我们把它放在 table.

通过提出 a 和 forall r. (((a -> r) -> r) -> r) -> r 之间的同构候选来解决这个问题：

-- If you want to play with these in actual code, make YD a newtype.
type YD a = forall r. (((a -> r) -> r) -> r) -> r

ydosi :: a -> YD a
ydosi x = \kk -> kk (\k -> k x)

ydiso :: YD a -> a
ydiso mm = mm (\m -> m id)

chi然后证明ydiso . ydosi = id，这就剩下ydosi . ydiso方向需要处理了。

现在，如果我们有一些 f 及其左逆 g (g . f = id)，它很容易得出 f . g . f = f。如果 f 是满射，我们可以 "cancel" 它在右边，导致我们 f . g = id （即同构的另一个方向）。既然如此，假设我们有 ydiso . ydosi = id，确定 ydosi 是满射就足以证明同构。一种调查方法是推理 YD a.

的居民

（虽然我不会在这里尝试这样做，但我认为可以根据 System F 打字规则来表达以下段落，从而使它们更加精确 -- cf. this Math.SE question。）

一个 YD A 值是一个延续的函数：

mm :: forall r. (((A -> r) -> r) -> r) -> r
mm = \kk -> _y
-- kk :: forall r. ((A -> r) -> r) -> r
-- _y :: r

这里获得类型 r 的结果的唯一方法是将 kk 应用于某物：

mm :: forall r. (((A -> r) -> r) -> r) -> r
mm = \kk -> kk _m
-- kk :: forall r. ((A -> r) -> r) -> r
-- _m :: forall r. (A -> r) -> r

由于 kk 的类型在 r 中是多态的，因此 _m 的类型也必须是多态的。这意味着我们也知道 _m 必须是什么样子，多亏了熟悉的 A/forall r. (A -> r) -> r 同构：

mm :: forall r. (((A -> r) -> r) -> r) -> r
mm = \kk -> kk (\k -> k _x)
-- kk :: forall r. ((A -> r) -> r) -> r
-- k :: forall r. (A -> r) -> r
-- _x :: A

然而，上面的右侧恰好是 ydosi:

mm :: forall r. (((A -> r) -> r) -> r) -> r
mm = ydosi _x
-- _x :: A

我们刚刚发现，对于某些 x :: A，任何 forall r. (((A -> r) -> r) -> r) -> r 值都是 ydosi x。紧接着ydosi是满射，足以证明同构

由于 a 同构于 forall r. ((forall s. (a -> s) -> s) -> r) -> r（参见）和 forall r. (((a -> r) -> r) -> r) -> r，传递性意味着两种嵌套悬挂类型都是同构的。

嵌套悬浮同构的见证者长什么样？如果我们定义...

-- The familiar isomorphism.
type Susp a = forall r. (a -> r) -> r

suosi :: a -> Susp a
suosi x = \k -> k x

suiso :: Susp a -> a
suiso m = m id

...我们可以写...

ydosi . suiso . suiso :: Susp (Susp a) -> YD a
suosi . suosi . ydiso :: YD a -> Susp (Susp a)

... 归结为：

-- A few type annotations would be necessary to persuade GHC about the types here.
\mm -> \kk -> kk (\k -> k (mm id id)) -- Susp (Susp a) -> YD a
\mm -> \kk -> kk (\k -> k (mm (\m -> m id))) -- YD a -> Susp (Susp a)

我们可以在第一个见证人的 mm 上应用 Susp a 自由定理...

f (mm g) = mm (f . g) -- Free theorem
f (mm id) = mm f

mm id id
($ id) (mm id)
mm ($ id)
mm (\m -> m id)

...等等：

\mm -> \kk -> kk (\k -> k (mm (\m -> m id))) -- Susp (Susp a) -> YD a
\mm -> \kk -> kk (\k -> k (mm (\m -> m id))) -- YD a -> Susp (Susp a)

令人着迷的是，证人 "the same" 除了他们的类型。我想知道是否有一些从这个观察开始的论证可以让我们倒退并以更直接的方式证明同构。

关于嵌套的 CPS 悬挂类型

On nested CPS suspension types

haskell

types

polymorphism

continuation-passing

higher-rank-types