是否可以在不破坏等式推理的情况下使用教会编码？

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])

总和的两个定义都是相同的,直到等式推理.然而,编译第二个作品的定义,但第一个定义没有,这个错误:

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中有教会编码的列表而不破坏它？

Answer 1

我的印象是ghc尽可能地渗透所有人:

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的包装,以避免这样的提升(因此我有条件较早使用的那款没有出现在文档的更新版本).

{-# 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])

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变成任意的任意东西.

Answer 3

通常,等式推理仅存在于Haskell所代表的"基础系统F"中.在这种情况下,正如其他人所指出的那样,你会被绊倒,因为Haskell forall向左移动并自动在不同的点上应用适当的类型.您可以通过提供有关应用程序应该通过newtype包装器发生的位置的提示来修复它.正如你所见,你也可以通过eta扩展来操作类型应用程序,因为Hindley-Milner的输入规则是不同的let并且对于lambda:foralls是通过"泛化"规则引入的,默认情况下是lets(和其他等价物)单独命名绑定.