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.