14

注意这个程序：

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

4

3 回答 3

13

我的印象是 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无法检查 's 类型。您可以通过将多态定义打包在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])
于 2015-08-11T12:56:56.600 回答
9

这是一个你可以尝试的有点可怕的技巧。到处都有 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变成真正任意的东西的风险。

于 2015-08-11T01:30:25.533 回答
6

通常，等式推理仅适用于 Haskell 所代表的“底层系统 F”。在这种情况下，正如其他人所指出的那样，您会被绊倒，因为 Haskellforall向左移动并自动在各个点应用正确的类型。您可以通过newtype包装器提供关于类型应用程序应在何处发生的提示来修复它。正如您所见，当类型应用发生时，您还可以通过 eta 扩展进行操作，因为 Hindley-Milner 类型规则let对于 lambda 和对于 lambda 是不同的：foralls 是通过“泛化”规则引入的，默认情况下，在lets （和其他等效的命名绑定）单独。

于 2015-08-11T15:53:29.937 回答