title: Servant-like implementation with GADTs
body: <p>I'm reading the excellent <a href="https://haskell-servant.github.io/posts/2018-07-12-servant-dsl-typelevel.html" rel="nofollow noreferrer">Why is servant a type-level DSL?</a>. I've got to the section where the problem with the implementation presented so far is that the number of captures in an <code>Endpoint</code> can vary and there is no way of implementing a total a link generating function without dependant types. </p>
  
  <p>The <code>Endpoint</code> definition is:</p>
  
  <pre class="lang-hs prettyprint-override"><code>data Method = Get | Post
  
  data Endpoint = Static String Endpoint
                | Capture Endpoint
                | Verb Method
  </code></pre>
  
  <p>and example definitions are:</p>
  
  <pre class="lang-hs prettyprint-override"><code>getHello :: Endpoint
  getHello = Static "hello" (Capture (Verb Get))
  
  twoCaptures :: Endpoint
  twoCaptures = Capture (Capture (Verb Post))
  
  noCaptures :: Endpoint
  noCaptures = Static "hello" (Verb Post)
  </code></pre>
  
  <p>and the <strong>non-total</strong> link making function is:</p>
  
  <pre class="lang-hs prettyprint-override"><code>linkTo :: Endpoint -&gt; [String] -&gt; 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)     _              = []
  </code></pre>
  
  <p>I'm intrigued by the following:</p>
  
  <blockquote>
    <p>Fortunately, GADTs can help here. We could turn <code>Endpoint</code> 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.</p>
  </blockquote>
  
  <p>I'm interested in experimenting with the GADT approach however I could do with some hints for how to create a GADT which will <em>"track captures and then use some type-level computations to get the type of the link-making function from our list of captures"</em> </p>
  
  <p>Can anyone give me some hints for how to get started with a GADT version. Thanks.</p>