解读 Servant 库中的 DataKind 类型提升

Deciphering DataKind type promotion in Servant library

我正在尝试使用 tutorial for the servant library, a type-level web DSL. The library makes extensive use of the DataKind 语言扩展。

在该教程的早期，我们找到了以下定义 Web 服务端点的行：

type UserAPI = "users" :> QueryParam "sortby" SortBy :> Get '[JSON] [User]

我不明白在类型签名中包含字符串和数组是什么意思。我也不清楚 '[JSON].

前面的刻度线 (') 是什么意思

所以我的问题归结为字符串和数组的 type/kind 是什么，这个 later 变成 WAI 端点时如何解释？

作为旁注，在描述 DataKinds 时一致使用 Nat 和 Vect 给我们留下了一组令人沮丧的示例，以便在试图理解这些东西时查看.我想我已经在不同的地方至少通读了十几遍那个例子，但我仍然觉得我不明白发生了什么。

启用 DataKinds 后，您将获得根据常规数据类型定义自动创建的新类型：

  • 如果您有 data A = B T | C U，您现在会得到一个新类型 A 和新类型 'B :: T -> A 和 'C :: U -> A，其中 T 和 U 是类似提升的 T 和 U 类型的新种类
  • 如果没有歧义，可以写B为'B等等
  • 类型级别的字符串都共享相同的类型 Symbol，因此您有例如"foo" :: Symbol 和 "bar" :: Symbol 为有效类型。

在您的示例中，"users" 和 "sortby" 都是 kind Symbol 类型，JSON 是 kind [=28= 的（老式）类型]（定义here），而'[JSON]是一种类型[*]，即它是一个单例类型级列表（它等同于JSON ': '[]，方式相同[x] 一般等同于 x:[]）。

[User]类型是kind的常规类型*；它只是 User 列表的类型。它不是单例类型级别的列表。

让我们打造一个 Servant

目标

我们的目标将是 Servant 的目标：

  • 将我们的 REST API 指定为单一类型 API
  • 将服务实现为一个单一的 side-effectful（阅读：monadic） 函数
  • 使用真实类型为资源建模，仅序列化为较小的类型 在最后，例如JSON 或字节串
  • 遵守最常用的 WAI（Web 应用程序接口）接口 Haskell HTTP 框架使用

跨越门槛

我们的初始服务将只是一个 / return 的列表 User 秒 JSON。

-- Since we do not support HTTP verbs yet we will go with a Be
data User = ...
data Be a
type API = Be [User]

虽然我们还没有写一行 value-level 代码，但我们已经 已经充分代表了我们的 REST 服务——我们只是 作弊并在类型级别完成。这让我们感到兴奋，并且， 很长一段时间以来，我们第一次对网络充满希望 再次编程。

我们需要一种方法将其转换为 WAI type Application = Request -> (Response -> IO ResponseReceived) -> IO ResponseReceived。 没有足够的篇幅来描述 WAI 是如何工作的。基础知识：我们是 给定一个请求 object 和一种构造响应 object 的方法，我们 预计 return 回应 object。有很多方法 这样做，但一个简单的选择是这样。

imp :: IO [User]
imp =
  return [ User { hopes = ["ketchup", "eggs"], fears = ["xenophobia", "reactionaries"] }
         , User { hopes = ["oldies", "punk"], fears = ["half-tries", "equivocation"] }
         ]

serve :: ToJSON a => Be a -> IO a -> Application
serve _ contentIO = \request respond -> do
  content <- contentIO
  respond (responseLBS status200 [] (encode content))

main :: IO ()
main = run 2016 (serve undefined imp)

这确实有效。我们可以 运行 并将其卷曲并得到 预期回复。

% curl 'http://localhost:2016/'
[{"fears":["xenophobia","reactionaries"],"hopes":["ketchup","eggs"]},{"fears":["half-tries","equivocation"],"hopes":["oldies","punk"]}]%

请注意，我们从未构造过 Be a 类型的值。我们用了 undefined。函数本身完全忽略了参数。 实际上没有办法构造 Be a 类型的值，因为 我们从未定义任何数据构造函数。

为什么还要有Be a参数？可怜的简单事实是我们需要 a 变量。它告诉我们我们的内容类型是什么，它 让我们设置甜蜜的 Aeson 约束。

代码：0Main.hs.

:<|>在路上

现在我们挑战自己设计一个路由系统，我们可以 在假 URL 文件夹中的不同位置有单独的资源 等级制度。我们的目标是支持此类服务：

type API =
       "users" :> Be [User]
  :<|> "temperature" :> Int

为此，我们首先需要打开 TypeOperators 和 DataKinds 个扩展名。正如@Cactus 的回答中详述的那样，数据类型 允许我们在类型级别存储数据，GHC 带有 built-in type-level 字符串文字。 （这很棒，因为在 类型级别不是我的乐趣。）

（我们还需要 PolyKinds 以便 GHC 可以 kind-infer 这种类型。是的，我们 现在在扩展丛林的深处。）

然后，我们需要为 :>（子目录 运算符）和 :<|>（析取运算符）。

data path :> rest
data left :<|> right =
  left :<|> right

infixr 9 :>
infixr 8 :<|>

我说聪明了吗？我的意思是非常简单。注意我们已经给出 :<|> 一个类型构造函数。这是因为我们将粘合我们的 monadic 共同发挥作用以实现析取和...哦，这只是 举个例子更容易。

imp :: IO [User] :<|> IO Int
imp =
  users :<|> temperature
  where
    users =
      return [ User ["ketchup", "eggs"] ["xenophobia", "reactionaries"]
             , User ["oldies", "punk"] ["half-tries", "equivocation"]
             ]
    temperature =
      return 72

现在让我们把注意力转向serve的特殊问题。不 我们可以再写一个依赖于 API 的函数 serve Be a。现在我们在 RESTful 的类型级别有了一点 DSL 服务，如果我们能以某种方式在 类型并为 Be a、path :> rest 实施不同的 serve， 和 left :<|> right。还有！

class ToApplication api where
  type Content api
  serve :: api -> Content api -> Application

instance ToJSON a => ToApplication (Be a) where
  type Content (Be a) = IO a
  serve _ contentM = \request respond -> do
    content <- contentM
    respond . responseLBS status200 [] . encode $ content

注意这里关联数据类型的用法（这又需要我们 打开 TypeFamilies 或 GADTs）。虽然 Be a 端点 有一个 IO a 类型的实现，这不足以 实施分离。作为报酬过低和懒惰的函数式程序员，我们 将简单地抛出另一层抽象并定义一个 type-level 名为 Content 的函数接受类型 api 和 returns 类型 Content api.

instance Exception RoutingFailure where

data RoutingFailure =
  RoutingFailure
  deriving (Show)

instance (KnownSymbol path, ToApplication rest) => ToApplication (path :> rest) where
  type Content (path :> rest) = Content rest
  serve _ contentM = \request respond -> do
    case pathInfo request of
      (first:pathInfoTail)
        | view unpacked first == symbolVal (Proxy :: Proxy path) -> do
            let subrequest = request { pathInfo = pathInfoTail }
            serve (undefined :: rest) contentM subrequest respond
      _ ->
        throwM RoutingFailure

我们可以在这里分解代码行：

  • 如果 编译器可以保证 path 是一个 type-level 符号（意思是 它可以 [除其他事项外] 映射到 String 与 symbolVal) 和 ToApplication rest 存在。

  • 当请求到达时，我们在pathInfos上进行模式匹配到 决定成败。失败时，我们会做懒惰的事情并抛出 IO.

    • 中的未检查异常

  • 成功后，我们将在类型级别递归（提示激光噪声 和烟雾机）与 serve (undefined :: rest)。请注意 rest 是 "smaller" 类型而不是 path :> rest 类型，很像当你 数据构造函数上的模式匹配最终得到 "smaller" 价值.

  • 在递归之前，我们用一个方便的方式减少 HTTP 请求 记录更新.

