从 Servant 论文中理解 'echo' 服务示例 API

Question

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] 是什么意思。

Answer 1

How is there a string literal in the definition of a type?

DataKinds extension lets you use these string literals in type signatures. Each one of them represents a different type. They all belong to the kind Symbol；我们可以使用 ghci:

中的 :kind 命令来测试它

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

因为在Haskell中只有种类*的类型有值，所以这些类型级别的字符串是不存在的。但是有functions让你无论如何都能得到相应的term-level字符串

What is the symbol :>?

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

What does the apostrophe before the list type mean?

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

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

这些提升的构造函数不包含任何项（因为它们有 * 以外的种类）。

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

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

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

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

从 Servant 论文中理解 'echo' 服务示例 API

Understanding 'echo' service example API from Servant paper

api

haskell

servant