"Variadic" Lambda Calculus Abstractions

[bakgatviooldoos]

Hi, Racket Discourse.

I guess this is more of a theoretical question than a Racket question, per se, but the audience is well-placed, nonetheless.

I am thinking about how one would implement "sugar" for variadic lambda abstractions, to avoid the need for right-hand wrapping expressions like cons when constructing a list for example, without necessarily resorting to syntactical sugar.

From what I can tell, one needs either:

• a) a counter of some sort, to "allocate" some number of arguments, or
• b) a sentinel value of some sort, to end a sequence of arguments

Considering the first option, as an example, one might define a procedure called FEED, taking a counter and some procedure f which is left-folded over any arguments applied to the continuation, until the counter is exhausted.

;; I am using a little DSL for de bruijn-index notation

(define FEED #λ ;; foldl-like
  [ ; _₃ f
    [ ; _₂ rec
      [ ; _₁ ctr
        [ ; _₀ accu
          IF (ZERO? _₁) _₀
             [_₃ (PRED _₂) (_₄ _₀ _₁)]
        ]
      ]
    ]
  ]
)
;; which roughly translates to the partially recursive
(lambda (f)
  (lambda (rec)
    (lambda (ctr)
      (lambda (accu)
        (if (zero? ctr)
            accu
            (lambda (x) ((rec (sub1 ctr)) (f x accu))))))))

This can then be used to define LIST:

(define LIST #λ[Y (FEED CONS) _₀ NULL]) ;; recursion using the Y-combinator
(define LIST₄
  #λ(LIST FOUR 1 2 3 4)) ;; although this is (list 4 3 2 1) haha

So, my question is, are there any other tactics besides counters and sentinel values to perform this sort of thing, or is it just the way it goes?

I mean, I can't see how you would get around saying, "stop," in this way, but one never knows.

[usao]

The way Haskellers do it (as seen in printf, whether or not you like it) is to use a type class that dispatches to either a continuation or the overall result, but well that’s just syntactic sugar cheating.

I think the two ways listed are all the options. I do think the “sentinel value” approach makes more sense, because you can as well just make a combinator that packs arguments into a list, like

#lang racket/base

(struct end ())
(define the-end (end))

(define (fix f)
  ((lambda (x) (f (lambda (v) ((x x) v))))
   (lambda (x) (f (lambda (v) ((x x) v))))))

(define (variadic f)
  ((fix (lambda (loop)
          (lambda (cont)
            (lambda (v)
              (if (end? v)
                  (cont null)
                  (loop (lambda (tail)
                          (cont (cons v tail)))))))))
   (lambda (lst) (f lst))))

(define list (variadic (lambda (lst) lst)))
((((list 1) 2) 3) the-end)

(define sum
  (variadic
   (fix (lambda (loop)
          (lambda (nums)
            (if (null? nums)
                0
                (+ (car nums) (loop (cdr nums)))))))))
((((sum 1) 2) 3) the-end)

Note that I also used a continuation-passing trick to build the list. This overall seems more uniformed than the counter-passing convention.

[bakgatviooldoos]

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

[usao]

It’s essentially just the same principle if you’re doing it in a typed setting: you need to wrap it in a variant type, say (let’s use Shplait syntax)

type Arg(?a)
| one(v :: ?a)
| end()

To translate this typed setting into the pure lambda calculus, you can use a Mogensen–Scott encoding. To demonstrate this, see

#lang lazy

(define (fix f)
  ((lambda (x) (f (x x)))
   (lambda (x) (f (x x)))))

(define diverge
  ((lambda (x) (x x))
   (lambda (x) (x x))))

;; type Arg(?a)
;; | one(v :: ?a)
;; | end()
(define (((one v) a) b)
  (a v))
(define ((end a) b)
  b)

;; type List(?a)
;; | cons(x :: ?a, xs :: List(?a))
;; | null()
(define ((((cons x) xs) a) b)
  ((a x) xs))
(define ((null a) b)
  b)

(define (head xs)
  ((xs (lambda (x)
         (lambda (xs)
           x)))
   diverge))

(define (variadic f)
  ((fix (lambda (loop)
          (lambda (cont)
            (lambda (arg)
              ((arg (lambda (v)
                      (loop (lambda (tail)
                              (cont ((cons v) tail))))))
               (cont null))))))
   (lambda (lst) (f lst))))

(define list (variadic (lambda (lst) lst)))
(head ((((list (one 1)) (one 2)) (one 3)) end))

Note that I had to use lazy here, because the encoding only works right under call-by-{name,need} (or if you make nullary handler take a unit value, but let’s keep that bureaucracy out). Also keep in mind that even more type-wrangling would be needed in a typed setting to get the recursion right.

[bakgatviooldoos]

Beautiful, @usao.

I never knew about lazy, thank you for the use.

I was just reading about MSE, also related to bruijn. I guess it stands to reason, but I am delighted that there is such a "direct" connection from this problem to meta-programming (referring to the link).