解密仆人库中的 DataKind 类型提升答案

【问题标题】：Deciphering DataKind type promotion in Servant library解密仆人库中的 DataKind 类型提升
【发布时间】：2016-08-29 05:57:51
【问题描述】：

我正在尝试为 servant 库（一个类型级 Web DSL）使用 tutorial。该库广泛使用DataKind 语言扩展。

在那篇教程的开头，我们发现下面一行定义了一个 Web 服务端点：

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

我不明白在类型签名中包含字符串和数组意味着什么。我也不清楚'[JSON]前面的勾号（'）是什么意思。

所以我的问题归结为字符串和数组的类型/种类是什么，以及当 later 变成 WAI 端点时如何解释它？

附带说明一下，在描述 DataKinds 时始终使用 Nat 和 Vect 给我们留下了令人沮丧的有限示例，以便在尝试理解这些内容时查看。我想我已经在不同的地方至少读过这个例子十几次了，但我仍然觉得我不明白发生了什么。

【问题讨论】：

使用像 Agda 或 Idris 这样的依赖类型语言进行一些编程，这将为您提供一个可靠的工具集来进行像这里这样的类型级编程。比仅仅阅读Nat 和Nat-indexed Vect 要好得多。

标签： haskell data-kinds servant

【解决方案1】：

让我们建立一个仆人

目标

我们的目标将是仆人的目标：

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

跨越门槛

我们的初始服务将只是一个/，它返回一个列表 Users 在 JSON 中。

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

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

我们需要一种方法将其转换为 WAI type Application = Request -> (Response -> IO ResponseReceived) -> IO ResponseReceived。没有足够的空间来描述 WAI 的工作原理。基础：我们是给定一个请求对象和构造响应对象的方法，我们预计会返回一个响应对象。有很多方法这样做，但一个简单的选择就是这样。

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 内置类型级字符串文字。（这很好，因为在类型级别不是我的乐趣。）

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

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

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这个特殊问题。不我们可以再写一个函数serve，它依赖于 API 是 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 类型的实现，这不足以实施析取。作为报酬过低和懒惰的函数式程序员，我们将简单地抛出另一层抽象并定义类型级别名为Content 的函数接受api 类型并返回一个类型 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

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

我们保证ToApplication 实例为path :> rest，如果编译器可以保证path是一个类型级符号（意思是它可以[除其他外]映射到String symbolVal) 和 ToApplication rest 存在。
当请求到达时，我们在 pathInfos 上进行模式匹配到 to 决定成功。失败时，我们会做懒惰的事情并抛出 IO 中的未经检查的异常。
成功后，我们将在类型级别递归（提示激光噪声和雾机）与serve (undefined :: rest)。请注意rest 是比path :> rest“更小”的类型，就像你在数据构造函数上的模式匹配你最终得到一个“更小” 价值。
在递归之前，我们使用方便的记录更新。

注意：

type Content 函数将 path :> rest 映射到 Content rest。类型级别的另一种递归形式！另请注意，这意味着路由中的额外路径不会改变资源。这符合我们的直觉。
在 IO 中抛出异常并不是出色的 Library Design™，但我会由你来解决这个问题。（暗示： ExceptT/throwError.)
希望我们在这里慢慢激发DataKinds 的使用带字符串符号。能够以类型表示字符串 level 使我们能够使用类型来模式匹配路由类型级别。
我使用镜头来打包和拆包。对我来说破解速度更快这些 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) 如果编译器可以保证你懂的。
在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%

给予和接受

现在让我们演示一个类型级列表的用法，它的另一个特性 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

为什么有两个不同的类型类？好吧，我们需要一个[*]，这是一种类型列表，一种是*，它是那种只是单一的类型。就像你不能定义一个函数接受参数既是列表又是一个非列表（因为它不会进行类型检查），我们不能定义一个类型类它接受一个既是类型级列表的参数和一个类型级别的非列表（因为它不会进行种类检查）。如果我们有类...

让我们看看这个类型类的实际效果：

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 出错，其中之一深奥（因此使用起来更有趣）状态代码。

但是等等，为什么首先要使用类型级列表呢？因为正如我们之前所做的那样，我们将对它的两个进行模式匹配构造函数：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

希望这种说法是有道理的。列表运行时发生故障在我们找到匹配之前为空； <|> 保证我们会短路关于成功； 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 是多类型的。 (undefined 有 * 类型，所以 undefined :: rest 甚至不会在这里检查。）

剩余工作

我们如何才能成为一个完整的 Servant 竞争对手？

我们需要将Be 分解为Get, Post, Put, Delete。注意其中一些动词现在也以请求的形式获取 in 数据身体。在类型级别建模内容类型和请求主体需要类似的类型级机制。
如果用户想要将她的功能建模为除了 IO，比如一堆monad转换器？
A more precise, yet more complicated, routing algorithm.
嘿，现在我们有了 API 类型，是否可以生成服务的客户端？使 HTTP 产生的东西对遵循 API 描述的服务的请求，而不是创建 HTTP 服务本身？
文档。确保每个人都了解所有这些类型级别的 hijinks 是。 ;)

那个勾号

我也不清楚'[JSON]前面的勾号（'）是什么意思。

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

由于构造函数和类型共享相同的命名空间，因此通过提升可以得到模棱两可的类型名称。在这些情况下，如果你想引用提升的构造函数，你应该在它的名字前面加上引号。

使用 -XDataKinds，Haskell 的列表和元组类型原生提升为种类，并在类型级别享受同样方便的语法，尽管前缀是引号。对于两个或多个元素的类型级列表，例如上面的 foo2 的签名，可以省略引号，因为含义是明确的。但是对于一个或零个元素的列表（如 foo0 和 foo1），引号是必需的，因为类型 [] 和 [Int] 在 Haskell 中具有现有含义。

我们上面必须写的所有代码是多么冗长，除此之外还有很多其他原因是由于类型级编程在 Haskell 中仍然是二等公民，这与依赖类型语言（Agda、Idris、Coq）不同）。语法很奇怪，扩展很多，文档很少，错误很无意义，但是类型级编程很有趣。

【讨论】：

很好的答案！这可以用implementing a minimal version of haskell servant 和Servant, Type Families, and Type-level Everything 来补充。

【解决方案2】：

启用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" 都是类型 Symbol 的类型，JSON 是类型 *（定义为 here）和 '[JSON] 的（老式）类型是一种类型[*]，即它是一个单例类型级列表（它等同于JSON ': '[]，同样[x] 等同于x:[]）。

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

【讨论】：