Can one make a sized list using singleton Nats (like 0, 1, ...) from Lists in Haskell?

Question

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

I don't think this is possible without a Maybe or something like that in the result type. This function claims to make a list of a fixed size, known at a type level, out of a list of an unknown size. There is no type level information about the size of the [a] list. What should happen if you call like this fromList (sing :: Sing 3) [1]? — David Young
Your function is sound in principle (as @DavidYoung notes, it is a partial function, but this is easy enough to fix). The problem is you can't perform induction on type level nats in this way - you have to use inductive naturals (i.e. promoted version of data Nat = Z | S Nat. — user2407038

BBMBR BBMBR · Accepted Answer · 2019-07-04T14:27:29

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

Can one make a sized list using singleton Nats (like 0, 1, ...) from Lists in Haskell?

3 Answers