注意：

  • type Content 函数将 path :> rest 映射到 Content rest。 类型级别的另一种递归形式！另请注意，这 意味着路由中的额外路径不会改变 资源。这符合我们的直觉。

  • 投掷一个IO 中的异常不是 Great Library Design™，但我会 由您来解决该问题。 （暗示： ExceptT/throwError.)

  • 希望我们能在这里慢慢激发 DataKinds 的使用 与字符串符号。能够以该类型表示字符串 级别使我们能够使用类型来模式匹配路由 类型级别。

  • 我用镜头打包和解包。这对我来说更快了 这些 SO 用镜头回答，但当然你可以只使用 pack 来自 Data.Text 库。

好的。再举一个例子。呼吸。休息一下。

instance (ToApplication left, ToApplication right) => ToApplication (left :<|> right) where
  type Content (left :<|> right) = Content left :<|> Content right
  serve _ (leftM :<|> rightM) = \request respond -> do
    let handler (_ :: RoutingFailure) =
          serve (undefined :: right) rightM request respond
    catch (serve (undefined :: left) leftM request respond) handler

在这种情况下我们

  • 保证ToApplication (left :<|> right)如果编译器可以 保证 blah blah blah 你明白了。

  • 在type Content函数中引入另一个入口。这里是 一行代码，让我们建立一个 IO [User] :<|> IO Int 的类型，并让编译器在 实例分辨率。

  • 捕获我们上面抛出的异常！当异常发生在 左边，我们往右边走。同样，这不是 Great Library Design™。

