You can change R3RS Scheme a little to get a language whose types are all functions that defines cons in the same way as in the lambda calculus, but passing aro

You can change R3RS Scheme a little to get a language whose types are all functions that defines cons in the same way as in the lambda calculus, but passing around symbols to describe types: (define cons (lambda (car cdr) (lambda (z) (z 'pair car cdr)))) (define car (lambda (pair) (pair (lambda (type car cdr) car)))) ; we don't actually check type correctness in this simple example (define cdr (lambda (pair) (pair (lambda (type car cdr) cdr)))) (define type-of (lambda (x) (x (lambda (type . rest) type)))) (define pair? (lambda (x) (eqv? 'pair (type-of x)))) Similar techniques can be used to code Booleans, nil, &c. Symbols in turn can be lifted out to be functions, whose type "symbol" is some particular function, say identity: here we need to have an atomic operation to define whether two functions are realised using the same closure, which is the usual meaning of eqv?. While Scheme has mutable structures (e.g., set-car!) and circular structures, this alternate language would not. Note that the Haskell 98 standard does not require implementations to let circular structures be defined, ghc does allow them (e.g., ones = 1:ones is a circular structure in ghc, but Haskell 98 would allow a Haskell to implement it as an infinite list).