使用 RankNTypes 编码的 System-F 自然数的“case”运算符无法进行类型检查

问题描述

在 Haskell 中，如果启用 RankNTypes 扩展

{-# Language RankNTypes           #-}

然后可以定义在 System-F 中编码的自然数：

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

耶！下一步是定义case操作：想法是

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 之间的“转换”，然后使用内置的句法 case到 Haskell。

在无类型的 lambda 演算中，caseN 可以写成

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

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

然而，这不会在 Haskell 中进行类型检查。试图用

隔离内部函数\(n0,f n0)

succf :: (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 上工作？需要不同的技巧吗？

解决方法

我认为典型的技巧是使用数据类型（或 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)