Dependently typed servers in Servant

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., Strings and Ints 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.