haskell - Haskell 中原始递归函数的良好表示

Question

我在 answer to a previous question 中认为可以在 Haskell 中表示 primitive recursive functions (PRF) 和 ⊥ 或 undefined 的单个额外值的联合。这个论点是基于对原始递归函数的公理结构的直接翻译；它需要许多语言扩展和关于函数数量的类型级推理。是否可以用更惯用的 Haskell 来表示一组等效的原始递归函数？

理想情况下，PRF 的惯用表示应该能够满足以下所有条件:

提供 Category 实例

不需要处理关于函数数量的类型级推理

除了原始递归的要求

任何输入的 undefined 函数都是所有输入的 undefined。这将 PRF 集限制为单个不可避免的额外值 ⊥ 而不是包含多个部分递归函数。这意味着 while 循环或类似部分递归函数的任何定义都应该是 undefined 。

我注意到原始递归函数的公理类似于 Category 定律， Arrow 没有 arr(实际上它与 arr 相反)，以及仅适用于自然数的有限循环形式。

Answer 1

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}

我们还需要提供一个接口(interface)来构建 PRF s。 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)

seq s 要求 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 结合使用时，它们是描述 (&&&) 行为所需的唯一函数。

在我们为 ArrowLike 提供 PRF 实例之前，我们会说普通函数 (->) 是如何 ArrowLike

import qualified Prelude (fst, snd)

instance ArrowLike (->) where
    fst = Prelude.fst
    snd = Prelude.snd
    f &&& g = \b -> (f b, g b)

对于 PRF s，我们将使用我们在 (.) 定义中为 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 。用 zero 替换 const :: c -> a b c 很诱人；这将是一个致命的缺陷，因为有人可以通过 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，具有构造和解构元组和自然数的能力。

例子

使用此接口(interface)更容易定义原始递归函数，例如 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 声明，但所有以这种方式构建的 PRF 将是 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

我们可以评估根据 PRF 方便地定义的 match 。

run isOdd (S $ S $ S Z)

Compiling function
Running function
S Z

但是 infiniteLoop 定义的函数一般都是 undefined ，而不仅仅是奇数。

run infiniteLoop (Z)

Compiling function