Sum/product of Church-encoded list of numbers does not type check

Question

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?

Upswell

Answer 1

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.

Evangelistic

Answer 2

You can isolate your types in newtype. This seems to work:

{-# 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

Papilionaceous