"Green Card" for untyped lambda calculus?

[Elke Kasimir]

This message is in MIME format
--_=XFMail.1.3.p0.Linux:001128191714:327=_
Content-Type: text/plain; charset=iso-8859-1

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@catmint.de>  
see: <http://www.catmint.de/elke>

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

--_=XFMail.1.3.p0.Linux:001128191714:327=_
Content-Disposition: attachment; filename="Lis.hs"
Content-Transfer-Encoding: base64
Content-Description: Lis.hs
Content-Type: application/octet-stream; name=Lis.hs; SizeOnDisk=1875

bW9kdWxlIExpcyAgCndoZXJlCgppbmZpeHIgYGNvbnMnYAppbmZpeHIgYGNvbnMnJ2AKaW5maXhy
IGBjb25zJycnYAoKLS0gYmFzaWMgaW1wbGVtZW50YXRpb246Cgpmb3JsaXN0ICAgICAgZm5pbCBm
Y29ucyBscyAgPSBscyBmbmlsIGZjb25zCmNvbnMgICAgeCB4cyBmbmlsIGZjb25zICAgICA9IGZj
b25zIHggeHMKbmlsICAgICAgICAgIGZuaWwgZmNvbnMgICAgID0gZm5pbAoKCnstICJtb3N0IGdl
bmVyYWwgdHlwZSIgdmVyc2lvbjogCi19CmZvcmxpc3QnID0gZm9ybGlzdApjb25zJyAgICA9IGNv
bnMKbmlsJyAgICAgPSBuaWwKCi0tIHBhc3NlczoKdGFpbCcgICAgICA9IGZvcmxpc3QnIHVuZGVm
aW5lZCAoXHggeHMgLT4geHMpCgotLSBkb2Vzbid0IHBhc3M6Ci0tIG1hcCcgZiAgICAgPSBmb3Js
aXN0JyBuaWwnIChceCB4cyAtPiBmIHggYGNvbnMnYCBtYXAnIGYgeHMpCgoKey0gdHlwZWQgdmVy
c2lvbiB3aXRoIHR3byB0eXBlIHZhcmlhYmxlczogCiAgIHRoZSBmaXJzdCBiZWluZyB0aGUgbGlz
dCBlbGVtZW50IHR5cGUsCiAgIHRoZSBzZWNvbmQgYmVpbmcgdGhlIHJlc3VsdCB0eXBlIG9mIHRo
ZSBmdW5jdGlvbiB0aGF0IGlzIAogICBjb25zdHJ1Y3RlZCB3aXRoIGZvcmxpc3QuCiAgIEVuZm9y
Y2VzIGxzIGFuZCAodGFpbCBscykgdG8gaGF2ZSB0aGUgc2FtZSB0eXBlOgotfQpuZXd0eXBlIExp
c3QnJyBhIGIgPSBMJycgKGIgLT4gKGEgLT4gTGlzdCcnIGEgYiAtPiBiKSAtPiBiKSAKCmZvcmxp
c3QnJyBmbmlsIGZjb25zIChMJycgbHMpID0gZm9ybGlzdCBmbmlsIGZjb25zIGxzCm5pbCcnICAg
ICAgICAgICAgICAgICAgICAgICAgID0gTCcnIG5pbApjb25zJycgeCB4cyAgICAgICAgICAgICAg
ICAgICA9IEwnJyAkIGNvbnMgeCB4cwoKLS0gcGFzc2VzOgptYXAnJyBmICA9IGZvcmxpc3QnJyBu
aWwnJyAoXHggeHMgLT4gZiB4IGBjb25zJydgIG1hcCcnIGYgeHMpIAoKLS0gZG9lc24ndCBwYXNz
OgotLSB0YWlsJycgPSBmb3JsaXN0JycgdW5kZWZpbmVkIChceCB4cyAtPiB4cykKCi0tIHBhc3Nl
cyBhdCB0aGUgY29zdCBvZiBjb3B5aW5nIHRoZSB3aG9sZSByZXN1bHQ6CnJlcGFpcmVkX3RhaWwn
JyA9IGZvcmxpc3QnJyB1bmRlZmluZWQgKFx4IHhzIC0+IG1hcCcnIGlkIHhzKQoJCQoKey0gdHlw
ZWQgdmVyc2lvbiB3aXRoIHRocmVlIHR5cGUgdmFyaWFibGVzOiAKICAgdGhlIGZpcnN0IGJlaW5n
IGxpc3QgZWxlbWVudCB0eXBlLAogICB0aGUgc2Vjb25kIGJlaW5nIHRoZSByZXN1bHQgdHlwZSBv
ZiB0aGUgZnVuY3Rpb24gd2hpY2ggaXMgY29uc3RydWN0ZWQgd2l0aCBmb3JsaXN0LAogICB0aGUg
dGhpcmQgYmVpbmcgdGhlIHJlc3VsdCB0eXBlIG9mIHRoZSBmdW5jdGlvbiB3aGljaCBjb25zdW1l
cyB0aGUgbGlzdC4KICAgRW5mb3JjZXMgKHRhaWwgbHMpIGFuZCAodGFpbCAodGFpbCBscykpIHRv
IGhhdmUgdGhlIHNhbWUgdHlwZToKLX0KbmV3dHlwZSBMaXN0JycnIGEgYiBjID0gTCcnJyAoYiAt
PiAoYSAtPiBMaXN0JycnIGEgYyBjIC0+IGIpIC0+IGIpIAoKZm9ybGlzdCcnJyBmbmlsIGZjb25z
IChMJycnIGxzKSA9IGZvcmxpc3QgZm5pbCBmY29ucyBscwpuaWwnJycgICAgICAgICAgICAgICAg
ICAgICAgID0gTCcnJyBuaWwKY29ucycnJyB4IHhzICAgICAgICAgICAgICAgICA9IEwnJycgJCBj
b25zIHggeHMKCi0tIHBhc3NlcyBhZ2FpbjoKbWFwJycnIGYgID0gZm9ybGlzdCcnJyBuaWwnJycg
KFx4IHhzIC0+IGYgeCBgY29ucycnJ2AgbWFwJycnIGYgeHMpIAoKLS0gbm93IHBhc3NlczoKdGFp
bCcnJyA9IGZvcmxpc3QnJycgdW5kZWZpbmVkIChceCB4cyAtPiB4cykKCi0tIGRvZXNuJ3QgcGFz
czoKLS0gdGFpbHRhaWwnJycgbHMgPSB0YWlsJycnICh0YWlsJycnIGxzKQoKCgoKCgoK

--_=XFMail.1.3.p0.Linux:001128191714:327=_--
End of MIME message