表示原始递归函数的指称语义

Question

有没有办法在 Haskell 中表示原始递归函数 (PRF) 的指称语义？

Answer 1

有点像。我们可以使用 Haskell 类或 GADT 对原始递归函数进行编码。然后我们可以认为原始递归函数是数据类型的等价类。最简单的等价是关于 PRF 解释的 Haskell 指称语义。由于 Haskell 的指称语义，这种表示最终将是不精确的，但让我们探索一下我们能做到多近。

原始递归函数

我们将使用definition of primitive recursive functions from Wikipedia。 PRF a 是一个原始递归函数，其元数为 a，其中 a 是自然数。

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}

data PRF (a :: Nat) where
    Const ::                             PRF 'Z
    Succ  ::                             PRF ('S 'Z)
    Proj  :: BNat n                   -> PRF n
    Comp  :: PRF k  -> List k (PRF m) -> PRF m
    PRec  :: PRF k  -> PRF (S (S k))  -> PRF (S k)

Const 构造常量函数或零参数，它总是返回 0。Succ 是参数一的后继函数。 Proj 构造投影函数系列，每个投影函数在跳过提供的参数数量后选择其中一个参数。 Comp 由提供其参数的其他函数列表组成一个函数。 PRec 在第一个参数上构建一个模式匹配的函数。 PRec 如果第一个参数为零，则将第一个函数应用于其余参数。如果第一个参数不为零，则它将第一个参数的前任作为第一个参数递归到自身，并返回应用于第一个参数的前任的第二个函数的结果、递归的结果和剩余的参数.这在从 PRF 到 Haskell 函数的编译器定义中更容易看出。

compile :: PRF n -> List n Nat -> Nat
compile Const = const Z
compile Succ  = \(Cons n Nil) -> S n
compile (Proj n) = go n
    where
        go :: BNat n -> List n a -> a
        go BZero     (Cons h _) = h
        go (BSucc n) (Cons _ t) = go n t
compile (Comp f gs) = \ns -> f' . fmap ($ ns) $ gs'
    where
        gs' = fmap compile gs
        f'  = compile f
compile (PRec f g) = h
    where
        h (Cons Z t)     = f' t
        h (Cons (S n) t) = g' (Cons n (Cons (h (Cons n t)) t))
        f' = compile f
        g' = compile g

以上要求定义自然数Nat、以类型级自然数为界的自然数BNat，以及类型级已知长度的列表List。

import qualified Data.Foldable as Foldable
import System.IO

data Nat = Z | S Nat
    deriving (Eq, Show, Read, Ord)

