# Dependently typed servers in Servant

(Not yet published), by edsko, andres.

Filed under coding.

In this brief blog post we will sketch a design for how one might implement dependently typed servers in Servant. That is, given some kind of type index

```
data T :: * -> * where
TStr :: T String -- ^ represented as "string" in the URL
TInt :: T Int -- ^ represented as "int" in the URL
```

we want to be able to have a dependently-typed server

```
serveNext :: T a -> Server (Capture "input" a :> Get '[JSON] a)
serveNext TStr a = return (a ++ "1")
serveNext TInt a = return (a + 1)
```

so that if our server provides `serveNext`

under the `/next`

prefix, we expect `/next/int/1`

to return `2`

, `/next/string/a`

to return `"a1"`

, and `/next/int/a`

to return a 404 (indicating, in this case, an ill-typed request). Note that the type of the capture as well as the return type are determined by the first argument to `serveNext`

.

We will assume familiarity with servant; see Implementing a minimal version of haskell-servant for an introduction. We will also assume familiarity with the following language extensions:

```
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
```

all of which we will need in this development.

## Preliminaries

We will need some reasonably standard preliminary definitions.

### Existentials

First, we need an existential type wrapper:

`data Some (f :: * -> *) = forall a. Some (f a)`

We will use these to parse type indices. If the route contains `int`

, we expect that to parse to `TInt`

, and when the route contains `string`

, we expect that to parse to `TStr`

. But then what is the type of the corresponding parser?

`fromText :: Text -> T ???`

Clearly, the type argument to `T`

here will depend on the input text. Hence, when we parse, we need to wrap the result in `Some`

:

```
instance FromText (Some T) where
fromText "string" = Just $ Some TStr
fromText "int" = Just $ Some TInt
fromText _ = Nothing
```

### Reified dictionaries

Haskell functions such as

`nub :: Eq a => [a] -> [a]`

have an implicit *dictionary* argument telling `nub`

how to compare elements of type `a`

. We can make this argument explicit by reifying the constraint:

```
data Dict (c :: Constraint) where
Dict :: c => Dict c
```

This allows us to write

```
nub' :: Dict (Eq a) -> [a] -> [a]
nub' Dict = nub
```

where we bring the `Eq a`

constraint constraint back into scope by pattern matching on the dictionary.

### Type level application

Finally, we will introduce a type family denoting type level application:

`type family Apply (f :: * -> *) (a :: *) :: *`

For instance, we can define

```
data Next a
type instance Apply Next a = Capture "input" a :> Get '[JSON] a
```

which would allow us to write the signature of `serveNext`

as

`serveNext :: T a -> Server (Apply Next a)`

The crucial point here is that `Next`

itself is a regular datatype, so that it’s legal to refer to `Next`

without its argument (as something of kind `* -> *`

).

## Dependently typed servers

A dependently typed server is a server with some argument, such that the value of that argument determines the type of the server. We can encode this as

```
newtype DepServer (ix :: * -> *) (f :: * -> *) (m :: * -> *) =
DepServer (forall a. ix a -> ServerT (Apply f a) m)
```

Here `ix`

is the type of the index (`T`

in our running example), and `f`

is the (dependent) type of the server (in our example, this will be `Next`

). The `m`

parameter is Servant’s standard server monad argument.

### HasDepServer

We now introduce a new type class, alongside the standard Servant standard `HasServer`

, that corresponds to dependent servers. *The key idea is that we will need a HasServer instance for all valid instantiations of the type argument:*

```
class HasDepServer ix f where
hasDepServer :: Proxy f -> ix a -> Dict (HasServer (Apply f a))
```

Let’s consider an example:

```
instance HasDepServer T Next where
hasDepServer _ TStr = Dict
hasDepServer _ TInt = Dict
```

What’s going on here? In order to show we can construct servers for `Next`

, we need to show that we have a `HasServer`

instance for all valid indices; in our case, that is `TStr`

and `TInt`

. In other words, we need to show we have `HasServer`

instances for both of

```
Capture "input" String :> Get '[JSON] String
Capture "input" Int :> Get '[JSON] Int
```

both of which we get for free from Servant. Hence, we can simply pattern match on the index and trivially construct the dictionary.

### Dependent captures

We’re almost there now. We can now introduce a dependent version of capturing part of a URL:

`data DepCapture (ix :: * -> *) (f :: * -> *)`

(For simplicity’s sake this combines the functionality of `(:>)`

and `Capture`

in a single combinator. It would be possible to separate this out.)

With this combinator we can define the API we want:

`type API = "next" :> DepCapture T Next`

The (somewhat simplified) `HasServer`

instance for the standard, non-dependent, `Capture`

looks like this:

```
instance (FromText a, HasServer f) => HasServer (Capture a :> f)
type ServerT (Capture a :> f) m = a -> ServerT f m
route = ...
```

The corresponding `HasServer`

for `DepCapture`

follows this closely; the main difference is that both the thing we are capturing and the remainder of the server now have kind `* -> *`

instead of kind `*`

. First, we note that the server for a dependent capture must be a dependent server:

```
instance (FromText (Some ix), HasDepServer ix f)
=> HasServer (DepCapture ix f) where
type ServerT (DepCapture ix f) m = DepServer ix f m
```

(We need the `DepServer`

newtype wrapper because we are not allowed to have a polymorphic type as the right hand side of a type family.)

In the router we attempt to parse the index; if this succeeds, we unwrap the existential, discovering the type index we need for the rest of the server, use the `HasDepServer`

type class to get a `HasServer`

instance for this particular type index, and continue as usual:

```
route Proxy (DepServer subserver) request respond =
case processedPathInfo request of
(p:ps) ->
case fromText p :: Maybe (Some ix) of
Nothing ->
respond $ failWith NotFound
Just (Some (p' :: ix a)) ->
case hasDepServer (Proxy :: Proxy f) p' of
Dict -> route (Proxy :: Proxy (Apply f a))
(subserver p')
request{ pathInfo = ps }
respond
_ ->
respond $ failWith NotFound
```

## Wrapping up

The hard work is now done. We can define our server in a straight-forward fashion:

```
server :: Server API
server = DepServer serveNext
serveNext :: T a -> Server (Apply Next a)
serveNext TStr a = return (a ++ "1")
serveNext TInt a = return (a + 1)
```

The full development is available from GitHub if you want to play with it. Note that the way we set things up defining dependent servers does not incur a lot of overhead; the use of the `Apply`

type family avoids the need for newtype wrappers, and providing `HasDepServer`

instances will typically be very simple.