You only need lambda (and primitives for doing I/O). You can define numbers, lists, and all other data types using only lambda. For example you can define booleans like this:

    (define true (lambda (a b) a)
    (define false (lambda (a b) b)
    (define if (lambda (b a b) (b a b)))

Now you can do:

    (if true 4 9) -> returns 4

You can define logical `and` and `or` like this:

    (define and (lambda (p q) (if p q false)))
    (define or (lambda (p q) (if p true q)))

To make that work right for (if b (...) (...)) you'd need lazy evaluation though, otherwise both the then and else branch would always be evaluated regardless of whether the condition is true or false. Or you could wrap the then and else branch in a lambda, and then call the lambda that is returned by `if`.

- So booleans are the type forall r. r -> r -> r. "To use a boolean, you have to give it a value of type r for the then branch, and a value of type r for the else branch, and then you get a value of type r back".

- You can define natural numbers as functions of type forall r. r -> (r -> r) -> r. "To use a natural number, you should give a value of type r for n=0, and a function of type r -> r for n=k+1, then you get a value of type r back".

- You can define pairs of type (A,B) as forall r. (A -> B -> r) -> r. "To use a pair of type A,B you have to give a function that takes an A and a B and returns an r, then you get an r back".

- You can define sum types A+B (either an A or a B) as forall r. (A -> r) -> (B -> r) -> r.

- You can define least fix points (inductive types) of a type constructor F as forall r. (F r -> r) -> r.

- You can define greatest fix points (coinductive types) of a type constructor F as exists s. (s, s -> F s).

See also http://en.wikipedia.org/wiki/Church_encoding

Church encodings are a general way to define data types in lambda calculus purely based on lambdas. Church encodings are still not fully understood. For example the relation between Church encodings and mathematical induction is not fully understood yet (in type theory terms, the relation between non-dependent elimination / recursion principle and dependent elimination / induction principle). Also it's not yet fully understood how to take a fix point of a contravariant type constructor. Another thing that's as far as I know not fully understood is how to do Church encodings for higher inductive types. This goes to the very foundations of mathematics, and researchers in type theory think that in the coming years we will have breakthroughs that will make type theory a viable replacement for set theory as the basis of mathematics, with the benefit that mathematical proofs will be verified by computers.