disallowing recursive definitions

[John Nowak]

Recently, I mentioned that if you disallow recursive definitions, then  
definitions can be thought of as macros or rewrite rules. In other  
words, you can replace every occurrence of foo in a program with foo's  
definition and then remove the definition without changing the meaning  
of the program. It is therefore trivial to remove all definitions in a  
program and be left with only a single function that only uses  
primitives built in to the system.

This dual view of definitions as functions and definitions as rewrite  
rules is, at least, aesthetically appealing. I began to think of what  
some other benefits of disallowing recursive definitions might be:

1. It isn't necessary to do tail call optimization; an appropriate  
combinator is used instead.
2. The type system and formalization of the language in general are  
simplified. A restriction on recursive definitions may actually be a  
requirement for a truly compositional type system.
3. WIth a small addition to the type system, it becomes possible to  
prove that the stack will not overflow given the correct set of  
recursive combinators. (Combinators like linrec would need to be  
disallowed or specially handled.)
4. Similarly, it becomes possible compute the maximum number of items  
that will ever be on the stack, and pre-allocate a stack of exactly  
the right size upon program initialization.
5. It allows additional ways of presenting code, such as an editor  
that can expand a definition inline to show what it does while still  
displaying a program with the same meaning.
6. It becomes possible to prove termination when using recursive  
combinators that always terminate given that their arguments always  
terminate (such as primrec).

There are likely other benefits that I'm missing.

The question therefore is how critical recursive definitions actually  
are. They're not necessary in an absolute sense; any recursive  
function can be expressed using while. Essentially, it seems like  
disallowing recursive definitions has the same sort of tradeoff as  
disallowing multiple references to the same value (and therefore  
enforcing linearity): Many nice properties emerge and things are  
simplified, but it may simply be too much of a pain. I think it may be  
worth a shot.

Thoughts?

- John

[John Nowak]

On Feb 28, 2008, at 3:39 PM, John Nowak wrote:

> 6. It becomes possible to prove termination when using recursive
> combinators that always terminate given that their arguments always
> terminate (such as primrec).

To clarify, this is possible with recursive definitions as well.  
Without them however, it's a trivial addition to the type system that  
works exactly the same way that tracking of side effects works.

- John

[John Cowan]

John Nowak scripsit:

> Recently, I mentioned that if you disallow recursive definitions, then  
> definitions can be thought of as macros or rewrite rules.

Sure, but then you can only compute primitive-recursive functions
(roughly speaking, ones in which all loops are bounded at compile time).

--
Do what you will,                       John Cowan
   this Life's a Fiction                cowan@...
And is made up of                       http://www.ccil.org/~cowan
   Contradiction.  --William Blake

[LittleDan]

> Recently, I mentioned that if you disallow recursive definitions, then
>  definitions can be thought of as macros or rewrite rules. In other
>  words, you can replace every occurrence of foo in a program with foo's
>  definition and then remove the definition without changing the meaning
>  of the program. It is therefore trivial to remove all definitions in a
>  program and be left with only a single function that only uses
>  primitives built in to the system.
>
>  This dual view of definitions as functions and definitions as rewrite
>  rules is, at least, aesthetically appealing. I began to think of what
>  some other benefits of disallowing recursive definitions might be:
>
>  1. It isn't necessary to do tail call optimization; an appropriate
>  combinator is used instead.
>  2. The type system and formalization of the language in general are
>  simplified. A restriction on recursive definitions may actually be a
>  requirement for a truly compositional type system.
>  3. WIth a small addition to the type system, it becomes possible to
>  prove that the stack will not overflow given the correct set of
>  recursive combinators. (Combinators like linrec would need to be
>  disallowed or specially handled.)
>  4. Similarly, it becomes possible compute the maximum number of items
>  that will ever be on the stack, and pre-allocate a stack of exactly
>  the right size upon program initialization.
>  5. It allows additional ways of presenting code, such as an editor
>  that can expand a definition inline to show what it does while still
>  displaying a program with the same meaning.
>  6. It becomes possible to prove termination when using recursive
>  combinators that always terminate given that their arguments always
>  terminate (such as primrec).
>
>  There are likely other benefits that I'm missing.
>
>  The question therefore is how critical recursive definitions actually
>  are. They're not necessary in an absolute sense; any recursive
>  function can be expressed using while. Essentially, it seems like
>  disallowing recursive definitions has the same sort of tradeoff as
>  disallowing multiple references to the same value (and therefore
>  enforcing linearity): Many nice properties emerge and things are
>  simplified, but it may simply be too much of a pain. I think it may be
>  worth a shot.
>
>  Thoughts?
>
>  - John

