What are all the mechanisms used to enable Servant's type-based API?

Question

I'm very puzzled by how Servant is able to achieve the magic that it does using typing. The example on the web site already puzzles me greatly:

type MyAPI = "date" :> Get '[JSON] Date
        :<|> "time" :> Capture "tz" Timezone :> Get '[JSON] Time

I get the "date", "time", [JSON] and "tz" are type-level literals. They are values that have "become" types. Okay.

I get that :> and :<|> are type operators. Okay.

I don't get how these things, after they've become types, can be extracted back out into values. What's the mechanism to do this?

I also don't get how the first part of this type can get the framework to expect a function of the signature IO Date, or how the second part of this type can get the framework to expect a function of the signature Timezone -> IO Time from me. How does this transformation happen?

And how then can the framework call a function for which it didn't initially know the type?

I'm sure there are a number of GHC extensions and unique features at play here that I'm not familiar with that combine to make this magic happen.

Can someone explain what features are involved here and how they are working together?

Answer 1

Looking at the Servant paper for a full explanation may be the best option. Nevertheless, I'll try to illustrate the approach taken by Servant here, by implementing "TinyServant", a version of Servant reduced to the bare minimum.

Sorry that this answer is so long. However, it's still a bit shorter than the paper, and the code discussed here is "only" 81 lines, available also as a Haskell file here.

Preparations

To start, here are the language extensions we'll need:

