继续传递类​​型的样式表示

Question

假设我们有一个单子，由return、(>>=) 和一组定律定义。有数据类型

newtype C m a = C { unC ∷ forall r. (a → m r) → m r }

也称为Codensity。 C m a ≅ m a 假设 m 是 Monad，即我们可以编写两个函数 to ∷ Monad m ⇒ m a → C m a 和 from ∷ Monad m ⇒ C m a → m a

to ∷ Monad m ⇒ m a → C m a
to t = C $ \f → t >>= f

from ∷ Monad m ⇒ C m a → m a
from = ($ return) . unC

并通过等式推理证明to ∘ from ≡ id 和from ∘ to ≡ id，例如：

from . to =                                  -- by definition of `(.)'
  \x → from (to x) =                         -- by definition of `to'
  \x → from (C $ \f → x >>= f) =             -- by definition of `from'
  \x → ($ return) (unC (C $ \f → x >>= f)) = -- unC . C ≡ id
  \x → ($ return) (\f → x >>= f) =           -- β-reduce
  \x → x >>= return =                        -- right identity law
  \x → x =                                   -- by definition of `id'
  id

到目前为止一切顺利。 我的问题是

• 给定一个类型和一堆定律，我们如何构造对应的同构 CPS 表示？
• 这种表示是唯一的吗（我猜不是）？
• 如果它不是唯一的，是否总是有最“简单”的（例如→s 的数量：））？

Answer 1

没有这样的编码是唯一的

当你提出这个问题时，答案显然是“不”

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

至于哪种编码最小……嗯，基本类型几乎可以肯定！

Codensity 可能不是你想要的

更重要的是，虽然 Codensity 很吸引人，但我不认为它与底层类型同构。 from . to = id 是简单的方向。

to . from
  = \x -> to (from x)
  = \x -> C $ \f -> (from x) >>= f
  = \x -> C $ \f -> (unC x return) >>= f
  = \(C g) -> C $ \f -> (g return) >>= f

但是你有点卡住了。当您尝试证明a = forall r. (a -> r) -> r 但您被“免费定理”拯救时，也会发生同样的事情（可能有一种方法可以做到这一点，但免费定理很容易）。我不知道 Codensity 没有相应的论据，我读过的大多数论文都证明它保留了 >>= 和 return，也就是说，如果你只使用单子操作和你所说的 @ 构造你的 C m a 987654328@ 那么对to . from 的调用就是身份。

如果我们足够努力，我们甚至可以想出同构的反例

evil :: C Maybe Int
evil = C $ \h -> case h 1 of
                      Nothing -> h 2
                      Just x  -> Nothing


 to . from $ evil
  = (\(C g) -> C $ \f -> (g return) >>= f) evil
  = C $ \f -> ((\h -> case h 1 of
                      Nothing -> h 2
                      Just x  -> Nothing) return) >>= f
  = C $ \f -> Nothing >>= f

这些都是一样的吗？

test 1 = Nothing
test n = Just n

unC evil test
  = Just 2
unC (C $ \f -> Nothing >>= f) test
  = Nothing >>= test
  = Nothing

我可能在推导中犯了一个错误。我还没有真正检查过，但我只想说现在我不认为C m a = m a

另一种 CPS

所有数据都可以编码为无类型的 lambda 函数，这是 Church 大约 70 年前发现的一个属性。我们经常谈论“Church encoding”数据结构，尽管 Oleg 建议至少在类型化设置中，我们应该谈论“Boehm-Beraducci”编码。不管你怎么称呼它，这个想法是

(a,b) = forall r. (a -> b -> r) -> r
Either a b = forall r. (a -> r) -> (b -> r) -> r

至少达到快速和松散的推理。很明显，这种编码提供了一种将 any ADT 编码为 System F 类型的方法。这也揭示了一种实现函数式语言的方式：将所有事物都视为底层的闭包，并将模式匹配作为函数应用程序来实现。

实际上，System F 甚至有一种将存在类型编码为通用类型的方法

exists a. f a = forall r. (forall a'. f a' -> r) -> r

事实证明这是一个非常重要的身份。除其他外，这有助于我们思考更高等级类型和存在类型的类型推断之间的关系。由于类型推断最多可判定为等级 2 类型，因此类型推断在具有等级 1 普遍性和存在性的系统中也是可判定的。因为存在量化是模块的基础，所以这是很重要的东西。