如何解决使用 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)
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。