Strictly speaking, recursive functions aren't necessary. However, they
make code a lot more readable than directly using combinators which
take 4 or 5 quotations. Try expressing the Magic Five algorithm (see
http://en.wikipedia.org/wiki/Selection_algorithm#Linear_general_selection_algorithm_-_.22Median_of_Medians_algorithm.22)
to get the median of an array in linear time (for guaranteed O(n log
n) Quicksort) in terms of a recursive combinator. It'd be really hard,
and I'm not sure which combinator would be appropriate. So, maybe you
don't want recursive functions strictly in the minimal formalized
subset of your language, but, like lexically scoped variables, it
might be nice if the compiler did the appropriate transformations to
allow them in user code.

Also, about restricting the set of combinators so the stack doesn't
overflow: I'm not sure if that's worth it. If there's no explicit
recursion, you'd want the set of combinators included to be as general
as possible. (There is a combinator, condnestrec, which encodes
general recursion, and this would obviously not be included if you
want to prevent stack overflow.) Things like depth-first search are
much easier to express on the system stack (which could overflow from
certain graphs) than on an explicit stack, though strictly speaking
it's possible either way (and I guess in some cases you would actually
want to use an explicit stack).

Dan

[LittleDan]

>  Sure, but then you can only compute primitive-recursive functions
>  (roughly speaking, ones in which all loops are bounded at compile time).

With linrec and cons, I think you could build yourself an ad-hoc
variable-depth stack anyway, where loops aren't necessarily bounded.
It'd just be awkward and not any more efficient.

[John Cowan]

Daniel Ehrenberg scripsit:
> >  Sure, but then you can only compute primitive-recursive functions
> >  (roughly speaking, ones in which all loops are bounded at compile time).
>
> With linrec and cons, I think you could build yourself an ad-hoc
> variable-depth stack anyway, where loops aren't necessarily bounded.
> It'd just be awkward and not any more efficient.

True.  It would be interesting to see a concatenative language
with support for data/codata, where you recurse downward on data
and upward on codata, a la "total functional programming".

--
John Cowan  <cowan@...>  http://www.ccil.org/~cowan
        Raffiniert ist der Herrgott, aber boshaft ist er nicht.
                --Albert Einstein

[Christopher Diggins]

On Thu, Feb 28, 2008 at 3:44 PM, John Cowan <cowan@...> wrote:
> John Nowak scripsit:
> > Recently, I mentioned that if you disallow recursive definitions, then
> > definitions can be thought of as macros or rewrite rules.
>
> Sure, but then you can only compute primitive-recursive functions
> (roughly speaking, ones in which all loops are bounded at compile time).

I don't believe this is true. The approach I take is to pass the
function definition as a named parameter to the function, and perform
the point-free conversion.

In Cat I can write the fibonnacci function (a tree recursive
procedure) to take its body as an argument:

>> define fibrec { \f.\n.[n 1 <= [1] [f n 1 - f apply f n 2 - f apply +] if] }

Which my horrible horrible abstraction algorithm translates to:

[dup dup [[[dup dup dup] dip [[[[id 1 <= [1]] papply dip] papply dip]
papply dip] papply dip] dip] dip [[[[[[id] dip id 1 -] papply dip id
apply] papply dip id] dip id 2 -] papply papply dip id apply +] papply
papply papply papply papply papply if]

>> define fib { fibrec swap fibrec apply }
>> 5 fib
8

Incidentally this managed to completely corrupt my type checker, thanks a lot!
:-)

- Christopher

[Joe Bowbeer]

On Thu, Feb 28, 2008 at 12:39 PM, John Nowak wrote:

