"Green Card" for untyped lambda calculus?

[Marcin 'Qrczak' Kowalczyk]

Tue, 28 Nov 2000 19:17:32 +0100 (CET), Elke Kasimir <elke.kasimir@catmint.de> pisze:

> 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

It can be implemented in extended Haskell with local universal
quantification (ghc -fglasgow-exts, hugs -98):

newtype List a = List (forall b. b -> (a -> List a -> b) -> b)

nil          = List (\fornil forcons -> fornil)
cons    x xs = List (\fornil forcons -> forcons x xs)
forlist      fornil forcons (List ls) = ls fornil forcons

map f = forlist nil (\x xs -> cons (f x) (map f xs))

In ghc algebraic types are really implemented in a similar way :-)
Pattern matching jumps into the value, giving to it an array of
continuations for each constructor. The value evaluates itself
and enters the chosen continuation.

It should be also directly implentable in OCaml with -rectypes flag
which turns off occurs check for types.

-- 
 __("<  Marcin Kowalczyk * qrczak@knm.org.pl http://qrczak.ids.net.pl/
 \__/
  ^^                      SYGNATURA ZASTĘPCZA
QRCZAK