GADT 的仆人式实施

Question

我正在阅读优秀的 Why is servant a type-level DSL?。我已经到了这部分，到目前为止实现的问题是 Endpoint 中的捕获数量可能会有所不同，并且没有办法实现一个 link 生成函数而不依赖类型。

Endpoint定义是：

data Method = Get | Post

data Endpoint = Static String Endpoint
              | Capture Endpoint
              | Verb Method

示例定义为：

getHello :: Endpoint
getHello = Static "hello" (Capture (Verb Get))

twoCaptures :: Endpoint
twoCaptures = Capture (Capture (Verb Post))

noCaptures :: Endpoint
noCaptures = Static "hello" (Verb Post)

和非总link制作函数是：

linkTo :: Endpoint -> [String] -> Link
linkTo (Static str rest) captureValues  = str : linkTo rest captureValues
linkTo (Capture rest)    (c : cs)       = c   : linkTo rest cs
linkTo (Capture rest)    []             = error "linkTo: capture value needed but the list is empty" -- :-(
linkTo (Verb method)     _              = []

我对以下内容很感兴趣：

Fortunately, GADTs can help here. We could turn Endpoint into a GADT that tracks captures and then use some type-level computations to get the type of the link-making function from our list of captures, as well as define the link making function through typeclass instances that would go through the captures and add an argument for each of them ... a GADT-based approach would work well (in addition to being more approachable) for very stable domains, and is not considered here because of the kind of flexibility we are asking for.

我有兴趣尝试使用 GADT 方法，但是我可以得到一些关于如何创建 GADT 的提示，它将 "track captures and then use some type-level computations to get the type of the link-making function from our list of captures"

谁能给我一些关于如何开始使用 GADT 版本的提示。谢谢。

Answer 1

我对 Servant 不熟悉，但也许引用的是像下面这样的一些 GADT。这个想法是定义一个类型 Endpoint t，其中 t 的形式是 String -> String -> ... -> Link，其中所有字符串参数都对应于捕获。完成后，toLink 就是 Endpoint t -> t.

类型

我没有使用类型类。

{-# LANGUAGE GADTs #-}
module ServantEndpoint where

type Link = [String]

data Method = Get | Post

data Endpoint t where
   Static :: String -> Endpoint t -> Endpoint t
   Capture :: Endpoint t -> Endpoint (String -> t)
   Verb :: Method -> Endpoint Link

linkTo :: Endpoint t -> t
linkTo e = go e []
   where
   go :: Endpoint t -> Link -> t
   go (Static str rest) l = go rest (str : l)
   go (Capture rest)    l = \s -> go rest (s : l)
   go (Verb _method)    l = reverse l

一个小例子：

test :: Link
test = f "capture1" "capture2"
   where f = linkTo (Capture (Static "static1" (Capture (Static "static2" (Verb Get)))))
-- output: ["capture1","static1","capture2","static2"]

GADT 的仆人式实施

Servant-like implementation with GADTs

haskell

gadt

servant