[Haskell] Re: Infinite, open, statically constrained HLists

[oleg at pobox.com]

Chung-chieh Shan wrote:
> If that's correct, would it also be possible to switch to a lazy list
> at the type level?...  A new and possibly infinite HList would be
> defined by defunctionalizing type-level thunks.

An excellent suggestion! This way we obtain strongly typed
heterogeneous, potentially infinite streams -- aka type-level streams.
We can map and zip those streams as we do value-level lists. We can
indeed write something very similar to

	fib = 1 : 1 : zipWith (+) fib (tail fib)

We have to remember that while Haskell is non-strict at the value
level, it is strict at the type level.  We cannot write something like
	hfib = HCons (HSucc HZero) ... hfib

because that would lead to an infinite type. However, there are very
easy work-arounds. The type abstraction (higher-rank types) inherent in
typeclasses lets us break the recursion. Incidentally, no overlapping
instances are needed to realize such lazy hlists...

The trick is to introduce the notation for a not-yet-applied
type-level function:

> data Thunk f x = Thunk f x

We assume that there exists the corresponding instance "Apply f x r".
However, we do not assert such a constraint. The instance will be
looked up (and the result `r' of the application determined) only when
we actually need it. This trivial contraption introduces laziness at
the type level.

The full code is committed to the HList library:
	http://darcs.haskell.org/HList/Lazy.hs


What follows are a few notable fragments, including Fibonacci. We
assume HListPrelude. Our first stream is an infinite stream of zeros:

> data LZeros
> lzeros = Thunk (undefined::LZeros) ()
>
> instance Apply LZeros () (HCons HZero (Thunk LZeros ())) where
>     apply _ _ = HCons hZero lzeros

The value lzeros has _implicitly_ an infinite type: lzeros implicitly
depends on the instance "Apply LZeros", which, in turn, explicitly
depends on lzeros. This is quite akin to the ordinary Haskell
expression
	zeros = 0:zeros

We can print the desired prefix of the stream:

> tzeros = htake four lzeros

where four is a Peano numeral.

We can easily define the stream of natural numbers:

> data LNats
> lnats = Thunk (undefined::LNats)
>
> instance HNat n => Apply LNats n (HCons n (Thunk LNats (HSucc n))) where
>     apply _ n = HCons n (lnats (hSucc n))
>
> tnats = htake five . htail $ lnats hZero

The HList library already defines fold, map and other functions for
finite heterogeneous lists. We don't need to redefine them -- merely
extend to handle streams. We need to add instances to handle
Thunks. For example, when HMap comes across a lazy cell, it creates
another lazy cell with the promise of the HMap action.

> newtype HMapC f = HMapC f
>
> instance HMap f (Thunk g x) (Thunk (HMapC f) (Thunk g x)) where
>   hMap f x = Thunk (HMapC f) x
>
> instance (Force x l, HMap f l r) => Apply (HMapC f) x r where
>     apply (HMapC f) l = hMap f (force l)

The HMap instance above has no constraints -- this is what breaks the
recursion. The mapping over the result of the thunk is implicit.

Now we can create other infinite lists just by mapping over the
existing ones. For example, we obtain a stream of evens by doubling
the stream of naturals:

> data Twice = Twice
> instance Apply Add (n,n) r => Apply Twice n r
>
> levens = hMap Twice (lnats hZero)
> tevens = htake five levens

After we define the zipping of two streams, we can write our
Fibonacci sequence. Of course a more straightforward way was to follow
the approach of LNats: carry the state of the promise in the Thunk
itself. The more recursive way seems cooler however:

> data LFibs = LFibs
> lfibs = HCons hone (HCons hone (Thunk LFibs ()))

> lfibs' = hMap Add (lzip lfibs (htail lfibs))

> instance Apply LFibs () 
>     -- the latter type is the type of lfibs' as inferred bu GHCi
>     -- I simply did ":t lfibs'" and cut and pasted the result from
>     -- one Emacs buffer (GHCi prompt) to the other.
>     (HCons (HSucc (HSucc HZero))
>      (Thunk (HMapC Add)
>       (Thunk LZipC
>        (HCons (HSucc HZero) (Thunk LFibs ()), Thunk LFibs ()))))
>  where
>     apply _ _ = lfibs'

And indeed, tfibs defined as
> tfibs = htake seven lfibs

has the value:

HCons HSucc HZero
 (HCons HSucc HZero (HCons HSucc (HSucc HZero) 
  (HCons HSucc (HSucc (HSucc HZero)) 
   (HCons HSucc (HSucc (HSucc (HSucc (HSucc HZero))))
    (HCons HSucc (HSucc (HSucc (HSucc (HSucc (HSucc (HSucc (HSucc HZero)))))))
     (HCons HSucc (HSucc (HSucc (HSucc (HSucc (HSucc (HSucc (HSucc
        (HSucc (HSucc (HSucc (HSucc (HSucc HZero)))))))))))) HNil))))))

that is, the list of first seven Fibonacci numbers.