Nice representation of primitive recursive functions in haskell

Question

I argued in the answer to a previous question that it's possible to represent in Haskell the union of the primitive recursive functions (PRFs) and the single extra value of ⊥ or undefined. This argument was based on a direct translation of an axiomatic construction of primitive recursive functions; it required a number of language extensions and type-level reasoning about the arity of functions. Is it possible to represent an equivalent set of primitive recursive functions in more idiomatic Haskell?

An idiomatic representation of PRFs should ideally be able to meet all of the following:

• Provide a Category instance
• Not need to mess around with type-level reasoning about function arity

In addition to the requirements for being primitive recursive

• Any function that's undefined for an input is undefined for all inputs. This restricts the set of PRFs to a single inescapable extra value of ⊥ instead of containing multiple partially recursive functions.This means that any definition of a while loop or similar partially recursive function should be undefined.

I noticed that the axioms for primitive recursive functions are like the Category laws, Arrow without arr (in fact it has the opposite of arr), and a limited form of looping that only works on natural numbers.

Answer 1

There's a very straightforward representation of primitive recursive functions in Haskell. It's a newtype for a function that we will assert is a correct-by-construction primitive recursive function. We don't export the constructor to prevent the construction of arbitrary functions which could be partially recursive. This technique is called a smart constructor.

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

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

We also need to provide an interface by which to build PRFs. A Category instance will provide the composition portion of the extended composition required for PRFs.

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)

The seqs require that f and g be in weak head normal form before any result can be calculated from them; if either function is undefined then the composition will be undefined as well.

The primitive recursive functions also require projection to select one argument from many. We'll view this as selecting one piece of data from a structure of data. If we use tuples instead of lists of known length the projection functions become fst and snd. Together with something like Arrow's (&&&) to build tuples we can cover all the requirements for extended projection. PRFs are like "Arrow without arr"; arr would allow arbitrary partially recursive functions to be made into PRFs. We'll define the class of ArrowLike categories.

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)

The projection functions fst and snd take the place of arr. They are the only functions needed to describe ArrowLike behavior when combined with fanout (&&&).

Before we provide an ArrowLike instance for PRF we'll say how ordinary functions (->) are ArrowLike

import qualified Prelude (fst, snd)

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

For PRFs we'll use the same inductive step we used in the definition of (.) for the Category instance and demand that both functions be in weak head normal form.

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

Finally, we'll provide the primitive recursion itself. We'll translate primitive recursion directly from the axiomatic definition using tuples instead of increasing function 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 is a natural number given by data Nat = Z | S Nat. I'm choosing to view the constant function zero and the successor function as part of primitive recursion, the only way the Nat values they construct can be deconstructed or inspected is with prec. It is tempting to replace zero with const :: c -> a b c; this would be a fatal flaw as someone could introduce infinity = S infinity with const to turn prec into an infinite loop.

The partially recursive functions (->) support primitive recursion.

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))

We'll define primitive recursion for PRF using the same inductive trick we used for (.) and (&&&).

instance PrimRec PRF where
    zero = PRF zero
    succ = PRF succ
    prec (PRF f) (PRF g) = PRF $ f `seq` g `seq` prec f g

The primitive recursive functions are a Category with the ability to construct and deconstruct both tuples and natural numbers.

Examples

Primitive recursive functions such as add are easier to define with this interface.

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)

We can still define useful functions like match which helps build primitive recursive functions that branch on whether a natural is zero.

match :: PrimRec a => a b c -> a (Nat, b) c -> a (Nat, b) c
match fz fs = prec fz (fs . snd)

Using match we can easily quickly test if a value is Z and eventually whether it is odd

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)

We can still write Haskell declarations that are generally recursive, but all PRFs built this way will be 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

This function, infiniteLoop, would fail to terminate only for odd inputs.

infiniteLoop :: PrimRec a => a Nat Nat
infiniteLoop = while isOdd (succ . succ)

When running our examples, we will be careful about the evaluation order like in the 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

We can evaluate PRFs that were defined conveniently in terms of match.

run isOdd (S $ S $ S Z)

Compiling function
Running function
S Z

But the function defined by infiniteLoop is undefined in general, not just for odd values.

run infiniteLoop (Z)

Compiling function