"Variadic" Lambda Calculus Abstractions

Thanks, @usao, that's spiffy!

I agree that the sentinel seems more coherent. On the other hand, if one were to go "full lambda", so to speak, with ~all terms in the reduction as lambdas, one has to devise a value that can never appear among the arguments passed to our variadic procedure, in order to distinguish it.

I guess this is where one would use "boxing" of some kind, such that each argument is wrapped in some standard term, perhaps with an empty box representing the sentinel.

Stealing some bits I saw from bruijn, one might have:

(define TRUE  (lambda (x) (lambda (y) x)))
(define FALSE (lambda (x) (lambda (y) y)))
(define IF    (lambda (x) (lambda (y) (lambda (z) ((x y) z)))))

(define BOX        (lambda (x) (lambda _ (lambda (y) (y x)))))
(define EMPTY-BOX  (lambda (x) (lambda _ x)))
(define EMPTY-BOX? (lambda (x) ((x TRUE) (lambda _ FALSE))))

(define BOX-GET (lambda (x) (lambda (y) ((y x) (lambda (z) z)))))

(define NULL  (lambda _ TRUE))
(define CONS  (lambda (x) (lambda (y) (lambda (z) ((z x) y)))))
(define HEAD  (lambda (x) (x TRUE)))

;; not as general as before, but demonstrates the principle
(define (variadic′ f)
  ((fix
    (lambda (loop)
      (lambda (cont)
        (lambda (v)
          (((IF (EMPTY-BOX? v))
            (cont NULL))
           (loop
            (lambda (tail)
              (cont ((CONS ((BOX-GET 'none) v)) tail)))))))))
   (lambda (lst) (f lst))))

(define list′ (variadic′ (lambda (x) x)))

(HEAD ((((list′ (BOX 1)) (BOX 2)) (BOX 3)) EMPTY-BOX))
;=> 1