用RankNTypes编码的System自然数的"case“运算符不能打印

Question

在Haskell中，如果启用了RankNTypes扩展

{-# Language RankNTypes           #-}

然后我们就可以定义自然数，因为它们是在System中编码的：

type Nat = forall a. a -> ((a -> a) -> a)

zero :: Nat 
zero = \z s -> z 

succ :: Nat -> Nat
succ n = \z s -> s (n z s)

fold :: a -> (a -> a) -> Nat -> a
fold z s n = n z s

耶！下一步是定义案例操作:其思想是

caseN :: Nat -> a -> (Nat -> a) -> a 
caseN n z f = "case n of 
    zero -> z 
    succ m -> f m"

当然，这是不可能的。一件可能的事情是将自然数定义为通常的{data Nats = Zero | Succ Nats}，并定义Nat和Nats之间的“转换”，然后使用内置到Haskell的语法case构造。

在非类型化的lambda演算中，caseN可以编写为

caseN n b f = snd (fold (zero, b) (\(n0, _) -> (succ n0, f n0)) n)

遵循Kleene显然发现的用于定义前驱者函数的技巧。这个版本的caseN看起来确实应该使用上面给出的类型来进行类型检查。(zero, b) :: (Nat, b)和\(n0, _) -> (succ n0, f n0) :: (Nat, b) -> (Nat, b)，所以fold (zero, b) (\(n0, _) -> (succ n0, f n0)) n :: (Nat, b)。

然而，这并不是哈斯克尔的打字机。试图将内部函数\(n0, _) -> (succ n0, f n0)与

succf :: (Nat -> b) -> (Nat, b) -> (Nat, b)
succf f (n, _y) = (succ n, f n)

显示可能需要ImpredicativeTypes扩展，因为succf似乎需要该扩展。对于更典型的{data Nats = Zero | Succ Nats}，caseN构造可以工作(在更改为适当的fold和Zero、Succ之后)。

能让caseN直接在Nat上工作吗？需要另一种诡计吗？

Answer 1

我认为典型的技巧是使用数据类型(或newtype，如注释所指出的)包装器。首先，您可以将Nat定义为类型同义词，而不是将其定义为：

newtype Nat = Nat { unNat :: forall a. a -> ((a -> a) -> a) }

这与您的定义是同构的，只是您必须显式地包装和展开内容。

我们可以继续编写与您定义相同的定义：

zero :: Nat
zero = Nat $ \z s -> z
succ :: Nat -> Nat
succ (Nat n) = Nat $ \z s -> s (n z s)
fold :: a -> (a -> a) -> Nat -> a
fold z s (Nat n) = n z s

这基本上是您已经拥有的，但是现在使用Nat (作为构造函数和模式)进行显式包装和展开。

在这一点上，您的最终定义只起作用：

caseN :: Nat -> b -> (Nat -> b) -> b
caseN n b f = snd (fold (zero,b) (\(n0,_) ->  (succ n0,f n0)) n)

succf :: (Nat -> b) -> (Nat, b) -> (Nat, b)
succf f (n,_y) = (succ n, f n)