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>
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
Marcin 'Qrczak' Kowalczyk wrote: | 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 : | In ghc algebraic types are really implemented in a similar way :-) Well, not really. This implementation does not give you sharing between lists. Everytime you use "forlist", the list is reevaluated. In GHC, this does not happen of course. Regards, Koen. -- Koen Claessen http://www.cs.chalmers.se/~koen phone:+46-31-772 5424 mailto:koen@cs.chalmers.se ----------------------------------------------------- Chalmers University of Technology, Gothenburg, Sweden
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
participants (4)
-
Elke Kasimir -
Koen Claessen -
Mark P Jones -
qrczak＠knm.org.pl