api - 了解 Servant 论文中的 'echo' 服务示例 API

Question

servant paper简介包含以下示例 API 类型:

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

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

以下是我对此的三个问题:

1. 类型定义中怎么会有字符串文字？

"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扩展允许您在类型签名中使用这些字符串文字。他们每个人都代表一种不同的类型。它们都属于Symbol类型;我们可以使用 ghci 中的 :kind 命令对此进行测试:

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

因为在 Haskell 中只有 * 类型才有值，所以这些类型级别的字符串不存在。但有functions无论如何，您都可以获取相应的术语级字符串。

What is the symbol :>?

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

What does the apostrophe before the list type mean?

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

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] :: [*]