Apologies for the vague title, here's some context: http://themonadreader.files.wordpress.com/2013/08/issue221.pdf
The GADTs article in the above issue introduces a Nat type, and a NatSing type for use in various type-level list functions (concat, !!, head, repeat, etc). For a couple of these functions it's necessary to create type families for defining + and < on the Nat type.
data Nat = Zero | Succ Nat
data NatSing (n :: Nat) where
ZeroSing :: NatSing Zero
SuccSing :: NatSing n -> NatSing (Succ n)
data List (n :: Nat) a where
Nil :: List n a
Cons :: a -> List n a -> List (Succ n) a
Anyways, I have written a function "list" that converts an ordinary [a]
into a List n a
, for convenience to the caller. This requires the length of the list as input, much like repeat
(from the linked article):
list :: [a] -> NatSing n -> List n a
list [] ZeroSing = Nil
list (x:xs) (SuccSing n) = Cons x (list xs n)
list _ _ = error "length mismatch"
It would be nice to utilize a helper function toNatSing :: Int -> NatSing n
, so the above can be written as
list :: [a] -> List n a
list xs = list' xs (toNatSing $ length xs)
where
list' :: [a] -> NatSing n -> List n a
list' = ... -- same as before, but this time I simply "know" the function is no longer partial
Is it possible to write such a function toNatSing
? I've been wrestling with types and haven't come up with anything yet.
Thanks a lot!