[Haskell] Infinite, open, statically constrained HLists

[oleg at pobox.com]

We show a presentation of heterogeneous sequences that admits infinite
sequences and permits post-hoc addition of new elements, even to an
already infinite sequence. We can also assert static constraints,
e.g., the sequence must be made of non-decreasing Peano numerals. Our
sequences permit all the common operations such as `head', `tail',
`cons', `map', `take' and `fold'. It is a type error to attempt to
take `head' of an empty sequence. Any finite sequence is
inter-convertible with the HCons-based HList.

The full code is available at
	http://darcs.haskell.org/HList/CHList.hs

The presentation is inspired by the problem posed by Greg Buchholz on
the following thread:

  http://www.haskell.org/pipermail/haskell-cafe/2006-October/018948.html
  http://www.haskell.org/pipermail/haskell-cafe/2006-October/019030.html

He observed how easy it is to define _some_ (potentially) infinite
heterogeneous data structures. For example,

	data SeqI a = ConsI a (SeqI (S a)) | NilI

defines the type of a sub-sequence of the sequence of natural Peano
numerals. We can construct finite 
	seqi1 = ConsI Z (ConsI (S Z) NilI)
and even infinite sequences
	seqi_inf :: n -> SeqI n
	seqi_inf n = ConsI n (seqi_inf (S n))
but not
	seqi2 = ConsI Z (ConsI Z NilI)
The latter ill-formed sequence is ill-typed. However, it is difficult
to generalize these constructions, for example, to the sequences of
Fibonacci Peano numerals or to the sequences of non-decreasing Peano
numerals.

The HList presentation, with familiar "HCons a b" and "HNil" types,
makes it straightforward to define sequences with arbitrary
constraints on the adjacent elements. The structure of such HList
values is reflected in their types, and so we can statically constrain
them. Alas, the type of an HList has as many HCons type constructors as
there are HCons data constructors. That seems to rule out infinite
sequences.

There is a trivial way out of this predicament, via a different
presentation. A sequence is a partial function from a range of natural
numbers. In other words, a sequence is a mapping from a Natural number
to {HNothing, HJust a}. We consider the HNothing element with the
smallest index to be the end of the sequence. This obvious idea leads
to the straightforward implementation:

> class Nat n => CHList l n r | l n -> r where
>     chel :: l -> n -> r
>     chel = undefined
>
> -- Default `cut-off' instance
> instance (Nat n, TypeCast r HNothing) => CHList l n r

where

> data HNothing = HNothing
> newtype HJust x = HJust x
> fromHJust (HJust x) = x		-- this is the total function!

The class 'CHList l n r' establishes the n-th element of the sequence
named 'l' to be 'r'. The empty sequence is defined then by the single
declaration:

> data LEmpty = LEmpty

Here is a bit more elaborate sequence, of two elements. Both are
Ints. Homogeneous sequences are just a subset of heterogenous ones.

> data L1 = L1
> instance CHList L1 Z (HJust Int) where
>     chel _ _ = HJust 0
> instance CHList L1 (S Z) (HJust Int) where
>     chel _ _ = HJust 1

We can convert such sequences to the regular HList; this is quite
handy for showing them. For example, 

> test1 = show $ chl_to_hl L1

yields "HCons 0 (HCons 1 HNil)"

Not surprisingly, we can implement all of the common List API, for
example,

> cl_head l = fromHJust (chel l Z)

It will be a type error attempting to apply cl_head to an empty
sequence. We can define tail

> newtype CLTail l = CLTail l
> instance (Nat n, CHList l (S n) r) => CHList (CLTail l) n r where
>     chel (CLTail l) n = chel l (S n)
>
> -- ensure the list to take the tail of is non-empty
> cl_tail :: CHList l Z (HJust e) => l -> CLTail l
> cl_tail l = CLTail l
>
> test_h3 = cl_head (cl_tail L1) -- 1

and cons

> data CLCons a l = CLCons a l
> cl_cons = CLCons
>
> instance CHList (CLCons a l) Z (HJust a) where
>     chel (CLCons x _ ) _ = HJust x
>
> instance (Nat n, CHList l n r) => CHList (CLCons a l) (S n) r where
>     chel (CLCons _ l) (S n) = chel l n

after which we can introduce and extend our sequences in the `normal'
way:

> test_c1 = cl_head (cl_tail (cl_cons ((-2)::Int) (cl_cons ((-1)::Int) L1)))
> test_c2 = cl_head (cl_tail (cl_cons () (cl_cons True LEmpty)))
> test_c3 = show $ chl_to_hl $ cl_cons () L1

