Convert list of type levels to value

Question

The GHC.TypeLits module currently provides natVal and symbolVal , which allow you to get the runtime value from a type of type Nat or Symbol . Is there a way to get the runtime value of type [String] from type type '[Symbol] ? I do not see an obvious way to do this. I can come up with one that uses the typeclass class with OverlappingInstances , but it looks like GHC already has a function for this.

Answer 1

symbolVal can be mapped to type level lists. For this we need ScopedTypeVariables and PolyKinds in addition to DataKinds and TypeOperators .

 {-# LANGUAGE DataKinds #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE PolyKinds #-} import Data.Proxy import GHC.TypeLits 

We will define a class of types (of any type) for which we can "get the runtime value of type [String] ".

 class SymbolVals a where symbolVals :: proxy a -> [String] 

We can get a list of strings for any empty list of types.

 instance SymbolVals '[] where symbolVals _ = [] 

We can get a list of strings for any type list, where we can get a string for the first type and a list of strings for the remainder.

 instance (KnownSymbol h, SymbolVals t) => SymbolVals (h ': t) where symbolVals _ = symbolVal (Proxy :: Proxy h) : symbolVals (Proxy :: Proxy t) 

Answer 2

I suggest using the singletons library. You have everything you need, but using Sing instead of Proxy type:

 $ stack ghci --package singletons Configuring GHCi with the following packages: GHCi, version 8.0.1: http://www.haskell.org/ghc/ :? for help Prelude> :set -XDataKinds Prelude> import Data.Singletons.Prelude Prelude Data.Singletons.Prelude> fromSing (sing :: Sing '["a","b"]) ["a","b"] Prelude Data.Singletons.Prelude> :t fromSing (sing :: Sing '["a","b"]) fromSing (sing :: Sing '["a","b"]) :: [String]