遵循 Church 编码的自然数和表示为右折叠的列表的标准定义,我想编写一个函数,将数字列表作为其参数并返回其元素的总和:
type Number = forall a. (a -> a) -> a -> a
type List a = forall b. (a -> b -> b) -> b -> b
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
并将其放在类型注释中,但也许我可以做一些比这更聪明/更巧妙的事情?
您可以在
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
在具有快速查看必然性的 GHC 版本(9.2 及更高版本)中,您只需启用
sum
扩展即可使原始 ImpredicativeTypes
函数发挥作用。