2

我正在阅读优秀的为什么仆人是类型级 DSL？. 我已经到了到目前为止提出的实现问题的部分，即 an 中的捕获数量Endpoint可能会有所不同，并且没有办法在没有依赖类型的情况下实现整个链接生成函数。

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)

非全链接功能为：

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)     _              = []

我对以下内容很感兴趣：

幸运的是，GADT 可以在这里提供帮助。我们可以Endpoint变成一个跟踪捕获的 GADT，然后使用一些类型级别的计算从我们的捕获列表中获取链接生成函数的类型，并通过将通过捕获的类型类实例定义链接生成函数并为它们中的每一个添加一个论点……对于非常稳定的域，基于 GADT 的方法可以很好地工作（除了更平易近人之外），并且由于我们所要求的灵活性而在此不予考虑。

我有兴趣尝试使用 GADT 方法，但是我可以提供一些关于如何创建 GADT 的提示，该 GADT 将“跟踪捕获，然后使用一些类型级计算从我们的列表中获取链接生成函数的类型捕获"

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

4

1 回答 1

2

我对仆人不熟悉，但也许这句话是指一些像下面这样的 GADT。这个想法是定义一个类型Endpoint t，其中所有字符串参数对应于捕获t的形式。String -> String -> ... -> Link一旦完成， thentoLink就是简单的 type 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"]
于 2018-08-17T09:39:37.993 回答