从仆人论文中理解“回声”服务示例 API答案

【问题标题】：Understanding 'echo' service example API from Servant paper从仆人论文中理解“回声”服务示例 API
【发布时间】：2017-06-08 17:34:26
【问题描述】：

servant paper 的介绍包含以下示例 API 类型：

type Echo = "echo"
          :> ReqBody ’[PlainText] String
          :> Get ’[PlainText] String

我试图理解这个例子。似乎是在定义一个类型同义词，但似乎涉及到一些我以前没有见过的东西。

我有以下三个问题：

"echo" 是一个字符串文字。我以为这些只用于定义特定的字符串，不知道在类型声明中使用时这是什么意思。

'servant' 包中这个符号的定义似乎是defined here，看起来像这样：

data (path :: k) :> a
    deriving (Typeable)
infixr 9 :>

我猜:> 对应于 api 字符串中的 /，但看不出这个定义是如何实现的。

这是我第一次看到函数类型->以外的非字母数字类型。

[PlainText] 我可以理解为简单地表示一个 PlainText 元素的列表，但相比之下我不明白 ’[PlainText] 的含义。

【问题讨论】：

这是 DataKinds 扩展在工作中，允许（大致）提升类型级别的值。使用它，可以定义一种依赖于 values 的类型，而不是像往常一样依赖于其他类型。这就是字符串可以出现在那里的原因。在类型级别，[T] 代表类型 list-of-T，而'[x] 代表（提升的）值“列表仅包含一个元素 x”。例如，甚至可以写'[x,y,z]。
这篇论文很好地解释了后面几节是如何实现的，没有假设太多知识，所以我建议你继续阅读:)。在阅读全文之前，我还发现 Andres Löh 的 Tiny Servant 文章是一个很好的介绍。

【解决方案1】：

类型的定义中怎么会有字符串字面量？

DataKinds 扩展允许您在类型签名中使用这些字符串文字。它们中的每一个都代表不同的类型。都属于Symbol的那种；我们可以使用 ghci 中的:kind 命令进行测试：

Prelude> :set -XDataKinds
Prelude> :kind "foo"
"foo" :: GHC.Types.Symbol

因为在 Haskell 中只有类型 * 的类型具有值，所以这些类型级别的字符串不会被占用。但是有functions，反正让你获取对应的词条级字符串。

符号是什么：>？

TypeOperators 扩展允许您使用运算符名称定义类型。这对于主要用于组合其他类型的参数化类型很有用。请注意，:> 有两个类型参数，但没有值级别的构造函数：它仅用于类型级别。

列表类型前的撇号是什么意思？

DataKinds 不仅仅是启用符号。它允许您将值构造函数用作types，而这些构造函数的类型依次变为kinds。例如：

Prelude> :set -XDataKinds
Prelude> :kind True
True :: Bool

这些提升的构造函数不包含任何术语（因为它们有除* 之外的其他种类）。

特别是，我们可以将列表提升到类型级别。但这会产生一些歧义。签名中的[Int] 是什么？它是Ints 的列表类型（具有* 的种类）还是具有一个元素的类型级列表，类型为Int？撇号清楚地表明我们正在讨论类型级列表。

Prelude> :set -XDataKinds
Prelude> :kind [Int]
[Int] :: *
Prelude> :kind '[Int]
'[Int] :: [*]
Prelude> :kind '[True]
'[True] :: [Bool]

多个元素的类型级列表不需要撇号，因为没有歧义：

Prelude> :kind [Int,Int]
[Int,Int] :: [*]

【讨论】：