Special syntax for anonymous tail recursion

[lukaszcz]

A common pattern in eager functional programming languages is introducing a helper tail-recursive function with additional "accumulator" arguments. The naming of this helper function is usually redundant. The helper function is used only to implement tail-recursion. One could want a special syntax capturing this pattern, extending the syntax of anonymous lambda-abstraction.

Clojure has a similar "loop" construct. Coq has anonymous recursion (fixpoints), but without explicit "accumulator" arguments.

Examples

The function:

fact : Nat -> Nat;
fact n := go 1 n;
  where
    go : Nat -> Nat -> Nat;
    go acc 0 := acc;
    go acc n := go (n * acc) (n - 1);

would translate to:

fact : Nat -> Nat;
fact := \(acc := 1){
  0 := acc;
  n := @\ (n * acc) (n - 1);
};

The function:

rev : {A : Type} -> List A -> List A;
rev l := go [] l;
  where
    go : List A -> List A -> List A;
    go acc [] := acc;
    go acc (h :: t) := go (h :: acc) t;

would translate to:

rev : {A : Type} -> List A -> List A;
rev := \(acc := []){
  [] := acc;
  h :: t := @\ (h :: acc) t;
};

The function:

fib : Nat -> Nat;
fib n := go 0 1 n;
  where
    go : Nat -> Nat -> Nat -> Nat;
    go x y n := x;
    go x y (S n) := go y (x + y) n;

would translate to

fib : Nat -> Nat;
fib := \(x := 0)(y := 1) {
  0   := x;
  S n := @\ y (x + y) n;
};

[mariari]

Clojure has a similar "loop" construct. Coq has anonymous recursion (fixpoints), but without explicit "accumulator" arguments.

Clojure only does this due to lack of TCO support in the JVM. Scheme does something similar to what is wanted here with it's let abstraction

(define (fact x)
  (let loop ((n x) (acc 1))
    (if (= 0 n)
        acc
        (loop (- n 1) (* acc n)))))

(fact 3)
6

Here loop is defined and called at the same time, this is almost as anonymous as the clojure case, as they use the word recur to refer to the nearest loop.

[lukaszcz]

Thanks for pointing out an analogous syntax in Scheme! I did play a bit with Scheme a long time ago, but I've already forgotten about named lets.

For reference, here's an explanation of this Scheme syntax: https://icem.folkwang-uni.de/~finnendahl/cm_kurse/doc/schintro/schintro_126.html#SEC165

[lukaszcz]

Since the most common case is to do tail recursion with the most recently introduced local function, explicitly naming it is usually redundant. We could consider adding a syntax for optionally locally naming the function, e.g.,

\[loop](acc := 1) {
  x := if x = 0 then acc else loop (n * acc) (n - 1)
}

[mariari]

I forgot to mention this piece of history, but there is an entire genre of macros that describe what you want, they are usually called anaphoric macros, and in particular you want alambda

 (defmacro alambda (parms &body body)
   `(labels ((self ,parms ,@body))
      #'self))

 ;; Factorial function defined recursively where `self' refers to the alambda function
 (alambda (n) 
   (if (= n 0)
       1 
       (* n (self (1- n)))))

https://en.wikipedia.org/wiki/Anaphoric_macro

here is a wikipedia page on their history, note that other languages like rust have similar ideas for let though they do give a brief name instead of making them Anaphoric

if let HitShift::Hit(shift) = hit_shift {

[lukaszcz]

Thanks again!

I think I like "self" for the recursive call more than "@\". We don't need to make it a keyword -- we can just implicitly bind it locally in the lambda.

As for macros of various kind, yes, one could implement all kinds of "syntactic sugar" with them. But for now we're not ready to introduce them into the language. Perhaps in some distant future when we move toward dependent types and need some meta-programming facility.

[lukaszcz]

We agreed on #1638