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

我在 answer to a previous question中论证,可以在Haskell中表示 primitive recursive functions(PRF)的联合以及⊥或undefined的单个额外值.这个论点是基于原始递归函数的公理结构的直接翻译;它需要一些语言扩展和关于函数arity的类型级推理.是否有可能在更惯用的Haskell中表示一组等效的原始递归函数?

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

>提供类别实例
>不需要乱搞关于函数arity的类型级推理

除了原始递归的要求

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

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

在Haskell中有一个非常简单的原始递归函数表示.它是函数的新类型,我们将断言它是一个正构构造的原始递归函数.我们不导出构造函数以防止构造可能部分递归的任意函数.这种技术称为 smart constructor.

module Data.PRF (
    -- We don't export the PRF constructor
    PRF (runPRF),
) where

newtype PRF b c = PRF {runPRF :: b -> c}

我们还需要提供一个构建PRF的接口. 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处于弱头正常形式,然后才能从中计算出任何结果;如果任一函数未定义,那么组合也将是未定义的.

原始递归函数还需要投影从多个参数中选择一个参数.我们将此视为从数据结构中选择一条数据.如果我们使用元组而不是已知长度的列表,则投影函数变为fst和snd.与Arrow(&&&)之类的东西一起构建元组,我们可以满足扩展投影的所有要求. PRF就像“没有arr的箭头”; arr允许将任意部分递归函数转换为PRF.我们将定义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)

对于PRF,我们将使用我们在(.)的定义中用于Category实例的相同归纳步骤,并要求两个函数都处于弱头正常形式.

instance ArrowLike PRF where
    fst = PRF fst
    snd = PRF snd
    PRF f &&& PRF g = PRF $f `seq` g `seq` (f &&& g)

最后,我们将提供原始递归本身.我们将使用元组直接从公理定义转换原始递归,而不是增加函数arities.

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是由数据Nat = Z |给出的自然数S Nat.我选择将常量函数零和后继函数视为原始递归的一部分,它们构造的Nat值的唯一解析方法是使用prec进行解构或检查.用const :: c – >替换零是很诱人的. a b c;这将是一个致命的缺陷,因为有人可以用const引入infinity = S infinity来将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

原始递归函数是一个类别,具有构造和解构元组和自然数的能力.

例子

使用此接口更容易定义诸如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 :: PrimRec a => a b c -> a (Nat, b) c -> a (Nat, b) c
match fz fs = prec fz (fs . snd)

使用匹配,我们可以很容易地快速测试值是否为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都是未定义的.

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.

run isOdd (S $S $S Z)

Compiling function
Running function
S Z

但是,infiniteLoop定义的函数通常是未定义的,不仅仅是奇数值.

run infiniteLoop (Z)

Compiling function
相关文章
相关标签/搜索