Following standard definitions of Church-encoded natural numbers and lists represented as right folds, I want to write a function that takes a list of numbers as its argument and returns sum of its elements:
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
This definition of sum does not type check - I assume it's because its type expands to
(forall a. (a -> a) -> a -> a) -> (forall a. (a -> a) -> a -> a) -> (forall a. (a -> a) -> a -> a)
whereas function definition demands rather
forall a. ((a -> a) -> a -> a) -> ((a -> a) -> a -> a) -> (a -> a) -> a -> a
and it does, in fact, type check:
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
Can I somehow avoid copying (a -> a) -> a -> a in all my definitions? Resulting types get very long very quickly... I could do
type Number a = (a -> a) -> a -> a
and place that in type annotations but perhaps I can do something smarter/tricker than that?
In versions of GHC with quick-look impredicativity (9.2 and newer), you can make your original sum function work just by enabling the ImpredicativeTypes extension.