是否可以在规范化理论中键入‘the’，如System-F或the Calculus of Constructions？

Question

下面的min定义适用于两个教堂编号，并返回最小的big。每个数字都成为一个连续数，将它的pred发送给另一个，zig和zag，直到到达零。此外，其中一个数字在每次调用时都会将f附加到结果中，因此，最后，您将得到(\ f x -> f (... (f (f x)) ...))，其中右侧的'f's的数量是第一个continuation被调用的次数。

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

似乎不能在System-F上键入min。例如，为了在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)

是否可以在System-F (或构造演算)上键入min？

Answer 1

这个函数(它是众所周知的吗？它看起来真的很聪明)是可打字的，它只是不能与教堂编码的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))

要使用教会编码的nats，min必须接受两个(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))

也是一个无限类型错误。