Servant-like implementation with GADTs

Question

I'm reading the excellent Why is servant a type-level DSL?. I've got to the section where the problem with the implementation presented so far is that the number of captures in an Endpoint can vary and there is no way of implementing a total a link generating function without dependant types.

The Endpoint definition is:

data Method = Get | Post

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

and example definitions are:

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

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

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

and the non-total link making function is:

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

I'm intrigued by the following:

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.

I'm interested in experimenting with the GADT approach however I could do with some hints for how to create a GADT which will "track captures and then use some type-level computations to get the type of the link-making function from our list of captures"

Can anyone give me some hints for how to get started with a GADT version. Thanks.

chi chi · Accepted Answer · 2018-08-17T09:39:37

I am not familiar with Servant, but perhaps the quote was referring to some GADT like the following one. The idea is to define a type Endpoint t where t is of the form String -> String -> ... -> Link where all the string arguments correspond to the captures. Once this is done, then toLink is simply of type Endpoint t -> t.

I did not use type classes.

{-# 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

A small example:

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

Servant-like implementation with GADTs

1 Answers