Is it possible to type `min` in a normalizing theory such as System-F or the Calculus of Constructions?

Question

This min definition below works on two church numbers and returns the least big. Each number becomes a continuation that sends its pred to the other, zig and zag, until zero is reached. Moreover, one of the numbers appends f to the result each time it is called, so, in the end, you'll have (\ f x -> f (... (f (f x)) ...)) where the number of 'f's on the right is the number of times the first continuation was called.

min a b f x = (a_continuator b_continuator)
    a_continuator = (a (\ pred cont -> (cont pred)) (\ cont -> x))
    b_continuator = (b (\ pred cont -> (f (cont pred))) (\ cont -> x))

It seems like min can't be typed on System-F. For example, in order to run it on GHC, I had to use unsafeCoerce twice:

import Unsafe.Coerce

(#)   = unsafeCoerce
min'  = (\ a b f x -> (a (\ p c -> (c # p)) (\ c -> x) (b (\ p c -> (f (c # p))) (\ c -> x))))
toInt = (\ n -> (n (+ 1) 0))
main  = print (toInt (min'
    (\ f x -> (f (f (f (f (f x))))))               -- 5
    (\ f x -> (f (f (f (f (f (f (f (f x))))))))))  -- 8
    :: Int)

Is it possible to type min on System-F (or the Calculus of Constructions)?

Answer 1

The function (is it well-known? it looks really clever) is typeable, it just doesn't work with Church-encoded nats.

Here is the type that GHC infers:

(((t3 -> t2) -> t3 -> t2) -> (b0 -> a0) -> t1 -> t0)
                        -> (((t6 -> t5) -> t6 -> t4) -> (b1 -> a0) -> t1)
                        -> (t5 -> t4)
                        -> a0
                        -> t0))

Here is the closest to the desired type I could get:

postulate t1 t2 : Set

A = ((t2 -> t1) -> t1) -> (((t2 -> t1) -> t1) -> t1) -> t1
B = (t2 -> t1) -> ((t2 -> t1) -> t1) -> t1
C = t1 -> t1

min : (A -> A) -> (B -> B) -> (C -> C)
min a b = \ f x -> a (\ p c -> c p) (\ c -> x) (b (\ p c -> f (c p)) (\ c -> x))

To work with Church-encoded nats min must accept two arguments of type (a -> a) -> a -> a, i.e. A must be of type a -> a, i.e.

a ~ (t2                 -> t1) -> t1
a ~ (((t2 -> t1) -> t1) -> t1) -> t1

i.e. t2 ~ (t2 -> t1) -> t1, which is a loop. There is no recursive types in System F or CoC and hence the term is not typeable as is.

However I ignored the Rank2Types stuff. Anyway,

newtype Church = Church { runChurch :: forall a. (a -> a) -> a -> a }

min' a b = Church $ \f x -> runChurch a (\p c -> c p) (\c -> x) (runChurch b (\p c -> f (c p)) (\c -> x))

is an infinite type error as well.