{-# LANGUAGE DataKinds, PolyKinds, TypeOperators #-}
{-# LANGUAGE TypeFamilies, FlexibleInstances, ScopedTypeVariables #-}
{-# LANGUAGE InstanceSigs #-}

The first three are needed for the definition of the type-level DSL itself. The DSL makes use of type-level strings (DataKinds) and also uses kind polymorphism (PolyKinds). The use of the type-level infix operators such as :<|> and :> requires the TypeOperators extension.

The second three are needed for the definition of the interpretation (we'll define something reminiscent of what a web server does, but without the whole web part). For this, we need type-level functions (TypeFamilies), some type class programming which will require (FlexibleInstances), and some type annotations to guide the type checker which require ScopedTypeVariables.

Purely for documentation purposes, we also use InstanceSigs.

Here's our module header:

module TinyServant where

import Control.Applicative
import GHC.TypeLits
import Text.Read
import Data.Time

After these preliminaries, we're ready to get going.

API specifications

The first ingredient is to define the datatypes that are being used for the API specifications.

data Get (a :: *)

data a :<|> b = a :<|> b
infixr 8 :<|>

data (a :: k) :> (b :: *)
infixr 9 :>

data Capture (a :: *)

We define only four constructs in our simplified language:

1. A Get a represents and endpoint of type a (of kind *). In comparison with full Servant, we ignore content types here. We need the datatype only for the API specifications. There are now directly corresponding values, and hence there is no constructor for Get.

2. With a :<|> b, we represent the choice between two routes. Again, we wouldn't need a constructor, but it turns out that we'll use a pair of handlers to represent the handler of an API using :<|>. For nested applications of :<|>, we'd get nested pairs of handlers, which look somewhat ugly using the standard notation in Haskell, so we define the :<|> constructor to be equivalent to a pair.

3. With item :> rest, we represent nested routes, where item is the first component and rest are the remaining components. In our simplified DSL, there are just two possibilities for item: a type-level string, or a Capture. Because type-level strings are of kind Symbol, but a Capture, defined below is of kind *, we make the first argument of :> kind-polymorphic, so that both options are accepted by the Haskell kind system.

4. A Capture a represents a route component that is captured, parsed and then exposed to the handler as a parameter of type a. In full Servant, Capture has an additional string as a parameter that is used for documentation generation. We omit the string here.

Example API

We can now write down a version of the API specification from the question, adapted to the actual types occuring in Data.Time, and to our simplified DSL:

type MyAPI = "date" :> Get Day
        :<|> "time" :> Capture TimeZone :> Get ZonedTime

Interpretation as server

The most interesting aspect is of course what we can do with the API, and that's also mostly what the question is about.

Servant defines several interpretations, but they all follow a similar pattern. We'll define one here, which is inspired by the interpretation as a web server.

In Servant, the serve function takes a proxy for the API type and a handler matching the API type to a WAI Application, which is essentially a function from HTTP requests to responses. We'll abstract from the web part here, and define

serve :: HasServer layout
      => Proxy layout -> Server layout -> [String] -> IO String

instead.

The HasServer class, which we'll define below, has instances for all the different constructs of the type-level DSL and therefore encodes what it means for a Haskell type layout to be interpretable as an API type of a server.

The Proxy makes a connection between the type and the value level. It's defined as

data Proxy a = Proxy

and its only purpose is that by passing in a Proxy constructor with an explicitly specified type, we can make it very explicit for what API type we want to compute the server.

The Server argument is the handler for the API. Here, Server itself is a type family, and computes from the API type the type that the handler(s) must have. This is one core ingredient of what makes Servant work correctly.

The list of strings represents the request, reduced to a list of URL components. As a result, we always return a String response, and we allow the use of IO. Full Servant uses somewhat more complicated types here, but the idea is the same.

The Server type family

We define Server as a type family first. (In Servant, the actual type family being used is ServerT, and it is defined as part of the HasServer class.)

type family Server layout :: *

The handler for a Get a endpoint is simply an IO action producing an a. (Once again, in the full Servant code, we have slightly more options, such as producing an error.)

type instance Server (Get a) = IO a

The handler for a :<|> b is a pair of handlers, so we could define

type instance Server (a :<|> b) = (Server a, Server b) -- preliminary

But as indicated above, for nested occurrences of :<|> this leads to nested pairs, which look somewhat nicer with an infix pair constructor, so Servant instead defines the equivalent

type instance Server (a :<|> b) = Server a :<|> Server b

It remains to explain how each of the path components is handled.

Literal strings in the routes do not affect the type of the handler:

type instance Server ((s :: Symbol) :> r) = Server r

A capture, however, means that the handler expects an additional argument of the type being captured:

type instance Server (Capture a :> r) = a -> Server r

Computing the handler type of the example API

If we expand Server MyAPI, we obtain

Server MyAPI ~ Server ("date" :> Get Day
                  :<|> "time" :> Capture TimeZone :> Get ZonedTime)
             ~      Server ("date" :> Get Day)
               :<|> Server ("time" :> Capture TimeZone :> Get ZonedTime)
             ~      Server (Get Day)
               :<|> Server ("time" :> Capture TimeZone :> Get ZonedTime)
             ~      IO Day
               :<|> Server ("time" :> Capture TimeZone :> Get ZonedTime)
             ~      IO Day
               :<|> Server (Capture TimeZone :> Get ZonedTime)
             ~      IO Day
               :<|> TimeZone -> Server (Get ZonedTime)
             ~      IO Day
               :<|> TimeZone -> IO ZonedTime

So as intended, the server for our API requires a pair of handlers, one that provides a date, and one that, given a time zone, provides a time. We can define these right now:

handleDate :: IO Day
handleDate = utctDay <$> getCurrentTime

handleTime :: TimeZone -> IO ZonedTime
handleTime tz = utcToZonedTime tz <$> getCurrentTime

handleMyAPI :: Server MyAPI
handleMyAPI = handleDate :<|> handleTime

The HasServer class

We still have to implement the HasServer class, which looks as follows:

class HasServer layout where
  route :: Proxy layout -> Server layout -> [String] -> Maybe (IO String)

The task of the function route is almost like serve. Internally, we have to dispatch an incoming request to the right router. In the case of :<|>, this means we have to make a choice between two handlers. How do we make this choice? A simple option is to allow route to fail, by returning a Maybe. (Again, full Servant is somewhat more sophisticated here, and version 0.5 will have a much improved routing strategy.)

Once we have route defined, we can easily define serve in terms of route:

serve :: HasServer layout
      => Proxy layout -> Server layout -> [String] -> IO String
serve p h xs = case route p h xs of
  Nothing -> ioError (userError "404")
  Just m  -> m

If none of the routes match, we fail with a 404. Otherwise, we return the result.

The HasServer instances

For a Get endpoint, we defined

type instance Server (Get a) = IO a

so the handler is an IO action producing an a, which we have to turn into a String. We use show for this purpose. In the actual Servant implementation, this conversion is handled by the content types machinery, and will typically involve encoding to JSON or HTML.

instance Show a => HasServer (Get a) where
  route :: Proxy (Get a) -> IO a -> [String] -> Maybe (IO String)
  route _ handler [] = Just (show <$> handler)
  route _ _       _  = Nothing

Since we're matching an endpoint only, the require the request to be empty at this point. If it isn't, this route does not match and we return Nothing.

Let's look at choice next:

instance (HasServer a, HasServer b) => HasServer (a :<|> b) where
  route :: Proxy (a :<|> b) -> (Server a :<|> Server b) -> [String] -> Maybe (IO String)
  route _ (handlera :<|> handlerb) xs =
        route (Proxy :: Proxy a) handlera xs
    <|> route (Proxy :: Proxy b) handlerb xs

Here, we get a pair of handlers, and we use <|> for Maybe to try both.

What happens for a literal string?

instance (KnownSymbol s, HasServer r) => HasServer ((s :: Symbol) :> r) where
  route :: Proxy (s :> r) -> Server r -> [String] -> Maybe (IO String)
  route _ handler (x : xs)
    | symbolVal (Proxy :: Proxy s) == x = route (Proxy :: Proxy r) handler xs
  route _ _       _                     = Nothing

The handler for s :> r is of the same type as the handler for r. We require the request to be non-empty and the first component to match the value-level counterpart of the type-level string. We obtain the value-level string corresponding to the type-level string literal by applying symbolVal. For this, we need a KnownSymbol constraint on the type-level string literal. But all concrete literals in GHC are automatically an instance of KnownSymbol.

The final case is for captures:

instance (Read a, HasServer r) => HasServer (Capture a :> r) where
  route :: Proxy (Capture a :> r) -> (a -> Server r) -> [String] -> Maybe (IO String)
  route _ handler (x : xs) = do
    a <- readMaybe x
    route (Proxy :: Proxy r) (handler a) xs
  route _ _       _        = Nothing

In this case, we can assume that our handler is actually a function that expects an a. We require the first component of the request to be parseable as an a. Here, we use Read, whereas in Servant, we use the content type machinery again. If reading fails, we consider the request not to match. Otherwise, we can feed it to the handler and continue.

Testing everything

Now we're done.

We can confirm that everything works in GHCi:

GHCi> serve (Proxy :: Proxy MyAPI) handleMyAPI  ["time", "CET"]
"2015-11-01 20:25:04.594003 CET"
GHCi> serve (Proxy :: Proxy MyAPI) handleMyAPI  ["time", "12"]
*** Exception: user error (404)
GHCi> serve (Proxy :: Proxy MyAPI) handleMyAPI  ["date"]
"2015-11-01"
GHCi> serve (Proxy :: Proxy MyAPI) handleMyAPI  []
*** Exception: user error (404)