"Green Card" for untyped lambda calculus?

I'm concerned with the following problem:

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

for which

forlist fornil forcons nil         = fornil
forlist fornil forcons (cons x xs) = forcons x xs

holds, that is, 'forlist' is a kind of case with 
pattern matching for lists. The straightforward 
implementation with buildt-in lists is

nil = []
cons = (:)
forlist fornil forcons []     = fornil
forlist fornil forcons (x:xs) = forcons x xs

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))

to the Haskell type checker.

I have made two other attempts to fit my implementation
in the haskell type system, without finding a usable
solution (see attachment).

(By the way, the map definition above can be easily optimized to:
map f ls fnil fcons = ls fnil (\x xs -> fcons (f x) (map f xs))
via straight inlining plus one optimization rule, which allows
for even more inlining if the consumer (fnil,fcons) is known.)

Has anyone an idea of how to express my lists in haskell
or some haskell type system extension?

Just a thought... Would it be possible for a Haskell Compiler/
Interpreter to provide a "Green Card" for untyped lambda
calculus...?

Elke.






---
Elke Kasimir
Skalitzer Str. 79
10997 Berlin (Germany)
fon:  +49 (030) 612 852 16
mail: elke.kasimir@xxxxxxxxxx>  
see: <http://www.catmint.de/elke>

for pgp public key see:
<http://www.catmint.de/elke/pgp_signature.html>

Lis.hs
Description: Lis.hs