Making Sense of Lambda Calculus 5: Bring Computation to (Aggregate) Data

A bright thumbnail with black text. The text is arranged in a schematic tree. The tree first branches to LAM and BDA, then to CAL, and finally to CULUS. The branches are soft academic purple. Attributions to AARTAKA.me and Artyom Bologov are in the bottom corners.

So we've covered numbers as compositions and booleans as branches in this series of posts. But both of these are "primitive" data types. We need aggregate types to build the whole world out of! This post goes over simple techniques to build data types in Lambda Calculus. And some conventional types too.

Note on syntax

Starting with this post, I'll use syntax of Lamber, my Lambda Calculus-based programming language. I find it more readable than conventional single-letter-single-argument lambdas.

Conses/Tuples/Pairs: All You Need #

A simple idea that generalizes to all of this post (and beyond:) Bring computation to data, not the other way around. It's a bit of a brain teaser, but let's see for ourselves. Conses (or pairs, or tuples) are two-element collections. With "car" (head) and "cdr" (tail):

def cons fn (car cdr)
  (fn (f) f car cdr) .

Cons type definitions

So cons takes two things: car and cdr. Then it takes a third argument, a function. It's curried, so we don't have to provide this function upfront. And applies the function to the first two arguments. That's what I was talking about. Make cons user provide their action on data. Don't just provide the data to them.

Now the simplest action might be fetching values. Here are two functions for fetching cons parts.

def car fn (pair)
  pair (fn (a b) a) .

def cdr fn (pair)
  pair (fn (a b) b) .

Cons accessors

See that? We apply the data structure to the accessor function. Not the other way around. It's counter-intuitive, but useful and generalizes well. Say, for...

Triples #

Triples are like tuples/conses, but with three elements.

def triple fn (first second third)
  (fn (f) f first second third) .

def first fn (triple)
  triple (fn (a b c) a) .

;; Et cetera for second and third

Triple definition

Trees #

With this simple two or three element collection, we can build arbitrarily complex structures. Cons trees (binary, ternary, or whatever else you come up with.) That's what Lisp code is all about—trees of symbols.

cons (cons 1 2)
     (cons (cons 3 (cons 4 nil)) (cons 5 (cons 6 7)))

Cons tree

Represents a tree with

1 and 2 (as one pair)
3 and 4 (as a so-called proper nil-terminated list)
and 5, 6, and 7 (as a chain of conses)

Or, visualizing it with a little piece of ASCII art (generated by draw-cons-tree)

[o|o]---[o|o]-------[o|o]-[o|o]-7
 |       |           |     |
[o|o]-2 [o|o]-[o|/]  5     6
 |       |     |
 1       3     4

Cons tree, visualized

See the tree there? Not the most readable thing, but the benefit is apparent: It allows creating arbitrarily complex structures. So we only need conses, right? In a sense yes, but there are more tricks and types we can use:

Union Types #

We can increase the number of values we store in the structure, like with triples. But we can also increase the number of actions! That's how union types actually work in LC. Get multiple functions, one per possible type, and only run the one matching the type.

The most representative union type is Either. Basically, it's either Left with one value (usually an error,) or Right with the other value (usually a result.)

def left fn (leftval)
  fn (leftfn rightfn)
    leftfn leftval .

def right fn (rightval)
  fn (leftfn rightfn)
    rightfn rightval .

Either constructors

There's only one value now, but two action functions! If the thing is right, call rightfn function, otherwise call leftfn. Now to actual functions processing these:

def isleft fn (either)
  either (fn _ true) (fn _ false) .

def leftval fn (either)
  either identity (fn _ nil) .

Left-related functions

The pattern repeats: we pass actions to data, not the other way around. But this time, there are multiple actions we pass. In this case, checking that the data is Left means passing a true-returning function as leftfn. And getting the left value is basically an identity leftfn to return whatever is stored there. Corresponding rightfn-s are obvious: return false/nil when Right.

Again, this simple example can be generalized to an arbitrary number of action functions. That's what Mogensen–Scott encoding is about. Store the data, get action functions, run the matching one, get the result.

Directions to More Complex Structures #

Now I'm too stupid for more complex data types. Luckily, Marvin Borner isn't. So go read his "Tiny, Untyped Monads" instead of a conclusion to this post. It's worth the read! I'll get to that too, and maybe I can steal some more of it into Lamber, my Lambda Calculus-compiling language.