Using haskell's singletons, how can I write `fromList :: [a] -> Vec a n`?

Question

As part of my journey in understanding singletons I have tried to bridge the gap between compile time safety, and lifting runtime values into that dependent type safety.

I think though that a minimal example of "runtime" values is a function that takes an unbounded list, and converts it to a size-indexed vector. The following skeleton provides length-indexed vectors, but I can't quite determine how to write fromList.

I have considered making the function take a size parameter, but I suspect it's possible to keep that implicit.

{-# LANGUAGE GADTs                #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TemplateHaskell      #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE TypeInType           #-}
{-# LANGUAGE UndecidableInstances #-}

import           Data.Singletons
import           Data.Singletons.TH

$(singletons
  [d|
    data Nat = Z | S Nat deriving (Show)
  |])

data Vec a n where
  Nil :: Vec a Z
  Cons :: a -> Vec a n -> Vec a (S n)

instance Show a => Show (Vec a n) where
  show Nil = "Nil"
  show (Cons x xs) = show x ++ " :< " ++ show xs

fromListExplicit :: forall (n :: Nat) a. SNat n -> [a] -> Vec a n
fromListExplicit SZ _ = Nil
fromListExplicit (SS n) (x : xs) = Cons x (fromListExplicit n xs)

ex1 = fromListExplicit (SS (SS (SS SZ))) [1..99]
-- 1 :< 2 :< 3 :< Nil

fromListImplicit :: (?????) => [a] -> Vec a n
fromListImplicit = ?????

main :: IO ()
main = do
  xs <- readLn :: IO [Int]
  print $ fromListImplicit xs

Answer 1

This is not possible using Haskell because Haskell does not yet have full dependent types (although GHC might in the future). Notice that

fromList :: [a] -> Vec a n

Has both a and n quantified universally, which means that the user should be able to pick their n and get back a Vec of the right size. That makes no sense! The trick is that n is not really for the user to choose - it has to be the length of the input list. (For the same reason, fromList :: Integer -> [a] -> Vec a n would not be any more useful - the size hint has to be something type-level.)

Looking to a dependently typed language like Idris, you can define

fromList : (l : List elem) -> Vec (length l) elem

And in fact they define this in the standard library.

So, what can you do? Short of saying that Vec has the length equal to the size of the input list (which requires lifting "length of the input list" to the type level), you can say it has some length.

data SomeVec a where { SomeVec :: Vec a n -> SomeVec a }

list2SomeVec :: [a] -> SomeVec a
list2SomeVec [] = SomeVec Nil
list2SomeVec (x:xs) = case list2SomeVec xs of
                        SomeVec ys -> SomeVec (x `Cons` ys)

That isn't spectacularly useful, but it is better than nothing.

Answer 2

You can do this with an existentially quantified type variable, as in @Alec’s answer, or equivalently by rewriting in continuation-passing style. The trick is to give fromList a continuation (function) that’s polymorphic in the size of the Vec; then, within the continuation, you have access to a type variable representing the size:

data Vec n a where
  Nil :: Vec Z a
  Cons :: a -> Vec n a -> Vec (S n) a

deriving instance (Show a) => Show (Vec n a)

fromList :: [a] -> (forall n. Vec n a -> r) -> r
fromList [] k = k Nil
fromList (x : xs) k = fromList xs $ \ xs' -> k (Cons x xs')

-- fromList [1, 2, 3] show == "Cons 1 (Cons 2 (Cons 3 Nil))"

You can’t know the actual value of n, because it’s not available at compile time.

If you replace your Nat with the one from GHC.TypeLits, I think you can get a KnownNat constraint for n by creating a SomeNat from the runtime length using fromJust (someNatVal (fromIntegral (length xs))), then get back the actual length value at runtime with natVal. I’m not really familiar with how to do it, and it might require the ghc-typelits-natnormalise plugin, but it might be a starting point.