Can you Church-encode a stream?

Is it possible to church-encode potentially infinite data structures using simply typed lambda calculus? The answer to this question would seem to be yes.

Simply typed lambda calculus

STLC is a form of typed lambda calculus that only has a type constructor for functions.

We also allow use of variables to represent "some function, to be filled in".

STLC cannot construct recursive expressions, eg. (λx. f (x x)) (λx. f (x x)) is not a valid expression.

Church encodings

Church encodings is a means of encoding datatypes using functions.

The trick is to take the constructors and construct the term requiring that those constructors are present. Lets take few examples of church encodings to illustrate this method.

Here's booleans:

true : bool
false : bool

bool = c → c → c

Here's maybe:

just : a → maybe a
nothing : maybe a

maybe a = (a → c) → c → c

Here's natural numbers:

zero : nat
succ : nat -> nat

nat = c → (c → c) → c

Here's pairs:

cons : a → b → pair a b

pair a b = (a → b → c) → c

Here's lists:

empty : list a
cons : a → list a → list a

list a = c → (a → c → c) → c

The function that represents the datatype works as an eliminator.

A stream?

Stream is a potentially infinite list. So can you Church encode these?

Lets try:

cons : a → stream a → stream a

stream a = (a → c → c) → c

Well.. You can contruct the type but you cannot construct any terms because you can't construct recursive expressions with STLC.

For example, this counter would not typecheck.

counter : nat → stream nat
counter n = λcons.cons n (counter (n+1))

Church encoding by rewriting constructors don't seem to work.

Flipping the role of constructor/eliminator

You got constructors and eliminators in any type you construct. Instead of starting Church-encoding from constructors, we could also try to rewrite eliminators.

uncons : stream a → pair a (stream a)

stream a c = d → (d → pair a d) → c

I had to adjust the rewriting a bit because now we get a value to eliminate into this structure as well. You also need to add a variable to represent things you get out.

What used to be an eliminator ends up being a constructor.

counter : nat → (stream nat c → c)
counter n f = f n (λk. cons k (k+1))

Give a constructor to eliminate the counter:

take : nat → stream nat (list nat)
take num = λinit.λuncons.
    num (λempty.λcons.λstream.empty)
        (λseq.uncons.λstream.stream (λi.λstream'.cons i (seq stream')))
        init

Now if you write counter (take 4), it ought retrieve 4 values from the stream and put them into a list.

I'm not sure if the take -program typechecks but I guess the approach is correct here. Flip the role of eliminator and constructor to church-encode infinite but otherwise well-formed constructs.

Lol

The church-encoding of "co-data-types" is likely something well-known by now. With a quick search I found a paper "The Church-Scott representation of inductive and coinductive data" by Herman Geuvers.

Update 2020-07-28: Somebody posted Mike Gordon's text "Corecursion and coinduction: what they are and how they relate to recursion and induction [pdf]" to r/programming. It seems to be a fairly nice text about the subject so I included it here.

Mike would write our counter like this:

uncons (CountFrom n) = (n, CountFrom (n+1))

Similar posts