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,
(λx. f (x x)) (λx. f (x x)) is not a valid expression.
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.
true : bool
false : bool
bool = c → c → c
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
cons : a → b → pair a b
pair a b = (a → b → c) → c
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.
Stream is a potentially infinite list. So can you Church encode these?
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.
(λseq.uncons.λstream.stream (λi.λstream'.cons i (seq stream')))
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.
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))