Safe Haskell | Safe-Inferred |
---|
Motivation
The purpose of the wai-routing
package is to facilitate the
convenient definition of safe WAI Application
s. Here safety
means that a handler can declare all pre-conditions which must be
fulfilled such that the handler can produce a successful response (excluding
the request body). It is then statically guaranteed that the handler will not be
invoked if any of these pre-conditions fails.
Introduction
The wai-routing
package defines a Boolean
type
which carries -- in addition to actual truth values T
and F
-- meta-data for each case:
data Boolean f t = F f | T Delta t deriving (Eq, Show)
Delta
can in most instances be ignored, i.e. set to 0.
Its purpose is as a measure of distance for those predicates which evaluate
to T
but some may be "closer" in some way than others. An
example is for instance HTTP content-negotiations (cf.
Accept
)
In addition there is a type-class Predicate
defined which
contains an evaluation function apply
, where the
predicate instance is applied to some value, yielding T
or F
.
class Predicate p a where type FVal p type TVal p apply :: p -> a -> Boolean (FVal p) (TVal p)
All predicates are instances of this type-class, which does not
specify the type against which the predicate is evaluated, nor the types
of actual meta-data for the true/false case of the Boolean returned.
WAI related predicates are defined against Req
which holds a regular Request
and path capture variables.
In case predicates fail, they return a status code and an optional message.
Besides these type definitions, there are some ways to connect two
predicates to form a new one as the logical OR
or the
logical AND
of its parts. These are:
In addition to evaluating to T
or F
depending on the truth values of
its parts, these connectives also propagate the meta-data and Delta
appropriately.
If :&:
evaluates to F
it has to combine the meta-data of both predicates,
and it uses the product type :::
for this.
This type also has a data constructor with the same symbol, so one can
combine many predicates without having to nest the meta-data pairs.
In the OR
case, the two predicates have potentially meta-data of
different types, so we use a sum type Either
whenever we combine
two predicates with :||:
. For convenience a type-alias
:+:
is defined for Either
, which allows simple infix
notation. However, for the common case where both predicates have
meta-data of the same type, there is often no need to distinguish which
OR
-branch was true. In this case, the :|:
combinator can be used.
Finally there are Const
and
Fail
to always evaluate to T
or F
respectively.
As an example of how these operators are used, see below in section "Routes".
Example Predicate
newtype Query = Query ByteString instance Predicate Query Req where type FVal Query = Error type TVal Query = ByteString apply (Query x) r = case lookupQuery x r of [] -> F (Error 400 (Just $ "Expected parameter '" <> x <> "'.")) (v:_) -> T [] v
This is a simple example looking for the existence of a Req
query
parameter with the given name. In the success case, the query value is
returned.
As mentioned before, WAI predicates usually fix the type a
from
Predicate
above to Req
. The associated
types FVal
and
TVal
denote the meta-data
types of the predicate. In this example, the meta-date type is
ByteString
. The F
-case is Error
which contains a status code and an optional message.
Routes
So how are Predicate
s used in an application?
One way is to just evaluate them against a given request, e.g.
someHandler :: Application someHandler r = case apply (accept :&: query "baz") (fromWaiRequest [] r) of T ((_ :: Media "text" "plain") ::: bazValue) -> ... F (Just (Error st msg)) -> ... F Nothing -> ...
This however requires the manual construction of a Req
and
for brevity we did not provide the list of captured path parameters.
The intended application of wai-routing
is to declare route definitions with the
Routes
monad which can be turned into a WAI Application
generalised from IO to arbitrary Monad
s through route
.
This application will at runtime select the actual handler to invoke (using the wai-route
library).
sitemap :: Routes () sitemap = do get "/a" handlerA $ accept :&: (query "name" :|: query "nick") :&: query "foo" get "/b" handlerB $ accept :&: (query "name" :||: query "nick") :&: query "foo" get "/c" handlerC $ failure (Error 410 (Just "Gone.")) post "/d" handlerD $ accept post "/e" handlerE $ accept
Handler definitions encode their pre-conditions in their type-signature:
handlerA :: Media "application" "json" ::: ByteString ::: ByteString -> IO Response handlerB :: Media "text" "plain" ::: (ByteString :+: ByteString) ::: ByteString -> IO Response handlerC :: Media "application" "json" ::: Char -> IO Response handlerD :: Media "application" "x-protobuf" -> IO Response handlerE :: Media "application" "xml" -> IO Response
The type-declaration of a handler has to match the corresponding predicate,
i.e. the type of the predicate's T
meta-data value.
One thing to note is that Fail
works with
all T
meta-data types which is safe because the handler is never
invoked, or Fail
is used in some logical disjunction.