在Servant库中解密DataKind类型提升

Question

我想戈克该教程的仆人库,类型级Web DSL.该库广泛使用DataKind语言扩展.

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

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

我不明白在类型签名中包含字符串和数组意味着什么.我也不清楚刻度线(')在前面是什么意思'[JSON].

所以我的问题归结为是什么类型/类型的字符串和数组,而这是怎么后来当它变成了WAI终点解释？

---

作为旁注,一致使用Nat和Vect描述DataKinds时,我们会在尝试理解这些内容时看到令人沮丧的有限例子.我想我已经在不同的地方至少读了十几次这个例子,我仍然觉得我不明白发生了什么.

Answer 1

让我们建立一个仆人

目标

我们的目标是仆人的目标:

• 将我们的REST API指定为单一类型 API
• 将服务实现为一个单一的副作用(读取:monadic)功能
• 使用真实类型来建模资源,仅在最后序列化为较小的类型,例如JSON或Bytestring
• 遵循大多数Haskell HTTP框架使用的通用WAI(Web应用程序接口)接口

越过门槛

我们的初始服务只是/返回UserJSON 中的s 列表 .

-- 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.

:<|> s在路上

现在我们挑战自己设计一个路由系统,我们可以在虚假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,如果我们能以某种方式对各类模式匹配,并实现不同这将是很好serve的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端点具有类型的实现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以确定成功.失败时,我们会做懒惰的事情并抛出一个未经检查的异常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在这里用来表示失败.再次,不是伟大的图书馆设计™.

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一种方法来抽象出将类型值转换为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能够与没有运行时的成本做到这一点,并在t在Proxy t是聚kinded.(undefined 有类型*所以undefined :: rest甚至不会在这里检查.)

剩下的工作

我们怎样才能一路走向完整的Servant竞争对手？

• 我们需要打破Be成Get, Post, Put, Delete.需要注意的是一些动词的现在也需要在数据请求主体的形式.在类型级别对内容类型和请求主体建模需要类似的类型级机制.

• 如果用户想要将其功能建模为其他内容 IO,例如一堆monad变换器,该怎么办？

• 更精确,更复杂的路由算法.

• 嘿,现在我们的API有一个类型,是否可以生成服务的客户端？是什么使得对服务的HTTP请求服从API描述而不是自己创建HTTP服务？

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

那个刻度线

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

答案是模糊不清的,并且在第7.9节的GHC手册中.

由于构造函数和类型共享相同的命名空间,因此通过提升,您可以获得不明确的类型名称.在这些情况下,如果要引用提升的构造函数,则应在其名称前加上引号.

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

这就是我们上面编写的所有代码的冗长程度,除此之外还有很多其他因为类型级编程仍然是Haskell中的二等公民,而不是依赖类型的语言(Agda,Idris,Coq).语法很奇怪,扩展很多,文档稀疏,错误是无稽之谈,但男孩哦男孩类型级编程很有趣.

Answer 2

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

• 如果你有data A = B T | C U，你现在得到一个新种类A和新类型'B :: T -> A，并且，'C :: U -> A哪里T和U是类似提升的新种类T和U类型
• 如果没有歧义的话，可以写B为'Betc。
• 类型级字符串都共享相同的 kind Symbol，因此您可以使用例如"foo" :: Symbol和"bar" :: Symbol作为有效类型。

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

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