Little help with length bounded lists
Philip K.F. Hölzenspies
p.k.f.holzenspies at utwente.nl
Tue Oct 23 07:10:04 EDT 2007
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
More information about the Glasgow-haskell-users
mailing list