问

用相应的符号标记字符串

手机用户2502873825 发布于 2023-01-12 13:37

我想要一个简单的方法来创建一个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看起来有点相关的函数,但是它生成了SomeSymbola Symbol而不是a ,我可以完全掌握如何使用它.

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,而不是一个符号,我可以完全掌握如何使用它.

SomeSymbol就像SSym它隐藏它携带的字符串,以便它不会出现在类型中.可以通过构造函数上的模式匹配来恢复字符串.
```
extractString'' :: SomeSymbol -> String
extractString'' (SomeSymbol proxy) = symbolVal proxy
```
当你想要批量操作不同的符号时,它会很有用,例如你可以把它们放在一个列表中(你不能用不同的SSym-s 做,因为它们的类型不同).
2023-01-12 13:40 回答

键盘上的泪g_752

撰写答案

今天，你开发时遇到什么问题呢？

立即提问

热门标签