运行 1Main.hs 你应该可以 curl 像这样。

% curl 'http://localhost:2016/users'
[{"fears":["xenophobia","reactionaries"],"hopes":["ketchup","eggs"]},{"fears":["half-tries","equivocation"],"hopes":["oldies","punk"]}]%

% curl 'http://localhost:2016/temperature'
72%

给予与索取

现在让我们演示 type-level 列表的用法，这是 DataKinds。我们将扩充 data Be 来存储类型列表 端点可以给出。

data Be (gives :: [*]) a

data English
data Haskell
data JSON

-- | The type of our RESTful service
type API =
       "users" :> Be [JSON, Haskell] [User]
  :<|> "temperature" :> Be [JSON, English] Int

让我们也定义一个类型类来匹配类型列表 端点可以给出 HTTP 请求的 MIME 类型列表 可以接受。我们将在这里使用 Maybe 来表示失败。再一次，不 伟大的图书馆设计™。

class ToBody (gives :: [*]) a where
  toBody :: Proxy gives -> [ByteString] -> a -> Maybe ByteString

class Give give a where
  give :: Proxy give -> [ByteString] -> a -> Maybe ByteString

为什么有两个不同的类型类？好吧，我们需要一个 [*], 这是类型列表的一种，一种是 *， 只是单一类型的那种。就像你不能定义一个 函数接受一个既是列表又是 a non-list（因为它不会 type-check），我们不能定义类型类 它需要一个既是 type-level 列表的参数 和 type-level non-list（因为它不会 kind-check）。如果我们有 kindclasses...

让我们看看这个类型类的作用：

instance (ToBody gives a) => ToApplication (Be gives a) where
  type Content (Be gives a) = IO a
  serve _ contentM = \request respond -> do
    content <- contentM
    let accepts = [value | ("accept", value) <- requestHeaders request]
    case toBody (Proxy :: Proxy gives) accepts content of
      Just bytes ->
        respond (responseLBS status200 [] (view lazy bytes))
      Nothing ->
        respond (responseLBS status406 [] "bad accept header")

非常好。我们使用 toBody 作为抽象计算的一种方式 将类型 a 的值转换为 WAI 的底层字节 想要。失败时，我们将简单地返回 406，其中一个 深奥的（因此使用起来更有趣）状态代码。

但是等等，为什么要首先使用 type-level 列表？因为 正如我们之前所做的那样，我们将在其两个 pattern-match 构造函数：nil 和 cons.

instance ToBody '[] a where
  toBody Proxy _ _ = Nothing

