Church 编码的数字列表的和/积不进行类型检查

Question

遵循 Church 编码的自然数和表示为右折叠的列表的标准定义，我想编写一个函数，它将数字列表作为其参数并返回其元素的总和：

type Number = forall a. (a -> a) -> a -> a

type List a = forall b. (a -> b -> b) -> b -> b

zero :: Number
zero _ x = x

plus :: Number -> Number -> Number
plus a b f x = a f (b f x)

sum :: List Number -> Number
sum xs = xs plus zero

这个定义sum不进行类型检查 - 我认为这是因为它的类型扩展到

(forall a. (a -> a) -> a -> a) -> (forall a. (a -> a) -> a -> a) -> (forall a. (a -> a) -> a -> a)

而函数定义则要求

forall a. ((a -> a) -> a -> a) -> ((a -> a) -> a -> a) -> (a -> a) -> a -> a

事实上，它确实进行了类型检查：

sum :: List ((a -> a) -> a -> a) -> (a -> a) -> a -> a  -- OK
sum xs = xs plus' zero
  where
    plus' :: (t1 -> t -> t3) -> (t1 -> t2 -> t) -> t1 -> t2 -> t3  -- inferred by compiler
    plus' a b f x = a f (b f x)
    zero _ x = x

我可以以某种方式避免复制(a -> a) -> a -> a我的所有定义吗？结果类型很快就会变得很长......我可以做

type Number a = (a -> a) -> a -> a

并将其放在类型注释中，但也许我可以做一些比这更聪明/更狡猾的事情？

Answer 1

您可以在 中隔离您的类型newtype。这似乎有效：

{-# LANGUAGE RankNTypes #-}

newtype Number = Number {num :: forall a. (a -> a) -> a -> a}

newtype List a = List {lst :: forall b. (a -> b -> b) -> b -> b}

plus :: Number -> Number -> Number
plus a b = Number (\f x -> (num a) f ((num b) f x))

zero :: Number
zero = Number (\_ x -> x)

sum :: List Number -> Number
sum xs = (lst xs) plus zero

Answer 2

在具有快速查看必然性的 GHC 版本（9.2 及更高版本）中，您sum只需启用ImpredicativeTypes扩展即可使原始函数正常工作。