λ calculus Example - Lists

Lists and list operators are usually "built in" with programming languages based on λ calculus but they can be defined in λ calculus. The following example shows a way to define CONS, NIL, HD (head), TL (tail), and NULL. (PRINT is a cheat because it is defined using the system's built-in lists ('::'), but it too could be defined in λ calculus.)

Lists:-

let rec
 CONS = lambda h. lambda t. lambda f. f h t,

 NIL = lambda f. true,

 NULL = lambda L. L (lambda h. lambda t. false),

 HD = lambda L. L (lambda h. lambda t. h),

 TL = lambda L. L (lambda h. lambda t. t),

 PRINT = lambda L.
   if NULL L then '/' else (HD L)::(PRINT (TL L))

in let L = CONS 1 (CONS 2 (CONS 3 NIL)) {an e.g.}

in PRINT( CONS (NULL NIL)       {T}
        ( CONS (NULL L)         {F}
        ( CONS (HD L)           {1}
        ( CONS (HD (TL L))      {2}
        ( CONS (HD (TL (TL L))) {3}
          NIL)))))              {/}

{ Define (Flat) Lists From Scratch. }




Also see [Boolean], [Ints], and built-in [lists].