Converting a list ([a]) to a type-level length-indexed list

Viewed 63

I'm fairly inexperienced with Haskell, but essentially I've started working with DataKinds and GADTs. I have a GADT which represents a list that "knows" its length:

data NSL :: N -> * -> * where
Null :: NSL 'Zero a
More :: a -> NSL n a -> NSL ('Incr n) a

which is created from the natural data representation

data N :: * where
    Zero :: N
    Incr :: N -> N

So my question is, how do I create a function

fromList :: [a] -> NSL n a

I've tried working with Foldable and similar ideas, but I can't quite wrap my head around it.

0 Answers
Related