用相应的符号标记字符串

Question

我想要一种简单的方法来创建带有自身标签的String。现在我可以 做类似的事情：

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

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

并像使用它

tag (Proxy :: Proxy "blah")

但这并不好，因为

• 关于标签的保证仅由tag 提供，GADT 不提供。
• 每次我想创建一个值时，我都必须提供一个类型签名，它 如果该值是某个更大表达式的一部分，则会变得笨拙。

有什么办法可以改善这一点，最好是从相反的方向，即从String 到Symbol？我想写Tag "blah" 并让 ghc 推断类型 TagString "blah"。

GHC.TypeLits 提供了someSymbolVal 函数，看起来有点 相关但它产生SomeSymbol，而不是Symbol，我可以完全掌握如何使用 它。

Answer 1

有什么办法可以改善这一点，最好是从相反的方向，即从字符串到符号？

不幸的是，没有办法直接从String 转到Symbol，因为 Haskell 不是依赖类型的。每次您想要一个新值并且没有带有所需符号的现有标签时，您都必须写出一个类型注释。

关于标签的保证仅由标签提供，GADT 不提供。

以下应该可以正常工作（其实在singletons包中可以找到相同的类型）：

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

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

这种类型与Proxy 的本质区别仅在于构造函数中有KnownSymbol 字典。即使符号是静态未知的，字典也可以让我们恢复其中包含的字符串：

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

我们在SSym 上进行模式匹配，从而将隐式KnownSymbol 字典纳入范围。仅Proxy 也无法做到这一点：

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

...它会产生一个 SomeSymbol，而不是 Symbol，我可以完全掌握如何使用它。

SomeSymbol 与SSym 类似，只是它隐藏了它携带的字符串，因此它不会出现在类型中。字符串可以通过构造函数上的模式匹配来恢复。

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

当您想批量操作不同的符号时，它会很有用，例如，您可以将它们放在一个列表中（对于不同的SSym-s，您不能这样做，因为它们的类型不同）。