Re: "Green Card" for untyped lambda calculus?

> nil     :: List a                  
> cons    :: a -> List a -> List a
> forlist :: b -> (a -> List a -> b) -> List a -> b
..
> The implementation I'm interested in (one without 
> constructors) is:
> 
> nil          fornil forcons    = fornil
> cons    x xs fornil forcons    = forcons x xs
> forlist      fornil forcons ls = ls fornil forcons
..
> As one might guess, this implementation relies on infinite
> types, which becomes obvious when offering for example
> 
> map f = forlist nil (\x xs -> cons (f x) (map f xs))

I have to admit that I misread your definitions at first, because they
are very similar to the representation of data structures as their own
folds. As your original question has been answered by now, it might be
interesting to have a look at this alternative. In the case of lists:

nil       c n   = n
cons x xs c n   = c x (xs c n)  -- pass c and n to xs
fold      c n l = l c n

The reversed order of the cons and nil replacements is just for
consistency with the standard fold, but note that the replacements get
passed down to the rest of the list in the definition of cons, ensuring
a consistent interpretation for all constructors in a given structure.
This gives you the obvious non-recursive

map f = fold (cons.f) nil

and all those other golden foldies

sum          = fold (+) 0
length       = fold (const (+1)) 0
append l1 l2 = fold cons l2 l1
..

Instead of an explicit recursion over an unknown structure, with
pattern-matching at each stage, these functions utilize the recursive
structure of the list parameter, and work uniformly on the whole list.

[This fold representation of lists just uses a parameterized variant of
 the successor function known from Church numerals. I seem to remember
 that Church himself used continuation-passing representations of data
 structures, but I don't have access to his presentation here:-( Could
 someone please confirm whether or not he used it for recursive
 structures (other than naturals) or only for pairs, products,
 conditionals and the like?]

To make things more visible, the following conversions are useful:

fromlist = foldr cons nil
tolist   = fold (:) []

Then you have, for instance

  Main> fromlist [1..4]
  <<function>>
  Main> tolist $ fromlist [1..4]
  [1,2,3,4]
  Main> tolist $ map (+1) $ fromlist [1..4]
  [2,3,4,5]

What I don't know is whether this representation is an option for you
or whether you need the "flat" pattern-matching. Your initial
definitions seem to correspond not to the standard lists but rather
to:

data L a b = N | C a b 

which doesn't fix the recursive structure and allows, among other
things, for heterogeneous lists and trees. You'll find it hard to
write some recursive functions even for this non-functional variant.

And if you fix (L a) to give you something equivalent to

data List a = N | C a (List a)

the flat functional representation is no longer the only possible
choice - it represents the "sums of products"-part, but leaves the
recursive structure unattended. The variant given above would take care
of that, but has other problems:

As mentioned, the variant that represents data structures as their own
folds corresponds -for lists- to Church numerals with parameterized
successor. Unfortunately, the predecessor for these numerals is known
to be slightly non-obvious, so the definition of tail for the
fold-style lists is left as an exercise to the reader;-)

If you absolutely need to operate on parts of your lists and want to
treat each cons individually, the modified definitions of the "flat",
pattern-matching-style representation given in other postings will be
more convenient but, where it is applicable, the whole-structure
approach supported by the "deep", fold-style representation is quite
attractive.

Claus