While learning about singletons and (semi) dependent typing, I started trying to make a sized list from a normal Haskell list with sizes given by Nats such as 0, 1, 2, 3,... instead of Z, S Z, S (S Z), etc.. I'm using the Data.Singletons.TypeLits library btw. (singletons-2.5.1).
This is the way I've been trying to do it:
data NatList (a :: *) (n :: Nat) where
Nah :: NatList a 0
Yea :: a -> NatList a n -> NatList a (n + 1)
fromList :: SNat n -> [a] -> NatList a n
fromList s [] = Nah
fromList s (x:xs) = Yea x (fromList (s %- (SNat :: SNat 1)) xs)
This code doesn't compile and gives me an error
"Couldn't match type ‘n’ with ‘0’ ‘n’ is a rigid type variable bound by the type signature for: fromList :: forall (n :: Nat) a. SNat n -> [a] -> NatList a n
After some time away from the problem I came back and found a solution that works for me: use an existential wrapper for the sized list type and convert the runtime list to that.
data SizedList (a :: *) (n :: Nat) where
Nil :: SizedList a 0
Cons :: a -> SizedList a n -> SizedList a (n+1)
data SomeSL (a :: *) where
MkSomeSL :: KnownNat n => SNat n -> SizedList a n -> SomeSL a
toList :: SizedList a n -> [a]
toList Nil = []
toList (Cons x xs) = x : toList xs
fromList :: [a] -> SomeSL a
fromList [] = MkSomeSL (SNat @0) Nil
fromList (x:xs) = case (fromList xs) of
MkSomeSL n ys -> MkSomeSL (n %+ SNat @1) (Cons x ys)
toList_ :: SomeSL a -> [a]
toList_ (MkSomeSL _ xs) = toList xs
Here, SomeSL wraps the SizedList type from my question along with a singleton nat, allowing functions to access the length through the SNat n.
Justin Le's series of blog posts about singletons was very helpful: https://blog.jle.im/entry/introduction-to-singletons-1.html