Tagging a string with corresponding symbol

Question

I would like an easy way to create a String tagged with itself. Right now I can do something like:

data TagString :: Symbol -> * where
    Tag :: String -> TagString s
    deriving Show

tag :: KnownSymbol s => Proxy s -> TagString s
tag s = Tag (symbolVal s)

and use it like

tag (Proxy :: Proxy "blah")

But this is not nice because

• The guarantee about the tag is only provided by tag not by the GADT.
• Every time I want to create a value I have to provide a type signature, which gets unwieldy if the value is part of some bigger expression.

Is there any way to improve this, preferably going in the opposite direction, i.e. from String to Symbol? I would like to write Tag "blah" and have ghc infer the type TagString "blah".

GHC.TypeLits provides the someSymbolVal function which looks somewhat related but it produces a SomeSymbol, not a Symbol and I can quite grasp how to use it.

Answer 1

Is there any way to improve this, preferably going in the opposite direction, i.e. from String to Symbol?

There is no way to go directly from String to Symbol, because Haskell isn't dependently typed, unfortunately. You do have to write out a type annotation every time you want a new value and there isn't an existing tag with the desired symbol already around.

The guarantee about the tag is only provided by tag not by the GADT.

The following should work well (in fact, the same type can be found in the singletons package):

data SSym :: Symbol -> * where
    SSym :: KnownSymbol s => SSym s

-- defining values
sym1 = SSym :: SSym "foo"
sym2 = SSym :: SSym "bar"

This type essentially differs from Proxy only by having the KnownSymbol dictionary in the constructor. The dictionary lets us recover the string contained within even if the symbol is not known statically:

extractString :: SSym s -> String
extractString s@SSym = symbolVal s 

We pattern matched on SSym, thereby bringing into scope the implicit KnownSymbol dictionary. The same doesn't work with a mere Proxy:

extractString' :: forall (s :: Symbol). Proxy s -> String
extractString' p@Proxy = symbolVal p 
-- type error, we can't recover the string from anywhere

... it produces a SomeSymbol, not a Symbol and I can quite grasp how to use it.

SomeSymbol is like SSym except it hides the string it carries around so that it doesn't appear in the type. The string can be recovered by pattern matching on the constructor.

extractString'' :: SomeSymbol -> String
extractString'' (SomeSymbol proxy) = symbolVal proxy

It can be useful when you want to manipulate different symbols in bulk, for example you can put them in a list (which you can't do with different SSym-s, because their types differ).