Haskell 中有一个非常直接的原始递归函数表示。这是一个newtype,我们将断言它是一个构造正确的原始递归函数。我们不导出构造函数以防止构造可能部分递归的任意函数。这种技术称为smart constructor。
module Data.PRF (
-- We don't export the PRF constructor
PRF (runPRF),
) where
newtype PRF b c = PRF {runPRF :: b -> c}
我们还需要提供一个接口来构建PRFs。 Category 实例将提供 PRF 所需的扩展组合的组合部分。
import Prelude hiding (id, (.), fst, snd, succ)
import Control.Category
instance Category PRF where
id = PRF id
PRF f . PRF g = PRF $ f `seq` g `seq` (f . g)
seqs 要求 f 和 g 在计算任何结果之前处于弱头范式;如果任一函数是undefined,那么组合也将是undefined。
原始递归函数也需要投影以从多个参数中选择一个参数。我们将其视为从数据结构中选择一个数据。如果我们使用元组而不是已知长度的列表,则投影函数变为fst 和snd。连同Arrow 的(&&&) 之类的东西来构建元组,我们可以满足扩展投影的所有要求。 PRF 就像“没有arr 的箭头”; arr 将允许将任意部分递归函数制成PRFs。我们将定义 ArrowLike 类别的类。
class Category a => ArrowLike a where
fst :: a (b, d) b
snd :: a (d, b) b
(&&&) :: a b c -> a b c' -> a b (c,c')
first :: a b c -> a (b, d) (c, d)
first = (*** id)
second :: a b c -> a (d,b) (d,c)
second = (id ***)
(***) :: a b c -> a b' c' -> a (b,b') (c,c')
f *** g = (f . fst) &&& (g . snd)
投影函数fst 和snd 代替了arr。当与扇出(&&&) 结合使用时,它们是描述ArrowLike 行为所需的唯一函数。
在我们为PRF 提供ArrowLike 实例之前,我们将说明(->) 的普通函数与ArrowLike 的区别
import qualified Prelude (fst, snd)
instance ArrowLike (->) where
fst = Prelude.fst
snd = Prelude.snd
f &&& g = \b -> (f b, g b)
对于PRFs,我们将使用我们在(.) 的定义中为Category 实例使用的相同归纳步骤,并要求这两个函数都是弱头范式。
instance ArrowLike PRF where
fst = PRF fst
snd = PRF snd
PRF f &&& PRF g = PRF $ f `seq` g `seq` (f &&& g)
最后,我们将提供原始递归本身。我们将使用元组直接从公理化定义中转换原始递归,而不是增加函数数量。
class ArrowLike a => PrimRec a where
zero :: a b Nat
succ :: a Nat Nat
prec :: a e c -> a (c, (Nat,e)) c -> a (Nat, e) c
Nat 是data Nat = Z | S Nat 给出的自然数。我选择将常量函数zero 和后继函数视为原始递归的一部分,唯一可以解构或检查它们构造的Nat 值的方法是使用prec。用const :: c -> a b c 替换zero 很诱人;这将是一个致命的缺陷,因为有人可以将infinity = S infinity 与const 一起引入,从而将prec 变成无限循环。
部分递归函数(->) 支持原始递归。
instance PrimRec (->) where
zero = const Z
succ = S
prec f g = go
where
go (Z, d) = f d
go (S n, d) = g (go (n, d), (n, d))
我们将使用与 (.) 和 (&&&) 相同的归纳技巧为 PRF 定义原始递归。
instance PrimRec PRF where
zero = PRF zero
succ = PRF succ
prec (PRF f) (PRF g) = PRF $ f `seq` g `seq` prec f g
原始递归函数是Category,具有构造和解构元组和自然数的能力。
示例
像add这样的原始递归函数更容易用这个接口定义。
import Prelude hiding (id, (.), fst, snd, succ)
import Control.Category
import Data.PRF
add :: PrimRec a => a (Nat, Nat) Nat
add = prec id (succ . fst)
我们仍然可以定义有用的函数,例如 match,它有助于构建原始递归函数,该函数根据自然值是否为零进行分支。
match :: PrimRec a => a b c -> a (Nat, b) c -> a (Nat, b) c
match fz fs = prec fz (fs . snd)
使用match,我们可以轻松快速地测试一个值是否为Z,并最终测试它是否为奇数
one :: PrimRec a => a b Nat
one = succ . zero
nonZero :: PrimRec a => a Nat Nat
nonZero = match zero one . (id &&& id)
isZero :: PrimRec a => a Nat Nat
isZero = match one zero . (id &&& id)
isOdd :: PrimRec a => a Nat Nat
isOdd = prec zero (isZero . fst) . (id &&& id)
我们仍然可以编写通常是递归的 Haskell 声明,但是以这种方式构建的所有 PRFs 都将是 undefined。
while :: PrimRec a => a s Nat -> a s s -> a s s
while test step = goTest
where
goTest = goMatch . (test &&& id)
goMatch = match id (goStep . snd)
goStep = goTest . step
这个函数,infiniteLoop,只会在奇数输入时无法终止。
infiniteLoop :: PrimRec a => a Nat Nat
infiniteLoop = while isOdd (succ . succ)
在运行我们的示例时,我们会注意评估顺序,例如 previous answer。
import System.IO
mseq :: Monad m => a -> m a
mseq a = a `seq` return a
run :: Show b => PRF a b -> a -> IO ()
run f i =
do
putStrLn "Compiling function"
hFlush stdout
f' <- mseq $ runPRF f
putStrLn "Running function"
hFlush stdout
n <- mseq $ f' i
print n
我们可以评估用match 方便地定义的PRFs。
run isOdd (S $ S $ S Z)
Compiling function
Running function
S Z
但infiniteLoop定义的函数一般是undefined,不只是奇数值。
run infiniteLoop (Z)
Compiling function