Argument for less recursion in datatype definitions

Date: Wed, 22 Mar 89 14:39:05 PST

        From: Gavin Wraith 
<gavinw%cogs.sussex.ac.uk-LEftKC8aXbilgWnZye4G+Q@xxxxxxxxxxxxxxxx>
        ...
        I am rather gratified to have had so much response to the kite I
        flew.

Spring is a nice season for flying kites.  For a spot of off-the-wall
writing, here's my anti-recursion kite.

Recursion is an invention of logic, not mathematics.  Real programmers
don't write Pascal, and real mathematicians don't recurse.  Neither do
many logicians nowadays, and computer science has become the last
refuge of recursion.  The writing is on the wall for recursion.

Or, to quote from my article on LISP in Encyclopedia of Computer Sciences
and Technology, vol. 10, (ed. Belzer et al), 1978:

                To iterate is illiterate.
                To recurse is worse.
                To avoid this trap see
                Instructions for mapc.

Now if you absolutely and positively have to use recursion to define
streams then what could be more appropriate than

        Stream(t) = t x Stream(t)?

But given the option I would rather define a stream as a function on
omega.

The general principle here is, rather than defining complex structures
recursively, start out with some basic recursively defined structures,
such as the ordinals, and treat the more complex structures as
functions defined on the basic structures.  Particular functions may be
most naturally defined by recursion, but what is the benefit of
defining the *type* of such functions by recursion?

By coincidence I ran across much the same principle yesterday in one of
the references on comma categories John Gray provided in response to my
request, namely his 1973 book LNM 371, "Formal Category Theory:
Adjointness for 2-categories."  There he takes the view that much of
the structure of category theory is reduced to that of a five-object
full sub-2-category of Cat, namely the ordinals 1 through 4 along with
2x2, under exponentiation (with the ordinals and their functors in the
exponent).  p7: "It turns out that in the things treated in Parts III
and IV - fibrations, the Yoneda lemma, adjointness, etc., -- the
crucial structure is provided by the functors and natural
transformations between 3 and 2x2." p10: "All this structure
transports itself throughout Cat by exponentiation."

Come to think of it, my amateur's account of lax pullbacks contains a
(relatively trivial) instance of this sort of thing, where I argued

              2 D          2xD          Dx2           D 2
            (C )     ~    C       ~    C       ~    (C )          (6)

The reasoning here takes place exclusively in the exponent.  Apparently
such "logic in the exponent" is not an isolated phenomenon but is
applicable to "much of category theory."

This is the first I'd heard of this application of that perspective,
but it seems like an excellent way to look at things.  Whatever its
advantages and disadvantages, they are presumably shared with the
approach of defining data structures as functions on ordinals and other
suitable structures such as graphs instead of directly by recursion.

I'd love to know what camps exist on this.  Are there other strong
opinions out there on the pros and cons of defining data types directly
by recursion vs. indirectly on simpler bases?
-v