From a pair to a list in lambda calculus / scheme

Question

I'm learning a bit about lambda calculus (which is very neat) and have defined the following in scheme for how a pair would be done:

; PAIR
; λabf.fab
(define PAIR (lambda (a) (lambda (b) (lambda (f) ((f a) b)))))
(define mypair ((PAIR 1) 2))

; FIRST
; λab.a
(define FIRST (lambda (a) (lambda (b) a)))

; SECOND
; λab.b
(define SECOND (lambda (a) (lambda (b) b)))

(display "First is: ")     (display (mypair FIRST))
(display " | Second is: ") (display (mypair SECOND))

First is: 1 | Second is: 2

How would one abstract this further to create a data structure of a list, for example, to make something like [1 2 3 4 5] instead of just [2 3] ?

The best I've been able to do by myself is to sort of hardcode these, for example, for five:

(define five (
    (PAIR 1) (
      (PAIR 2) (
        (PAIR 3) (
          (PAIR 4) 5)))))

(display (five FIRST)) (display ((five SECOND) FIRST)) (display (((five SECOND) SECOND) FIRST)) (display ((((five SECOND) SECOND) SECOND) FIRST)) (display ((((five SECOND) SECOND) SECOND) SECOND))

12345

Is there a more 'general' solution for this?

Answer 1

Normal LISP lists are not [1 2 3], they are (1 . (2 . (3 . ()))). They are created with (cons 1 (cons 2 (cons 3 '()))) so the exact equal list in lambda calculus would be ((PAIR 1) ((PAIR 2) ((PAIR 3) ...)))

Now a standard lisp implementation usually prints (1 2 3), but that is some funky magic done by the printer. Its rule is that if the cdr is a list you can omit the dot and one set of parentheses. When you are using lambda calculus to model data the REPL will always show lambda/closure objects so you need utility functions that understands the structure and displays a visualization that corresponds. This is not par of lambda calculus as for it it is OK to just satisfy the axioms:

(car (cons a b)) ; ==> a
(cdr (cons a b)) ; ==> b

list is a auxiliary function that cons chain the arguments. You could indeed make something similar for pairs but it is not a part of lambda calculus:

(define TRUE (lambda (p) (lambda (q) p)))
(define NIL (lambda (x) TRUE))

(define (ch-list . args)
  (let helper ((lst (reverse args)) (result NIL))
    (if (null? lst)
        result
        (helper (cdr lst)
                ((PAIR (car lst)) result)))))