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.