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

Question

假设我们有一个单子,通过定义return,(>>=)以及一套法律.有一种数据类型

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

也称为密度.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表示？
• 这种表现形式是独一无二的(我猜不是)？
• 如果它不是唯一的,那么总是最"简单"(?例如,在数量上:) :)一个？

Answer 1

没有这样的编码是唯一的

当你提出问题答案显然是"不"

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

至于哪个编码是最小的......那么基础类型几乎可以肯定!

密码可能不是您想要的

最重要的是,虽然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使用一元操作,你叫什么to,然后调用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函数,这是大约70年前Church发现的一个属性.我们经常谈论"教会编码"数据结构,尽管Oleg建议相反,至少在打字环境中,我们应该谈论"Boehm-Beraducci"编码.无论你怎么称呼它,这个想法都是

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

至少可以快速而宽松的推理.很明显,这种编码提供了一种将任何 ADT 编码为系统F类型的方法.这也揭示了一种实现函数式语言的方法:将所有内容视为封闭式内容,并将模式匹配仅作为函数应用程序实现.

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

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

结果证明这是一个非常重要的身份.除此之外,这有助于我们思考更高等级类型的类型推断与存在类型之间的关系.由于类型推断可以判定为2级类型,因此类型推断在具有等级1通用和存在性的系统中也是可判定的.由于存在量化是模块的基础,因此这是重要的事情.