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