Subject: Polymorphic variants (extensible, recursive sums) with HList
Date: Monday 3rd July 2006 01:35:12 UTC (over 11 years ago)
The existing HList records support, without further programming, polymorphic variants: extensible recursive open sum datatypes, quite similar to Polymorphic variants of OCaml. HList thus solves the familiar (in OO, at least) `expression problem' -- an ability to add new variants to a datatype without changing the existing code. We should be able to extend old processing functions to deal with the extended data type, maximally reusing the old code. Furthermore, values of unextended data types should be processed by extended functions without any ado. http://darcs.haskell.org/HList/VariantP.hs Our implementation of polymorphic variants in terms of HList records uses no type classes, no type-level programming or any other type hacking. In fact, there are no type annotations, type declarations, or any other mentioning of types, except in the comments. Our example is patterned after the running example of the paper by Koji Kagawa,`Polymorphic Variants in Haskell' <http://guppy.eng.kagawa-u.ac.jp/~kagawa/PVH> which proposed quite different approach to the same problem. We start our example by `declaring' a list-like data type data List a = Nil | Cons a (List a) which we later extend with two more alternatives. In our example, we declare labels (for simplicity, of four models of labels, we use the simplest and the most ungainly) > l_nil = firstLabel > l_cons = nextLabel l_nil and define two constructrors: > nil consumer = consumer .!. l_nil > cons a l consumer = (consumer .!. l_cons) a (l consumer) and that is basically it. We can immediately build lists > tl2 c = cons 10 (cons 1 (cons 2 (cons 3 nil))) c and define list processing functions, e.g., to find the length of the list > lengthL () = l_nil .=. 0 > .*. l_cons .=. (\x a -> a + 1) > .*. emptyRecord > tekiyou consumer lst = lst (consumer ()) > test_lL2 = tekiyou lengthL tl2 Incidentally, the list tl2 is actually polymorphic over any numbers (Num). Now, we want to make our lists more efficient and so add to more alternatives to the List a data type, so it would now `read' data List a = Nil | Cons a (List a) | Unit a | App (List a) (List a) We only need to define two more labels, l_unit and l_app, and two constructors > unit a c = (c .!. l_unit) a > app l1 l2 c = (c .!. l_app) (l1 c) (l2 c) and we can build new lists > tl3 c = cons 1 (unit 2) c > tl4 c = cons 10 (app tl3 tl2) c by mixing old and new constructors. The code of the old constructors remains as it were. We can define a processing function over the extended lists: > sumA () = l_nil .=. 0 > .*. l_cons .=. (+) > .*. l_unit .=. id > .*. l_app .=. (+) > .*. emptyRecord and apply it to the extended list > test_sum2 = tekiyou sumA tl4 as well to the original, simple, unextended list: > test_sum1 = tekiyou sumA tl2 However, we can't pass extended lists tl3 and tl4 to a regular lenghtL. The type error message says that the field l_unit is missing But we can extend lengthL, reusing as much of previous functionality as possible > lengthA () = l_unit .=. const 1 > .*. l_app .=. (+) > .*. (lengthL ()) > > test_lL4 = tekiyou lengthA tl3 > test_lL5 = tekiyou lengthA tl4 The VariantP.hs file has more examples. An attentive reader has noticed that we took advantage of the fact that the deMorgan law NOT (A | B) -> (NOT A & NOT B) holds both in classical, and, more importantly, intuitionistic logics. Our encoding of sums is the straightforward Curry-Howard image of that law.