<p>Your function is completely structurally recursive on <code>n</code>, so it is pretty much just a change of notation to make it a catamorphism on the natural numbers.</p>

<pre><code>type nat = Z | S of nat 

(* cata : α → (α → α) → nat → α *)                      
let rec cata z s = function
  | Z -&gt; z 
  | S n -&gt; s (cata z s n)

(* halting_search : nat → (α → bool) → (α → α) → α → α option *)             
let halting_search n = 
  cata (fun test next seed -&gt; None)
       (fun recur test next seed -&gt; 
         if test seed then 
           Some seed
         else 
           recur test next (next seed))
       n
</code></pre>

<p>For languages with higher-order functions and strictly positive datatypes, having a fold is equivalent in expressive power to permitting structural recursion. However, it is not equivalent in terms of efficiency. If you just have fold, then implementing the predecessor function on the Peano natural numbers is O(n), whereas if you have a case form, it is O(1). </p>

<pre><code>(* This is linear time! *)
pred : nat -&gt; nat option 
let pred n = cata None (function 
                           | None   -&gt; Some Z 
                           | Some n -&gt; Some (S n)) n 
</code></pre>

CC BY-SA 3.0
2018-02-14T07:56:45.977Z
If the language iz lazy, doesn't the predecessor implemented with `fold` become efficient?
Andrej Bauer
CC BY-SA 3.0
2018-02-14T13:03:47.807Z
If you just have the fold as the only eliminator, this is equivalent to the Church encoding in System F, and my understanding is that Church encodings of the natural numbers don't support constant-time predecessor regardless of evaluation order (IIRC, you need the Scott encoding for that). But now I'm wondering if I am wrong...
Neel Krishnaswami
CC BY-SA 3.0
2018-02-14T14:09:00.720Z
I am just thinking "what would Haskell do"?
Andrej Bauer
CC BY-SA 3.0
2018-02-13T12:28:36.467Z
2018-02-13T12:28:36.467Z
Neel Krishnaswami
<p>In particular, I am thinking of a function which involves conditionals changing the recursive behavior and multiple F-algebras.</p>

<pre><code>halting_search :: int -&gt; (a -&gt; bool) -&gt; (a -&gt; a) -&gt; a -&gt; Maybe a
halting_search 0 f_test f_next_candidate candidate = Nothing
halting_search (S n) f_test f_next_candidate candidate = case (f_test candidate) of
  true =&gt; Just candidate
  false =&gt; halting_search n f_test f_next_candidate (f_next_candidate candidate)
</code></pre>

<p>Is this capable of being written just using the <code>cata</code> operator?  The reason I'm asking is because I want a functional language that is fairly expressive but not overly expressive, and it seems like one way to do that might be to not allow explicit recursion but make <code>cata</code> a primitive function.</p>

<functional-programming><ct.category-theory>
Can all structurally recursive functions be written without explicit recursion using a catamorphism/fold?
lightning
# Can all structurally recursive functions be written without explicit recursion using a catamorphism/fold?

(Asked by: username_0 on 2018-02-12)

In particular, I am thinking of a function which involves conditionals changing the recursive behavior and multiple F-algebras.
halting_search :: int -> (a -> bool) -> (a -> a) -> a -> Maybe a
halting_search 0 f_test f_next_candidate candidate = Nothing
halting_search (S n) f_test f_next_candidate candidate = case (f_test candidate) of
  true => Just candidate
  false => halting_search n f_test f_next_candidate (f_next_candidate candidate)

Is this capable of being written just using the cata operator?  The reason I'm asking is because I want a functional language that is fairly expressive but not overly expressive, and it seems like one way to do that might be to not allow explicit recursion but make cata a primitive function.

**Tags:** functional-programming, ct.category-theory


---

## 1 answers

### Answer by username_1 on 2018-02-13. Score: 7 | Accepted answer

Your function is completely structurally recursive on n, so it is pretty much just a change of notation to make it a catamorphism on the natural numbers.
type nat = Z | S of nat 

(* cata : α → (α → α) → nat → α *)                      
let rec cata z s = function
  | Z -> z 
  | S n -> s (cata z s n)

(* halting_search : nat → (α → bool) → (α → α) → α → α option *)             
let halting_search n = 
  cata (fun test next seed -> None)
       (fun recur test next seed -> 
         if test seed then 
           Some seed
         else 
           recur test next (next seed))
       n

For languages with higher-order functions and strictly positive datatypes, having a fold is equivalent in expressive power to permitting structural recursion. However, it is not equivalent in terms of efficiency. If you just have fold, then implementing the predecessor function on the Peano natural numbers is O(n), whereas if you have a case form, it is O(1). 
(* This is linear time! *)
pred : nat -> nat option 
let pred n = cata None (function 
                           | None   -> Some Z 
                           | Some n -> Some (S n)) n

> **Comments:**
> **username_2**: If the language iz lazy, doesn't the predecessor implemented with `fold` become efficient?  
> **username_1**: If you just have the fold as the only eliminator, this is equivalent to the Church encoding in System F, and my understanding is that Church encodings of the natural numbers don't support constant-time predecessor regardless of evaluation order (IIRC, you need the Scott encoding for that). But now I'm wondering if I am wrong...  
> **username_2**: I am just thinking "what would Haskell do"?  

---

