FromList.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
module Main (main) where

import Data.Kind
import Data.List
import Data.Singletons.Prelude
import Data.Singletons.Prelude.List
import GHC.TypeLits
import System.Environment

data Vec :: Nat -> Type -> Type where
  Nil  :: Vec 0 a
  Cons :: a -> Vec n a -> Vec (1 + n) a
infixr 5 `Cons`

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

fromList :: SingKind a => Sing (list :: [a]) -> Vec (Length list) (Demote a)
fromList SNil         = Nil
fromList (SCons x xs) = Cons (fromSing x) (fromList xs)

main :: IO ()
main = do
  -- Statically known list
  print $ fromList (STrue `SCons` SFalse `SCons` SNil)
  -- Another way to do it
  withSomeSing [True, False] (print . fromList)

  -- It doesn't *need* to be statically known, though
  args <- getArgs
  let argLens :: [Integer]
      argLens = map genericLength args
  withSomeSing argLens (print . fromList)