Defining other functions like `take', `map' and `fold' is
straightforward and elided. The latter require the generalized `Apply'
class defined in the HList library. We can write, for example,

> test_m1 = cl_map (succ :: Int->Int) L1
> test_m2 = show $ chl_to_hl test_m1

because regular functions are already instances of the Apply class and
so apply-able. It is worth noting a close resemblance between test_m1
above and

> test_m1' = map (succ :: Int->Int) l1
>     where l1 = [0,1]

The difference seems to be in the case of the identifier: `l1' vs
`L1'. Indeed, both l1 and L1 _denote_ certain values. The rules of
looking up the value given the name are implicit in the case of l1 and
explicit (and defined by us) in the case of L1. The type-checking is
more explicit in the latter case too -- that's why we are able to
assert more constraints, as we shall see soon.

It goes without saying that our sequences can as well be infinite:

> data LNats = LNats  -- lists of successive numerals
> instance Nat n => CHList LNats n (HJust n) where
>     chel _ n = HJust n

which defines the infinite list of Peano numerals. That is quite akin
to "seqi_inf Z", described in the beginning of this message. Now,
however, we can introduce other infinite sequences, e.g., by mapping
arbitrary function over LNats. We can also define sequences by
recursion, e.g., LFibs.

Perhaps more interesting is the fact that our lists are open, even
when they are extensible. For example, if we define only

> data LCyc = LCyc
> instance (Nat n, CHList LCyc n r) => CHList LCyc (S (S n)) r where
>     chel l (S (S n)) = chel l n

then

> test_cyc = show $ chl_to_hl $ cl_take five LCyc

yields "HNil". If we later add another instance

> instance CHList LCyc Z (HJust ()) where chel _ _ = HJust ()

the same test_cyc will give "HCons () HNil". The addition the third
instance

> instance CHList LCyc (S Z) (HJust Bool) where chel _ _ = HJust True

makes our list infinite. test_cyc now gives
  "HCons () (HCons True (HCons () (HCons True (HCons () HNil))))"

We may still add instances, for example

> instance CHList LCyc (S (S Z)) (HJust Bool) where chel _ _ = HJust False

causes test_cyc to return
 "HCons () (HCons True (HCons False (HCons True (HCons False HNil))))"


Finally, we show constrained lists. A constraint is a binary
predicate; it is apply-ed to two consecutive elements of the
sequence, and must return HTrue. For simplicity, we introduce the
following non-generic class of constrained lists, whose elements must
be non-decreasing numerals:

> data CK l = CK l
> class (Nat n, Apply (CK l) (n,r) HTrue) => C1 l n r | l n -> r where
>     chel1 :: l -> n -> r; chel1 = undefined
> instance (Nat n, TypeCast r HNothing, Apply (CK l) (n, r) HTrue) => C1 l n r
>
> instance Apply (CK l) (Z,r) HTrue
> instance Apply (CK l) (S n,HNothing) HTrue
> instance (C1 l n (HJust ep), Apply PLEQ (ep,e) r) 
>     => Apply (CK l) (S n,HJust e) r

The constraint is specified as a class constraint; therefore, all
instances of C1 must obey it. All instances of C1 are CHLists,
after we say

> newtype C1toCL cl = C1toCL cl
> instance C1 cl n r => CHList (C1toCL cl) n r where
>     chel (C1toCL l) n = chel1 l n

We introduce

> data LC1 = LC1
> instance C1 LC1 Z (HJust Z)
> instance C1 LC1 (S Z) (HJust Z)
> instance C1 LC1 (S (S Z)) (HJust (S (S (S Z))))
> test_cl1 = show $ chl_to_hl $ C1toCL LC1

but we cannot add the instance
	instance C1 LC1 (S (S (S Z))) (HJust Z)
because it fails the non-decreasing constraint. The constrained list
may be infinite:

> data LC2 = LC2
> instance C1 LC2 Z (HJust Z)
>           -- this constraint suggested by the typechecker
> instance (Apply PLEQ (r, S (S r)) HTrue, 
> 	  C1 LC2 n (HJust r))
>     => C1 LC2 (S n) (HJust (S (S r)))
>
> test_cl2 = show $ chl_to_hl $ cl_take five $ C1toCL LC2

We check the constraint by applying the predicate to the current and
the previous element of the sequence (if it exists). Even in case of
the infinite sequence, the prefix is finite, so our constraint is
effectively verifiable.