# Dependently typed servers in Servant

Wednesday, 02 December 2015, by Edsko de Vries, Andres Löh.

Filed under coding.

Suppose we have a webserver that can perform different kinds of operations on different kinds of values. Perhaps it can reverse or capitalize strings, and increment or negate integers:

```
# curl http://localhost:8081/example/reverse
elpmaxe
# curl http://localhost:8081/example/caps
EXAMPLE
# curl http://localhost:8081/1234/inc
1235
# curl http://localhost:8081/1234/neg
-1234
```

Moreover, it can echo back any value:

```
# curl http://localhost:8081/example/echo
example
# curl http://localhost:8081/1234/echo
1234
```

However, it does not make sense to try to reverse an integer or increment a string; requesting either of

```
http://localhost:8081/1234/reverse
http://localhost:8081/example/inc
```

should result in HTTP error.

This is an example of a dependently typed server: the value that we are given as input determines the type of the rest of the server. If we get a string as input, we expect a string operation as the second argument and the response is also a string; if we get an integer as input, we expect an integer operation as the second argument and the response is also an integer.

We can encode the type of values that are either strings or integers using the GADT

```
data Value :: * -> * where
VStr :: Text -> Value Text
VInt :: Int -> Value Int
```

and the type of operations on a particular kind of value as

```
data Op :: * -> * where
OpEcho :: Op a
OpReverse :: Op Text
OpCaps :: Op Text
OpInc :: Op Int
OpNeg :: Op Int
```

The core of our server will be:

```
execOp :: Value a -> Op a -> Value a
execOp val OpEcho = val
execOp (VStr str) OpReverse = VStr $ Text.reverse str
execOp (VStr str) OpCaps = VStr $ Text.toUpper str
execOp (VInt i) OpInc = VInt $ i + 1
execOp (VInt i) OpNeg = VInt $ negate i
```

Note that the type of `execOp`

reflects precisely that the type of the input matches both the type of the operation we’re applying and the type of the result.

In the remainder of this blog post we will explain which combinators we need to add to Servant to be able to define such a dependently typed webserver. We will assume familiarity with the implementation of 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

Consider parsing a `Value`

; what would be the type of

`fromText :: Text -> Value ???`

Clearly, the type argument to `Value`

here depends on the actual run-time value of the `Text`

. Since we do not know this type argument before parsing, we need to hide it in an existential. We can define a general existential wrapper as

```
data Some :: (* -> *) -> * where
Some :: f a -> Some f
```

We can then define a `FromText`

instance as follows:

```
instance FromText (Some Value) where
fromText t = Just $ case readMaybe (Text.unpack t) of
Just n -> Some $ VInt n
Nothing -> Some $ VStr t
```

### Reified dictionaries

Consider trying to convince the type checker that all values (i.e., `String`

s and `Int`

s in our running example) admit an equality test. One way to do this is to use reified type class dictionaries:

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

Using `Dict`

we can define

```
valueEq :: Value a -> Dict (Eq a)
valueEq (VStr _) = Dict
valueEq (VInt _) = Dict
```

The first use of `Dict`

in `valueEq`

captures the in-scope `Eq String`

constraint, and the second use captures the in-scope `Eq Int`

constraint. We can bring these constraints back into scope by pattern matching:

```
useEq :: Dict (Eq a) -> a -> a -> Bool
useEq Dict = (==)
```

### Simulating type-level lambda

In order to define the type dependency in the webserver we will need a type level function *f* that says “if the input has type *a*, then the remainder of the server has type *f a*”. We might try to use a type synonym for this:

```
type ExecOp a = Capture "op" (Op a)
:> Get '[PlainText] (Value a)
```

Unfortunately, we will need to be able to refer to `ExecOp`

without an argument, which is not possible in Haskell: type synonyms must always be fully applied. We could use a `newtype`

, but that will lead to other headaches (`HasServer`

cannot be derived).

Instead, we will apply defunctionalization and use a datatype to symbolically denote a particular type-level function, and then use a type family to implement application of the symbolic function to an argument:

```
data ExecOp
type family Apply f a :: *
type instance Apply ExecOp a = Capture "op" (Op a)
:> Get '[PlainText] (Value a)
```

As an example of using `Apply`

, given the definition of `execOp`

above, we can define the following wrapper:

```
serveExecOp :: Value a -> Server (Apply ExecOp a)
serveExecOp val op = return $ execOp val op
```

This use of defunctionalization to simulate type-level lambdas was pioneered in the work on the singletons package (see Promoting Functions to Type Families in Haskell).

## 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 (`Value`

in our running example), and `f`

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

). 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 Value ExecOp where
hasDepServer _ (VStr _) = Dict
hasDepServer _ (VInt _) = Dict
```

In order to show we can construct servers for `ExecOp`

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

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

and `Int`

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

instances for both of

```
Capture "op" (Op String) :> Get '[PlainText] (Value String)
Capture "op" (Op Int) :> Get '[PlainText] (Value Int)
```

both of which we get (almost) for free from Servant. Hence, we can simply pattern match on the index and trivially construct the dictionary. This follows precisely the same strategy as in the `valueEq`

example.

### 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 = DepCapture Value ExecOp`

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. 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

To define the full server, we just need to wrap `serveExecOp`

in the `DepServer`

constructor and we’re done:

```
server :: Server API
server = DepServer serveExecOp
```

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.