data List (n :: Nat) a where
    Nil   ::                  List 'Z     a
    Cons  :: a -> List n a -> List ('S n) a

instance Functor (List n) where
    fmap f Nil        = Nil
    fmap f (Cons h t) = Cons (f h) (fmap f t)    

-- A natural number in the range [0, n-1]
data BNat (n :: Nat)  where
    BZero ::           BNat ('S n)
    BSucc :: BNat n -> BNat ('S n)

我们现在可以编写我们的第一个原始递归函数了。我们将编写两个用于标识和加法的示例。

ident :: PRF (S Z)
ident = Proj BZero

add :: PRF (S (S Z))
add = PRec ident (Comp Succ (Cons (Proj (BSucc BZero)) Nil))

请注意，我们在 Haskell 中重用了声明来简化这些函数的编写；我们在add 的定义中重新使用了ident。最终，使用 Haskell 声明的能力将允许我们创建无限或非全部的递归结构，我们可以潜入 PRF 类型。

我们可以编写一些示例代码来试用我们的add 函数。对于seq 和hFlush 的评估顺序，我们会有点偏执，以便我们以后可以看到我们的表示有多么错误。

mseq :: Monad m => a -> m a
mseq a = a `seq` return a

runPRF :: PRF n -> List n Nat -> IO ()
runPRF f i = 
    do
        putStrLn "Compiling function"
        hFlush stdout
        f' <- mseq $ compile f
        putStrLn "Running function"
        hFlush stdout
        n <- mseq $ f' i
        print n

如果我们使用add 运行一个示例，我们会得到一个不错的、令人满意的输出

runPRF add (Cons (S (S Z)) (Cons (S (S (S Z))) Nil))

Compiling function
Running function
S (S (S (S (S Z))))

Haskell 声明

我们可以使用 Haskell 声明做一些有趣且最终具有破坏性的事情。首先，我们将使模式匹配更容易。如果能够使用来自PRec 的模式匹配而不提供使用递归结果的函数，那就太好了。 match 将为我们添加额外的虚拟参数。

match :: (Depths List k) => PRF k -> PRF (S k) -> PRF (S k)
match fz fs = PRec fz (addArgument (BSucc BZero) fs)

为此，它需要一个辅助函数来添加参数 addArgument 和一些其他实用程序来测量具有已知类型 Depths 的列表的大小，比较和转换 BNats，以及证明增加的自然数仍然在新的界限之下。

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE StandaloneDeriving #-}

class Depths f (n :: Nat) where
    depths :: f n (BNat n)

instance Depths List 'Z where
    depths = Nil

instance (Depths List n) => Depths List ('S n) where
    depths = Cons BZero (fmap BSucc depths)

deriving instance Eq (BNat n)
deriving instance Show (BNat n)
deriving instance Ord (BNat n)

bid :: BNat n -> BNat (S n)
bid BZero = BZero
bid (BSucc x) = BSucc (bid x)

addArgument :: (Depths List k) => BNat (S k) -> PRF k -> PRF (S k)
addArgument n f = Comp f . fmap p $ depths
    where
        p d =
            if d' >= n
            then Proj (BSucc d)
            else Proj d'
            where d' = bid d

这在编写诸如

之类的完全合理的东西时非常有用

nonZero :: PRF (S Z)
nonZero = match Const (Comp Succ (Cons (Comp Const Nil) Nil))

isZero :: PRF (S Z)
isZero = match (Comp Succ (Cons Const Nil)) (Comp Const Nil)

isOdd :: PRF (S Z)
isOdd = PRec Const (addArgument BZero isZero)

递归 Haskell 声明

我们还可以写出不只是undefined 的非常具有破坏性的东西。首先，我们将使用递归定义一个while 构造。我们知道用while 构建的东西不应该存在于原始递归函数的闭包中。

while :: (Depths List k) => PRF (S k) -> PRF (S k) -> PRF (S k)
while test step = goTest
    where
        --goTest :: PRF (S k)
        goTest  = Comp goMatch (Cons test (fmap Proj depths))
        --goMatch :: PRF (S (S k))
        goMatch = match (Proj BZero) (addArgument BZero goStep)
        --goStep :: PRF (S k)
        goStep  = Comp goTest (Cons step (fmap (Proj . BSucc) depths))

这让我们可以编写一个仅对某些输入不终止的循环。

infiniteLoop :: PRF (S Z)
infiniteLoop = while isOdd (Comp Succ (Cons Succ Nil))

如果我们对偶数运行此命令，例如 Z 或 S (S Z)，它将终止返回输入。如果我们为奇数运行它，它永远不会完成。

runPRF infiniteLoop (Cons (S Z) Nil)
Compiling function
Running function

因为我们对seq 和hFlush 非常小心，所以我们可以确定编译值以周头范式存在于不是原始递归函数且不仅仅是undefined 的东西中。这是因为compile 步骤并不严格，减少到周头正常形式并不会导致一直减少到头正常形式。我们可以通过将seqs 添加到compile 来解决此问题。我只更改了需要它的两种模式。

compile (Comp f gs) = f' `seq` gs' `seq` go
    where
        go = \ns -> f' . fmap ($ ns) $ gs'
        gs' = fmap compile gs
        f'  = compile f
compile (PRec f g) = f' `seq` g' `seq` h
    where
        h (Cons Z t)     = f' t
        h (Cons (S n) t) = g' (Cons n (Cons (h (Cons n t)) t))
        f' = compile f
        g' = compile g

这将在编译时检查PRF 是否有限。

runPRF infiniteLoop (Cons Z Nil)
Compiling function
GHC stack-space overflow: current limit is 33632 bytes.
Use the `-K<size>' option to increase it.

整理

我们讨论过的类型都没有真正一对一地代表原始递归函数。 PRF a 被上面定义的递归结构和undefined 以外的其他事物所占据。它还包含相同原始递归函数的多种表示形式。例如，恒等函数还有其他定义，包括前导函数（我没有定义）与后继函数的组合。编译的结果，List n Nat -> Nat，被任何具有相同类型的 Haskell 函数所占据，这将包括所有的部分递归函数。

要隐藏同一个函数的多个表示，我们可以使用 Haskell 所做的相同技巧：隐藏函数的内部。如果有人可以检查 PRF 的唯一方法是严格编译它并将其应用到某物上，那么没有人能分辨出相同原始递归函数之间的区别。

将我们的 GADT 转换为类型类并仅导出该类和 compile 就足以隐藏构造函数。

Another interface 可以导出，如果我们稍微转头并注意到原始递归函数的公理类似于Category 定律，Arrow 没有arr（实际上它有相反的情况） arr)，以及仅适用于自然数的有限循环形式。

这应该足以让您相信这几乎是可能的。不管我们做什么，我们仍然会被一个额外的居民undefined所困扰。对 how to make it nice would belong to a different question 的进一步讨论，包括对它应该如何良好的具体关注。