From oleg-at-okmij.org Sun Jul  2 18:35:12 2006
To: haskell@haskell.org
Subject: Polymorphic variants (extensible, recursive sums) with HList
From: oleg-at-pobox.com
Message-ID: <20060703013512.D19C9AC97@Adric.metnet.fnmoc.navy.mil>
Date: Sun,  2 Jul 2006 18:35:12 -0700 (PDT)
Status: OR


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://okmij.org/ftp/Haskell/generics.html#PolyVariant

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.