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!
No, you cannot write such a function.
A function of type
Int -> NatSing n
says that it can transform any integer into a polymorphic NatSing. But there is no polymorphic NatSing.
What you seem to want here is to have n determined by the incoming Int. That'd be a dependent type:
(n :: Int) -> NatSing n
Such a thing isn't possible in Haskell. You'd have to use Agda or Idris or another dependently typed language. The hack with singletons is exactly Haskell's way to get around this. If you want to make a distinction based on a value, you have to lift the value to the type level, which is what NatSing is.
You could write a function that returns a NatSing for some n, by wrapping the n up in an existential type:
data ExNatSing where
ExNatSing :: NatSing n -> ExNatSing
But this wouldn't give you much benefit in practice. By wrapping the n up, you lose all information about it, and cannot make decisions based on it later.
By exactly the same argument, you can also not hope to define a function
list :: [a] -> List n a
The only approach you can use to save yourself some typing work is to define a type class that construct the NatSing value automatically:
class CNatSing (n :: Nat) where
natSing :: NatSing n
instance CNatSing Zero where
natSing = ZeroSing
instance CNatSing n => CNatSing (Succ n) where
natSing = SuccSing natSing
Then, you can say:
list :: CNatSing n => [a] -> List n a
list xs = list' xs natSing
where
list' :: [a] -> NatSing n -> List n a
list' = ... -- same as before, but still partial
Here, the type context you use this in makes GHC fill in the right NatSing. However, this function is still partial, because still the caller of the function can choose at what n to use this. If I want to use a [Int] of length 3 as a List (Succ Zero) Int it's going to crash.
Again, you could wrap this up in an existential instead:
data SomeList a where
SomeList :: NatSing n -> List n a -> SomeList a
Then you could write
list :: [a] -> SomeList a
list [] = SomeList ZeroSing Nil
list (x : xs) = case list xs of
SomeList n xs -> SomeList (SuccSing n) (x : xs')
Again, the benefit is small, but in contrast to ExNatSing, there at least is one: you now can temporarily unwrap a SomeList and pass it to functions that operate on a List n a, getting type-system guarantees on how the length of the list is transformed by these functions.