7

我正在尝试阅读servant库的教程，这是一个类型级的Web DSL。该库广泛使用语言扩展。DataKind

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

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

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

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

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

4

2 回答 2

14

让我们建立一个仆人

目标

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

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

跨过门槛

我们的初始服务将只是一个以 JSON 格式/返回 s 列表的 a 。User

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

尽管我们还没有编写一行值级别的代码，但我们已经充分代表了我们的 REST 服务——我们只是在类型级别上作弊并完成了它。这让我们感到很兴奋，很长一段时间以来，我们第一次对 Web 编程再次抱有希望。

我们需要一种将其转换为 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"]}]%

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

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

代码：0Main.hs。

:<|>在路上

现在我们挑战自己设计一个路由系统，在这个系统中，我们可以在虚假 URL 文件夹层次结构中的不同位置拥有不同的资源。我们的目标是支持此类服务：

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

为此，我们首先需要打开TypeOperators和 DataKinds扩展。正如@Cactus 的回答中所详述的，数据种类允许我们在类型级别存储数据，GHC 内置了类型级别的字符串文字。（这很好，因为在类型级别定义字符串不是我的乐趣。）

（我们还需要PolyKindsGHC 可以对这种类型进行类推断。是的，我们现在深入扩展丛林的中心。）

:>然后，我们需要对（子目录运算符）和:<|>（析取运算符）进行巧妙的定义。

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，如果我们能以某种方式对类型进行模式匹配并实现不同serve的 for Be a、path :> rest和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端点具有 type 的实现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是一个类型级别的符号（意味着它可以[除其他外]映射到 a Stringwith symbolVal）并且存在ToApplication rest。

  • 当请求到达时，我们进行模式匹配pathInfos以确定成功。失败时，我们将做懒惰的事情并在IO.

  • 成功后，我们将在类型级别（提示激光噪声和雾机）递归serve (undefined :: rest)。请注意，这rest 是一个比 更“小”的类型path :> rest，就像在数据构造函数上进行模式匹配时最终得到一个“更小”的值一样。

  • 在递归之前，我们通过方便的记录更新来减少 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)编译器是否可以保证你得到它。

  • 在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在这里用 来表示失败。同样，不是 Great Library Design™。

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

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

为什么有两个不同的类型类？好吧，我们需要一个用于 kind [*]，它是一个类型列表的 kind ，一个用于 kind *，它只是一个单一类型的 kind 。就像你不能定义一个函数来接受既是列表又是非列表的参数（因为它不会进行类型检查），我们不能定义一个类型类来接受既是类型又是类型的参数。级别列表和类型级别的非列表（因为它不会进行类型检查）。要是我们有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其用作抽象出将类型值转换为aWAI 所需的底层字节的计算的一种方式。如果失败，我们将简单地错误输出 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能够在没有运行时成本的情况下做到这一点，并且tinProxy t是多类型的。（undefined 有类型*所以undefined :: rest甚至不会在这里检查。）

剩下的工作

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

  • 我们需要分解Be成Get, Post, Put, Delete. 请注意，其中一些动词现在也以请求正文的形式接收数据。在类型级别对内容类型和请求主体进行建模需要类似的类型级别机制。

  • 如果用户想将她的函数建模为 之外的东西 IO，比如一堆 monad 转换器怎么办？

  • 更精确但更复杂的路由算法。

  • 嘿，现在我们有了 API 的类型，是否可以生成服务的客户端？向遵循 API 描述的服务发出 HTTP 请求而不是创建 HTTP 服务本身的东西？

  • 文档。确保每个人都了解所有这些类型级别的 hijink 是什么。;)

那个勾号

我也不清楚 '[JSON] 前面的刻度线 (') 是什么意思。

答案是模糊的，并且停留在GHC 的手册第 7.9 节中。

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

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

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

于 2016-05-04T07:10:17.823 回答
3

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

  • 如果你有data A = B T | C U，你现在得到一个新种类A和新类型'B :: T -> A，以及类似提升的新种类和类型的新种类'C :: U -> A在哪里？TUTU
  • 如果没有歧义，你可以写Bfor 'Betc。
  • 类型级字符串都共享相同的 kind Symbol，所以你有 eg"foo" :: Symbol和"bar" :: Symbol作为有效类型。

在您的示例中，"users"and"sortby"都是 kind 的类型Symbol，JSON是 kind 的（老式）类型（在此处*定义），并且是 kind 的类型，即它是单例类型级列表（它等同于相同的方式相当于一般）。'[JSON][*]JSON ': '[][x]x:[]

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

于 2016-05-04T05:41:14.197 回答