5

The module GHC.TypeLits currently provides natVal and symbolVal, which allow us to get a runtime value from a type of kind Nat or Symbol. Is there a way to get a runtime value of type [String] out of a type of kind '[Symbol]? I can't see an obvious way to do this. I can think of one that uses a typeclass with OverlappingInstances, but it seems like GHC should already have a function for this.

2
  • Are you interested in something like forall (xs :: [Symbol]) -> HList xs -> [String] or forall (xs :: [Symbol]) -> Proxy xs -> [String]. The former is simple, the latter is slightly less simple (you'll need a type class constraint on xs). Feb 23, 2015 at 4:05
  • I'm looking for the latter. Although I'd be intrigued to see how the former is done as well (but it seems to me that kind HList (xs :: '[Symbol]) is more like a list of lists). Also, I've never seen the forall used quite like that. Isn't there supposed to be a period after the thing it quantifies? Feb 23, 2015 at 12:06

2 Answers 2

6

symbolVal can be mapped onto type level lists. To do so we'll 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'll defined the class of types (of any kind) for which we can "get a 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 list of types 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)
1
  • Ah, very good. I forgot that this wouldn't be a scenario that required OverlappingInstances because the types '[] and (h ': t) don't overlap. Thanks. Feb 23, 2015 at 19:40
2

I suggest to use singletons library. You have all that 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]

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.