4

在 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

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

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

当然这不是直接可能的。可能的一件事是正常定义自然数并定义and{data Nats = Zero | Succ Nats}之间的“转换” ，然后使用Haskell 内置的句法构造。NatNatscase

在无类型 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)。

但是，这不会在 Haskell 中进行类型检查。试图\(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吗？需要不同的技巧吗？

4

1 回答 1

5

我认为典型的技巧是使用数据类型（或者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)
于 2021-05-19T03:19:12.867 回答