嵌套CPS悬挂类型研究

Question

让我们从熟悉的CPS挂起计算开始，(a -> r) -> r，在mtl中拼写为Cont r a。我们知道r。如果我们嵌套这种类型，就会得到这个级别-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“1来实现，利用(a -> r) -> r的自由定理，任何m :: (a -> r) -> r的f (m g) = m (f . g)。

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

Answer 1

我对下面这件事的看法并不完全有信心(这感觉太好了，不太真实)，但这是迄今为止我所能提供的最好的，所以让我们把它摆在桌面上吧。

chi's answer通过在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是满射的，我们可以在右边“取消”它，将我们引向f . g = id (即同构的另一个方向)。既然如此，既然我们有ydiso . ydosi = id，建立ydosi是满射的就足以证明同构。对此进行调查的一种方法是对YD a居民进行推理。

(虽然我不会在这里尝试这样做，但我认为通过使用System类型规则-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

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

由于a与forall r. ((forall s. (a -> s) -> s) -> r) -> r (cf )同构。( Twan van Laarhoven's comment)和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)

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

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)

令人着迷的是，除了他们的类型之外，证人是“相同的”。我想知道，从这个观察开始的论点，是否能让我们倒退，以更直接的方式证明同构。

Answer 2

(部分答覆)

如果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