是否可以在规范化理论中输入`min`,如System-F或Constructions？

Question

这min下面的定义适用于两个教堂数量和返回至少大.每个数字都成为一个延续,将其pred传递给另一个,zig和zag,直到达到零.此外,每次调用时,其中一个数字会将f附加到结果中,因此,最后,您将获得(\ f x -> f (... (f (f x)) ...))右边的'f'的数量是第一个连续调用的次数.

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))

似乎min无法在System-F上输入.例如,为了在GHC上运行它,我不得不使用unsafeCoerce两次:

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)

是否可以输入minSystem-F(或构造微积分)？

Answer 1

该函数（它是众所周知的吗？它看起来非常聪明）是可输入的，它只是不适用于 Church-encoded nats。

这是 GHC 推断的类型：

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

这是我能得到的最接近所需的类型：

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))

要使用 Church-encoded natsmin必须接受两个类型的参数(a -> a) -> a -> a，即A必须是类型a -> a，即

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

即t2 ~ (t2 -> t1) -> t1，这是一个循环。System F 或 CoC 中没有递归类型，因此该术语不能按原样输入。

然而我忽略了这些Rank2Types东西。反正，

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))

也是一个无限类型错误。