> Recently, I mentioned that if you disallow recursive definitions, then
> definitions can be thought of as macros or rewrite rules. In other
> words, you can replace every occurrence of foo in a program with foo's
> definition and then remove the definition without changing the meaning
> of the program. It is therefore trivial to remove all definitions in a
> program and be left with only a single function that only uses
> primitives built in to the system.
>
> This dual view of definitions as functions and definitions as rewrite
> rules is, at least, aesthetically appealing. I began to think of what
> some other benefits of disallowing recursive definitions might be:
>
> 1. It isn't necessary to do tail call optimization; an appropriate
> combinator is used instead.
> 2. The type system and formalization of the language in general are
> simplified. A restriction on recursive definitions may actually be a
> requirement for a truly compositional type system.
> 3. WIth a small addition to the type system, it becomes possible to
> prove that the stack will not overflow given the correct set of
> recursive combinators. (Combinators like linrec would need to be
> disallowed or specially handled.)
> 4. Similarly, it becomes possible compute the maximum number of items
> that will ever be on the stack, and pre-allocate a stack of exactly
> the right size upon program initialization.
> 5. It allows additional ways of presenting code, such as an editor
> that can expand a definition inline to show what it does while still
> displaying a program with the same meaning.
> 6. It becomes possible to prove termination when using recursive
> combinators that always terminate given that their arguments always
> terminate (such as primrec).
>
> There are likely other benefits that I'm missing.
>
> The question therefore is how critical recursive definitions actually
> are. They're not necessary in an absolute sense; any recursive
> function can be expressed using while. Essentially, it seems like
> disallowing recursive definitions has the same sort of tradeoff as
> disallowing multiple references to the same value (and therefore
> enforcing linearity): Many nice properties emerge and things are
> simplified, but it may simply be too much of a pain. I think it may be
> worth a shot.
>
> Thoughts?
>
> - John
>
>

As a former Schemer and fan of continuations, I'm conditioned to view (tail)
recursion as the simpler, more powerful concept.  Not looping.

Functional programming languages rely on recursion and still boast of
referential transparency: the ability to substitute function applications by
their definitions.  But they don't take the substitution as far as you'd
like to...

Functional languages favor recursion over looping because looping
traditionally requires a loop variable whose value changes: a side effect.
Recursion also allows tree-like control structures that are not easily
replaced by while loops.

--Joe


[Non-text portions of this message have been removed]

[John Nowak]

On Feb 28, 2008, at 5:23 PM, Christopher Diggins wrote:

> Incidentally this managed to completely corrupt my type checker,  
> thanks a lot!

I'd be surprised if Cat were able to handle such a translation in the  
general case. Take something like the ackermann function in Haskell:

    ack 0 n = n + 1
    ack m 0 = ack (m - 1) 1
    ack m n = ack (m - 1) (ack m (n - 1))

By passing the function itself as an additional argument, we can  
remove the recursive call:

    ackcore f 0 n = n + 1
    ackcore f m 0 = f f (m - 1) 1
    ackcore f m n = f f (m - 1) (f f m (n - 1))

    ack m n = ackcore ackcore m n

