Little help with length bounded lists

[Philip K.F. Hölzenspies]

Dear GHC-ers,

I'm trying to write a program using list-length codings in types.
Based on the material from the many "faking it" papers I've found, I
wrote up the following class, where 'l' is the list type, 'a' is the
type of the elements in the list and 'n' is the number of elements in
the list:


class BoundList l a n | l -> a n where
	asList  :: l -> [a]
	llength :: l -> n
	mkList  :: [a] -> (l,[a])


Now I made two obvious list-constructors WITH the corresponding type
constructors:


data Nil  a      = Nil
data Cons a n tl = Cons a tl


Empty lists are typed with the parameter of the type constructor.
Non-empty lists are typed, but by using only the definition above, the
list may be heterogeneous (there are no restrictions on tl). By making
these types instances of the BoundList class, lists are homogeneous
(see below). Lengths are coded linearly as:


data Z   -- zero
data S x -- successor


Giving the means to restrict the length of lists as well. The instance
declarations look like this:


instance BoundList (Nil a) a Z where
	asList  _    = []
	llength _    = (undefined :: Z)
	mkList  as   = (Nil, as)
instance BoundList l a n => BoundList (Cons a (S n) l) a (S n) where
	asList  (Cons a as) = a : asList as
	llength _           = (undefined :: S n)
	mkList  (a:as)      = (Cons a tl, rs)
                       where (tl,rs) = mkList as


Based on Uktaad B'mal's "Beginning Faking It" paper, I constructed
reflection and reification of the length coding, viz:


class Reflect s where
	intValue :: s -> Int
instance Reflect Z where
	intValue _ = 0
instance Reflect x => Reflect (S x) where
	intValue _ = intValue (undefined :: x) + 1

reifyInt :: Int -> (forall s . Reflect s => s -> w) -> w
reifyInt 0 k = k (undefined :: Z)
reifyInt (n+1) k = reifyInt n (\(_::s) -> k (undefined :: S s))


What I can't bend my mind around, is how I should construct a function
that will partition a normal list into a list of length bounded lists.
Basically, I want to have a function that, given an Int n and a list
list xs, that chops up xs into chunks of size n and actually
constructs Cons/Nil lists for me.

I understand that I can't "bring the type out," as in:

partition :: BoundList l a n => Int -> [a] -> l

but I would have hoped for a way to apply functions to my constructed
bounded lists, like, maybe:

partition :: Int -> [a] -> (forall l . BoundList l a n => l -> w) -> [w]

Like I said, my mind doesn't bend this way. Does anybody have a
suggestion that can help me out? Also, have I blatantly missed a
library that will neatly do this for me?

Eventually, I want to use this library so that I can define a block
size in my function types. This could (hopefully) be used to do
SDF-like run-time scheduling of threads, or - when distributed over
multiple processors - processes.

Regards,

Philip