instance (Give first a, ToBody rest a) => ToBody (first ': rest) a where
  toBody Proxy accepted value =
    give (Proxy :: Proxy first) accepted value
      <|> toBody (Proxy :: Proxy rest) accepted value

希望这是有道理的。当列表 运行s 时发生故障 在我们找到匹配之前为空； <|> 保证我们会 short-circuit 成功时； toBody (Proxy :: Proxy rest) 是递归的情况。

我们需要一些有趣的 Give 实例来玩。

instance ToJSON a => Give JSON a where
  give Proxy accepted value =
    if elem "application/json" accepted then
      Just (view strict (encode value))
    else
      Nothing

instance (a ~ Int) => Give English a where
  give Proxy accepted value =
    if elem "text/english" accepted then
      Just (toEnglish value)
    else
      Nothing
    where
      toEnglish 0 = "zero"
      toEnglish 1 = "one"
      toEnglish 2 = "two"
      toEnglish 72 = "seventy two"
      toEnglish _ = "lots"

instance Show a => Give Haskell a where
  give Proxy accepted value =
    if elem "text/haskell" accepted then
      Just (view (packed . re utf8) (show value))
    else
      Nothing
再次

运行 服务器，您应该可以 curl 像这样：

% curl -i 'http://localhost:2016/users' -H 'Accept: application/json'
HTTP/1.1 200 OK
Transfer-Encoding: chunked
Date: Wed, 04 May 2016 06:56:10 GMT
Server: Warp/3.2.2

[{"fears":["xenophobia","reactionaries"],"hopes":["ketchup","eggs"]},{"fears":["half-tries","equivocation"],"hopes":["oldies","punk"]}]%

% curl -i 'http://localhost:2016/users' -H 'Accept: text/plain'
HTTP/1.1 406 Not Acceptable
Transfer-Encoding: chunked
Date: Wed, 04 May 2016 06:56:11 GMT
Server: Warp/3.2.2

bad accept header%

% curl -i 'http://localhost:2016/users' -H 'Accept: text/haskell'
HTTP/1.1 200 OK
Transfer-Encoding: chunked
Date: Wed, 04 May 2016 06:56:14 GMT
Server: Warp/3.2.2

[User {hopes = ["ketchup","eggs"], fears = ["xenophobia","reactionaries"]},User {hopes = ["oldies","punk"], fears = ["half-tries","equivocation"]}]%

% curl -i 'http://localhost:2016/temperature' -H 'Accept: application/json'
HTTP/1.1 200 OK
Transfer-Encoding: chunked
Date: Wed, 04 May 2016 06:56:26 GMT
Server: Warp/3.2.2

72%

% curl -i 'http://localhost:2016/temperature' -H 'Accept: text/plain'
HTTP/1.1 406 Not Acceptable
Transfer-Encoding: chunked
Date: Wed, 04 May 2016 06:56:29 GMT
Server: Warp/3.2.2

bad accept header%

% curl -i 'http://localhost:2016/temperature' -H 'Accept: text/english'
HTTP/1.1 200 OK
Transfer-Encoding: chunked
Date: Wed, 04 May 2016 06:56:31 GMT
Server: Warp/3.2.2

seventy two%

万岁！

请注意，我们已停止使用 undefined :: t 并切换到 Proxy :: Proxy t。两者都是黑客。在 Haskell 中调用函数让我们 为值参数指定值，但不为类型参数指定类型。 悲伤的不对称。 undefined和Proxy都是编码方式 在值级别键入参数。 Proxy 可以不用 运行时间成本和Proxy t中的t是poly-kinded。 (undefined 有类型 * 所以 undefined :: rest 甚至不会 kind-check 这里。）

剩余工作

我们如何才能一路晋升为完整的 Servant 竞争对手？

  • 我们需要将 Be 分成 Get, Post, Put, Delete。注意 其中一些动词现在也以请求的形式获取 in 数据 body。在类型级别建模内容类型和请求主体 需要类似的 type-level 机器。

  • 如果用户想要将她的功能建模为除此之外的东西怎么办 IO，比如一堆monad transformer?

  • A more precise, yet more complicated, routing algorithm.

  • 嘿，既然我们有了 API 的类型，是否可以 生成一个client的服务？使 HTTP 成为可能的东西 请求服从 API 描述的服务，而不是 创建 HTTP 服务本身？

  • 文档。确保每个人body 都明白所有这些 type-level hijinks 是。 ;)

那个刻度线

I am also unclear what the tick mark (') means in front of '[JSON].

答案晦涩难懂，卡在GHC's manual in section 7.9。

Since constructors and types share the same namespace, with promotion you can get ambiguous type names. In these cases, if you want to refer to the promoted constructor, you should prefix its name with a quote.

With -XDataKinds, Haskell's list and tuple types are natively promoted to kinds, and enjoy the same convenient syntax at the type level, albeit prefixed with a quote. For type-level lists of two or more elements, such as the signature of foo2 above, the quote may be omitted because the meaning is unambiguous. But for lists of one or zero elements (as in foo0 and foo1), the quote is required, because the types [] and [Int] have existing meanings in Haskell.

这个，我们上面写的所有代码是多么冗长，除此之外还有很多其他原因是 type-level 编程在 Haskell 中仍然是 second-class 公民，这与在dependently-typed 种语言（Agda、Idris、Coq）。语法很奇怪，扩展很多，文档很少，错误都是胡说八道，但是男孩哦男孩 type-level 编程很有趣