Unfortunately, this will fail the occurs check. The only way that Cat  
could not run into this problem is if it discards the recursive  
constraint, which very well could be by your type checker is returning  
nonsense. (Of course, it's hard to tell for sure from here.)

- John

[John Nowak]

On Feb 28, 2008, at 6:47 PM, Joe Bowbeer wrote:

> As a former Schemer and fan of continuations, I'm conditioned to  
> view (tail)
> recursion as the simpler, more powerful concept.  Not looping.

I have a Scheme background as well.

> Functional programming languages rely on recursion and still boast of
> referential transparency: the ability to substitute function  
> applications by
> their definitions.  But they don't take the substitution as far as  
> you'd
> like to...

Indeed.

> Functional languages favor recursion over looping because looping
> traditionally requires a loop variable whose value changes: a side  
> effect.

What's surprising is how easily the stack lets you write code in an  
imperative style while remaining purely functional. Here's a small  
example where, given a natural number, we construct a list from 1 to  
that number:

    ; Scheme, via recursion

    (define (foo n)
      (let f ((n n) (xs '()))
        (if (zero? n)
            xs
            (f (- n 1) (cons n xs)))))

    ; Joy-like, via recursive combinator

    foo = null swap ((cons) keep pred) (zero?) until pop

    ; Another Joy-like version
    ; (prec :: A int int (A int -> A) -> A)

    foo = null swap 1 (cons) prec

- John

[Joe Bowbeer]

Thanks for the examples.

I think there's a relation between stack languages and Lisp's anaphoric
macros:

 http://www.bookshelf.jp/texi/onlisp/onlisp_15.html#SEC99 -and-
 http://common-lisp.net/project/anaphora/anaphora.html

In a stack language, the top of the stack is the anaphoric "it".


On Thu, Feb 28, 2008 at 6:43 PM, John Nowak wrote:

>
> On Feb 28, 2008, at 6:47 PM, Joe Bowbeer wrote:
>
> > As a former Schemer and fan of continuations, I'm conditioned to
> > view (tail)
> > recursion as the simpler, more powerful concept.  Not looping.
>
> I have a Scheme background as well.
>
> > Functional programming languages rely on recursion and still boast of
> > referential transparency: the ability to substitute function
> > applications by
> > their definitions.  But they don't take the substitution as far as
> > you'd
> > like to...
>
> Indeed.
>
> > Functional languages favor recursion over looping because looping
> > traditionally requires a loop variable whose value changes: a side
> > effect.
>
> What's surprising is how easily the stack lets you write code in an
> imperative style while remaining purely functional. Here's a small
> example where, given a natural number, we construct a list from 1 to
> that number:
>
>    ; Scheme, via recursion
>
>    (define (foo n)
>      (let f ((n n) (xs '()))
>        (if (zero? n)
>            xs
>            (f (- n 1) (cons n xs)))))
>
>    ; Joy-like, via recursive combinator
>
>    foo = null swap ((cons) keep pred) (zero?) until pop
>
>    ; Another Joy-like version
>    ; (prec :: A int int (A int -> A) -> A)
>
>    foo = null swap 1 (cons) prec
>
> - John
>
>

[Non-text portions of this message have been removed]

[Christopher Diggins]

On Thu, Feb 28, 2008 at 9:19 PM, John Nowak <john@...> wrote:

>
>
> On Feb 28, 2008, at 5:23 PM, Christopher Diggins wrote:
>
> > Incidentally this managed to completely corrupt my type checker,
> > thanks a lot!
>
> I'd be surprised if Cat were able to handle such a translation in the
> general case. Take something like the ackermann function in Haskell:
>
> ack 0 n = n + 1
> ack m 0 = ack (m - 1) 1
> ack m n = ack (m - 1) (ack m (n - 1))
>
> By passing the function itself as an additional argument, we can
> remove the recursive call:
>
> ackcore f 0 n = n + 1
> ackcore f m 0 = f f (m - 1) 1
> ackcore f m n = f f (m - 1) (f f m (n - 1))
>
> ack m n = ackcore ackcore m n
>
> Unfortunately, this will fail the occurs check. The only way that Cat
> could not run into this problem is if it discards the recursive
> constraint,

Cat does.

> which very well could be by your type checker is returning
> nonsense. (Of course, it's hard to tell for sure from here.)

I suspect this is the problem. Here is the fibonacci function again
(forcing it to use ints):

>> define fib { \f.\n.[n 1 lteq_int [1] [f n 1 sub_int f apply f n 2
sub_int f apply add_int] if] }

Here is the type:

fib : ( -> (A int int int int (A int int int int (A int int int int (A int int i
nt int ((B -> C) -> A int int int int) int -> A int int int int) int -> A int in
t int int) int -> A int int int int) int -> A int int int))

Looks like I am going to have reintroduce recursive types.

- Christopher

[John Nowak]

On Feb 28, 2008, at 10:26 PM, Christopher Diggins wrote:

> Looks like I am going to have reintroduce recursive types.

I've come to the same conclusion. They're almost certainly needed if  
you disallow recursive  definitions. ("Disallow" is really the wrong  
way to put it of course; "choose not to introduce" is more accurate.)

- John

[John Cowan]

Joe Bowbeer scripsit:

> As a former Schemer and fan of continuations, I'm conditioned to view (tail)
> recursion as the simpler, more powerful concept.  Not looping.

Sure it's simpler and more powerful.  That's because it's a general goto
(with transfer of values).  And as Dijkstra said, "the go to statement
as it stands is just too primitive; it is too much an invitation to make
a mess of one's program."

If you haven't actually read Dijkstra's squib, it's very much worth reading at
http://www.u.arizona.edu/~rubinson/copyright_violations/Go_To_Considered_Harmful.html
and numerous other places around the Net.

--
John Cowan   http://ccil.org/~cowan    cowan@...
We want more school houses and less jails; more books and less arsenals;
more learning and less vice; more constant work and less crime; more
leisure and less greed; more justice and less revenge; in fact, more of
the opportunities to cultivate our better natures.  --Samuel Gompers

[Joe Bowbeer]

On Thu, Feb 28, 2008 at 8:35 PM, John Cowan wrote:

> Joe Bowbeer scripsit:
>
> > As a former Schemer and fan of continuations, I'm conditioned to view
> (tail)
> > recursion as the simpler, more powerful concept.  Not looping.
>
> Sure it's simpler and more powerful.  That's because it's a general goto
> (with transfer of values).  And as Dijkstra said, "the go to statement
> as it stands is just too primitive; it is too much an invitation to make
> a mess of one's program."
>
> If you haven't actually read Dijkstra's squib, it's very much worth
> reading at
>
> http://www.u.arizona.edu/~rubinson/copyright_violations/Go_To_Considered_Harmful.html<http://www.u.arizona.edu/%7Erubinson/copyright_violations/Go_To_Considered_Harmful.html>
> and numerous other places around the Net.
>
>

As far as I know, Dijkstra didn't have a beef with recursion.

The author of the following retrospective writes that Dijkstra probably
considered recursion to be intellectually easier to grasp than iterative
looping:

 http://david.tribble.com/text/goto.html

In any event, it's clear from Dijkstra's letter than he didn't consider
recursion to be harmful!

To avoid confusion, I should have used the word "elegant".

Recursion is the simple, elegant solution.

--
Joe Bowbeer
  http://mitpress.mit.edu/sicp/front/node3.html
    [ Sobre los gustos no hay disputa. ]


[Non-text portions of this message have been removed]

[William Tanksley, Jr]

John Cowan <cowan@...> wrote:
> Joe Bowbeer scripsit:
>  > As a former Schemer and fan of continuations, I'm conditioned to view (tail)
>  > recursion as the simpler, more powerful concept.  Not looping.

>  Sure it's simpler and more powerful.  That's because it's a general goto
>  (with transfer of values).  And as Dijkstra said, "the go to statement
>  as it stands is just too primitive; it is too much an invitation to make
>  a mess of one's program."

I'm generally on Knuth's side on this one.

But I don't see how tail recursion is a general goto statement. It
seems structured -- in particular, a tail recursion has only one entry
point.

>  John Cowan   http://ccil.org/~cowan    cowan@...

-Wm

[John Cowan]

William Tanksley, Jr scripsit:

> I'm generally on Knuth's side on this one.

Remember that Knuth thought Dijkstra was *mostly* right, and takes care to
disclaim the notion that he is in favor of random gotos.  AFAIK, gotos are
only used in TeX to compensate for Pascal's lack of a return statement.

> But I don't see how tail recursion is a general goto statement. It
> seems structured -- in particular, a tail recursion has only one entry
> point.

If you take an arbitrary tagbody (a list of statements and labels with
gotos embedded in the statements), you can restructure it into a sequence
of functions, one per label, where each function ends by tail calling the
next function in sequence (corresponding to flowing through the label)
and each goto is changed into a tail call.  This can be done entirely as
a local transformation.

So while it's true that tail calls have only one entry point, entry
points and labels are basically the same thing from a Scheme perspective,
something that neither Knuth nor Dijkstra deals with.  "Lambda: the
ultimate GOTO."

--
Well, I have news for our current leaders       John Cowan
and the leaders of tomorrow: the Bill of        cowan@...
Rights is not a frivolous luxury, in force      http://www.ccil.org/~cowan
only during times of peace and prosperity.
We don't just push it to the side when the going gets tough.  --Molly Ivins

[Joe Bowbeer]

On Fri, Feb 29, 2008 at 5:36 AM, John Cowan wrote:

> William Tanksley, Jr scripsit:
>
> > I'm generally on Knuth's side on this one.
>
> Remember that Knuth thought Dijkstra was *mostly* right, and takes care to
> disclaim the notion that he is in favor of random gotos.  AFAIK, gotos are
> only used in TeX to compensate for Pascal's lack of a return statement.
>
> > But I don't see how tail recursion is a general goto statement. It
> > seems structured -- in particular, a tail recursion has only one entry
> > point.
>
> If you take an arbitrary tagbody (a list of statements and labels with
> gotos embedded in the statements), you can restructure it into a sequence
> of functions, one per label, where each function ends by tail calling the
> next function in sequence (corresponding to flowing through the label)
> and each goto is changed into a tail call.  This can be done entirely as
> a local transformation.
>
> So while it's true that tail calls have only one entry point, entry
> points and labels are basically the same thing from a Scheme perspective,
> something that neither Knuth nor Dijkstra deals with.  "Lambda: the
> ultimate GOTO."
>
>

I would say, rather: "continuations: the ultimate goto".  And I would mean
that in a good way:)

What you're describing is an equivalence between gotos and a sequence of
function calls, something which is not 100% possible without support for
recursion, and something which is not 100% efficient without tail-call
optimization, but I can't see how you can twist this around to indict
recursion.

I do sort of see, now, how the anaphoric (from hell?) quality of stack
programming languages does provide a lot of expressive power without the
need to resort to recursion.

--Joe


[Non-text portions of this message have been removed]