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

[Chung-chieh Shan]

oleg at pobox.com wrote in article <20061026073838.7939FAC04 at Adric.metnet.fnmoc.navy.mil> in gmane.comp.lang.haskell.general:
> 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.

I understand this technique as switching (at the type level) from a
nested tuple to a function from natural numbers.  If that's correct,
would it also be possible to switch to a lazy list at the type level?
That is, one would revise the HList library to always "force"/"evaluate"
an HList type before matching it against HNil or HCons.

    class Force thunk result | thunk -> result where ...

A new and possibly infinite HList would be defined by defunctionalizing
type-level thunks.  Existing HLists would continue to work because we
can define "instance Force (HCons a b) (HCons a b)".

Just a thought...

-- 
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
Batman don't...but Kathmandu!