使用带有 Haskell 的 -XDataKinds 的列表类型

Question

我在函数中使用了返回类型（使用包haskell-src-exts）：

import Language.Haskell.Exts.Syntax (Exp(..))
import Language.Haskell.Exts.SrcLoc (SrcSpanInfo(..))
:k Exp SrcSpanInfo
Exp SrcSpanInfo :: *

这是一种类型。到目前为止一切顺利。

但现在我想更好地打字：

:set -XDataKinds
> :k 'List
'List :: l -> [Exp l] -> Exp l

所以，这东西想要更多的东西。好吧，我能做到。

> :k 'List SrcSpanInfo 
'List SrcSpanInfo :: [Exp *] -> Exp *

一步之遥。好的。

> :k 'List SrcSpanInfo [Exp SrcSpanInfo]

<interactive>:1:19: error:
    • Expected kind ‘[Exp *]’, but ‘[Exp SrcSpanInfo]’ has kind ‘*’
    • In the second argument of ‘ 'List’, namely ‘[Exp SrcSpanInfo]’
      In the type ‘ 'List SrcSpanInfo [Exp SrcSpanInfo]’

在这一点上，我感到很困惑。 对我来说，感觉就像我给它的东西绝对是它所要求的。 究竟是什么意思？

Answer 1

从 cmets 中，我突然想到您实际上可能不是在寻找提升的类型（即种类），而是在寻找常规类型。

从 cmets（特别是：“...desired kind *...”）看来，您只是想构造一个 Exp SrcSpanInfo 类型的值（实际上，这些类型实际上并不适用于种类级别的使用）。

为此，只需将参数应用于构造函数：

> span = noInfoSpan $ mkSrcSpan noLoc noLoc
> :t span
span :: SrcSpanInfo
> list = List span []
> :t list
list :: Exp SrcSpanInfo

---

原答案

表达式[Exp SrcSpanInfo] 不表示“具有单个元素Exp SrcSpanInfo的类型的类型级列表”，而是表示“单个类型是Exp SrcSpanInfo" 类型的元素，类似于 [Int] 或 [String]。

编译器无法区分前者和后者，所以它默认使用更旧、更标准的解释。

为了让它看到一个类型级别的列表，它必须用单引号引起来，就像你对'List所做的那样。

此外，Exp 是一种类型，但是当用于一种类型的签名时，它会被提升为一种类型。为了构造一个类型Exp *，你必须使用one of its constructors。我将使用List 构造函数，因为它最容易实例化：

> :k 'List SrcSpanInfo '[ 'List SrcSpanInfo '[] ]

Answer 2

[a] 是列表的类型。要构建（提升）列表，请写'[a]：

:k 'List SrcSpanInfo '[ 'List Int '[] ]

将'List 应用于SrcSpanInfo 之类的类型可能也不是您想要的（希望我的示例也将它应用于Int 表明某些情况已关闭）。