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  -- 编译器推导的类型
    plus' a b f x = a f (b f x)
    zero _ x = x

我希望避免在所有定义中重复书写冗长的(a -> a) -> a -> a类型，除了定义type Number a = (a -> a) -> a -> a之外，有没有更巧妙的实现方法？

方法一：用newtype包装多态函数（最推荐） #

用newtype把丘奇数字的多态函数包起来，既能保留原有的语义，又能让类型系统顺利通过检查，还不用重复写冗长的类型：

{-# LANGUAGE RankNTypes #-}

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

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

zero :: Number
zero = Number $ \_ x -> x

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

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

这里Number变成了一个具体的新类型，折叠列表时plus的类型Number -> Number -> Number完全符合List Number的折叠函数要求，类型检查直接通过。需要使用数字的具体功能时，调用runNumber就能拿到底层的多态函数。

方法二：调整plus的多态性适配折叠需求 #

不用包装类型，而是修改plus的类型签名，让它能接受针对特定类型的丘奇数字，而非封闭的多态数字：

{-# LANGUAGE RankNTypes #-}

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

zero :: Number
zero _ x = x

-- 让plus适配任意特定类型a的数字运算
plus :: ((a->a)->a->a) -> ((a->a)->a->a) -> (a->a)->a->a
plus a b f x = a f (b f x)

sum :: List Number -> Number
sum xs = xs (\n acc -> plus n acc) zero

这里把plus改成了针对特定a的多态函数，传给列表折叠时，会自动实例化到合适的类型，避免了原版本中多态类型无法统一的问题。

方法三：用类型族统一命名 #

如果不想定义带参数的type，可以用类型族来统一指代(a->a)->a->a：

{-# LANGUAGE RankNTypes, TypeFamilies #-}

type family NumberF a where
  NumberF a = (a->a)->a->a

type Number = forall a. NumberF a

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

zero :: Number
zero _ x = x

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

sum :: List Number -> Number
sum xs = xs (\n acc -> plus n acc) zero

这种方式和定义type Number a = ...类似，但用类型族可以更灵活地扩展类型关联逻辑。

内容的提问来源于stack exchange，提问作者shooqie