使用GADT的类服务实现

Question

我正在读优秀的为什么仆人是类型级别的DSL？。到目前为止，实现的问题在于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)     _              = []

我对以下内容很感兴趣：

幸运的是，GADTs可以在这里有所帮助。我们可以将Endpoint转换为跟踪捕获的GADT，然后使用某些类型级别的计算从捕获列表中获取链接生成函数的类型，并通过类型生成实例定义链接生成函数，这些实例将通过捕获并为每个实例添加一个参数.对于非常稳定的域，基于GADT的方法会很好地工作(除了更容易接近)，并且在这里不考虑，因为我们所要求的灵活性。

我对GADT方法感兴趣，但是我可以提供一些提示，说明如何创建一个GADT，它将“跟踪捕获，然后使用一些类型级别的计算从我们的捕获列表中获取链接生成函数的类型”。

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

Answer 1

我不熟悉仆人，但也许这句话指的是像下面这样的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"]