haskell - 可以为类型提供文字的构造函数的数据类型提升

Question

我有一个简单的数据类型

data Label  = LabelK String 

声明：

• 一种Label类型Type
• LabelK类型的数据构造函数String -> Label

我想象的类型会提升为：

• 一种'Label
• 'LabelK一种类型的构造函数forall {l :: Symbol}. Label l

但是，情况似乎并非如此，而是我得到了

:kind 'LabelK :: String -> Label 

因此，promotion'LabelK是一个函数（？），它以 aString作为输入并给出一种类型'Label。恐怕 Haskell 做不到。

我们可以验证

data Proxy (i :: k) where  
  ProxyK :: Proxy i      

如果我们想在 type 上建立一个见证'LabelK "titi"

v3 = ProxyK :: Proxy ('LabelK "titi") -- fails

"titi"被提升为 a Symbol，作为提升 Literals的一部分，我们有一个类型错误。

---

那么，只有在文档中使用类型级字符串（又名 a Symbol）来参数化命名类型来自己编写它吗？：

data Labl (l :: Symbol) = 
   Get 

Get类似于ProxyK并给我们一个类型的值Labl l

:t Get :: forall {l :: Symbol}. Labl l 

然后

Get :: Labl "x"

消除了在类型索引处构建代理的需要，LabelK "titi"这是我们无法做到的

---

PS：在ghci，一个可以使用

:set -fprint-explicit-kinds
:set -fprint-explicit-foralls

v6 = Get :: forall {l :: Symbol}. Labl l（但由于某种原因我们不能写？）

标签： haskellghcitype-level-computation