RE: "Green Card" for untyped lambda calculus?

Hi Elke,

| A possible (though probably unusual) characterization
| of list data structures is three functions
| 
| 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

For fans of the untyped lambda calculus, or for enthusiasts of
second order polymorphic lambda calculus, this characterization
of lists is not at all unusual.  But for those of us who spend
most of our time in the Hindley-Milner land, between those two
systems, it may well seem a little unusual.  If you're interested
in a technical understanding of the problems that occur here,
then you might find my old paper on "First-class Polymorphism
with Type Inference" (http://www.cse.ogi.edu/~mpj/pubs/fcp.html)
to be of interest.  It includes this representation of lists as
one example.  As Marcin has pointed out, you can code up these
examples in GHC and Hugs, providing you enable the right command
line settings.  (But beware that there are some differences in
syntax between the paper and the implementations.)

All the best,
Mark