能否在不破坏等式推理的情况下使用 Church 编码？

Question

请注意这个程序：

{-# LANGUAGE RankNTypes #-}

import Prelude hiding (sum)

type List h = forall t . (h -> t -> t) -> t -> t

sum_ :: (Num a) => List a -> a
sum_ = \ list -> list (+) 0

toList :: [a] -> List a
toList = \ list cons nil -> foldr cons nil list

sum :: (Num a) => [a] -> a
-- sum = sum_ . toList        -- does not work
sum = \ a -> sum_ (toList a)  -- works

main = print (sum [1,2,3])

两种 sum 的定义在方程推理上是相同的。然而，编译第二个定义可行，但第一个定义不行，会出现以下错误：

tmpdel.hs:17:14:
    Couldn't match type ‘(a -> t0 -> t0) -> t0 -> t0’
                  with ‘forall t. (a -> t -> t) -> t -> t’
    Expected type: [a] -> List a
      Actual type: [a] -> (a -> t0 -> t0) -> t0 -> t0
    Relevant bindings include sum :: [a] -> a (bound at tmpdel.hs:17:1)
    In the second argument of ‘(.)’, namely ‘toList’
    In the expression: sum_ . toList

看起来 RankNTypes 会破坏等式推理。在 Haskell 中有没有不破坏它的情况下使用 church 编码列表的方法？

- MaiaVictor

---

是的，但这将涉及对编译器进行黑客攻击... 排名2类型推断是可决定的，但尚无人实现它。排名3类型推断是不可判定的（因此存在Rank2Types和RankNTypes，即使它们目前执行相同的操作）。 - Daniel Wagner

我很难理解你在这里所说的“等式推理”的意思。你正在使用一个同构，它显然不是通常的相等关系。 - dfeuer

没关系，我也不知道。 - MaiaVictor

@Viclib 记住，专注于箭头左侧是可以的。所以我猜测 head :: List (Maybe a) a -> Maybe a; head f = f Just Nothing 或者 unsafeHead :: List a a -> a; unsafeHead f = f id undefined。 - Daniel Wagner

请注意，[a] -> List a 是 GHC 中实际上不存在的类型（参见https://dev59.com/oo3da4cB1Zd3GeqPzGX6#31629197），这使得 sum_ . toList 的类型不正确。 - András Kovács

Answer 1

我有这样的印象，ghc会尽可能地将所有的for-all标记向左移动：

forall a t. [a] -> (a -> t -> t) -> t -> t)

并且

forall a. [a] -> forall t . (h -> t -> t) -> t -> t

可以互换使用，如下所示：

toList' :: forall a t. [a] -> (a -> t -> t) -> t -> t
toList' = toList

toList :: [a] -> List a
toList = toList'

这可能解释了为什么无法检查sum的类型。您可以通过将多态定义打包到newtype包装器中来避免此类问题，以避免出现这种hoisting（该段落在新版本的文档中不再出现，因此我之前使用了条件语句）。

{-# LANGUAGE RankNTypes #-}
import Prelude hiding (sum)

newtype List h = List { runList :: forall t . (h -> t -> t) -> t -> t }

sum_ :: (Num a) => List a -> a
sum_ xs = runList xs (+) 0

toList :: [a] -> List a
toList xs = List $ \ c n -> foldr c n xs

sum :: (Num a) => [a] -> a
sum = sum_ . toList

main = print (sum [1,2,3])

- gallais

---

确实应该这样定义“List”。 GHC 对于 rank-n 类型的处理比较次等，如果不使用 newtype 封装，会有问题。 - augustss

很棒的答案，我希望你的被采纳而不是我的。 =D - Daniel Wagner

还应该注意到newtypes不会增加任何开销。 - PyRulez

Answer 2

这里有一个有些令人不安的技巧，你可以尝试一下。在你需要一个rank-2类型变量的地方，使用空类型代替；在你需要选择类型变量的实例化时，使用unsafeCoerce。使用空类型可以确保（尽可能地）不执行任何可以观察到不应该被观察到的值的操作。因此：

import Data.Void
import Unsafe.Coerce

type List a = (a -> Void -> Void) -> Void -> Void

toList :: [a] -> List a
toList xs = \cons nil -> foldr cons nil xs

sum_ :: Num a => List a -> a
sum_ xs = unsafeCoerce xs (+) 0

main :: IO ()
main = print (sum_ . toList $ [1,2,3])

您可能想编写一个稍微更安全的 unsafeCoerce 版本，例如：

instantiate :: List a -> (a -> r -> r) -> r -> r
instantiate = unsafeCoerce

然后 sum_ xs = instantiate xs (+) 0 可以作为一种替代定义，这样你就不会把你的List a变成真正的任意类型。

- Daniel Wagner

---

那又怎样呢...我想我会放下恐惧，开始在我的词汇表中采用unsafeCoerce。您正在创造一个怪物，先生。 - MaiaVictor

不知道，不是那个。有时候治疗比疾病更加严重。我并没有真正看到需要解决的问题。 - dfeuer

这并不是真正有建设性的，但我喜欢dfeuer的反应，毫不意外呵。 - MaiaVictor

太可怕了。一般来说，对于unsafeCoerce没有任何保证。除了在特定实现的模块之外的任何使用都应该受到最严厉的惩罚。 - augustss

经过类型检查后，我的理想编译器会在终止检查成功时将 f :: T -> Void 优化为大致的 \_ -> undefined，并将 g :: T -> () 优化为 \_ -> ()（对于其他单值类型，例如 a:~:b，也是类似的）。由于 GHC（目前）还没有那么智能，所以我猜 unsafeCoerce 应该可以运行。不过，这看起来非常危险。 - chi

Answer 3

一般来说，等式推理只在Haskell代表的“基础System F”中成立。在这种情况下，正如其他人所指出的，你会因为Haskell将forall向左移动并在各个点上自动应用正确的类型而受阻。你可以通过使用newtype包装器提供类型应用发生的线索来解决这个问题。正如你所看到的，你也可以通过eta扩展来操作类型应用的时间，因为Hindley-Milner的类型规则对于let和lambda是不同的：forall通常是通过“泛化”规则在let（和其他等效的命名绑定）中引入的。

- J. Abrahamson