Servant.API.TypeLevel

This module collects utilities for manipulating servant API types. The functionality in this module is for advanced usage.

The code samples in this module use the following type synonym:

type SampleAPI = "hello" :> Get '[JSON] Int
            :<|> "bye" :> Capture "name" String :> Post '[JSON, PlainText] Bool

Documentation

The doctests in this module are run with following preamble:

>>> :set -XPolyKinds
>>> :set -XGADTs
>>> import Data.Proxy
>>> import Data.Type.Equality
>>> import Servant.API
>>> data OK ctx where OK :: ctx => OK ctx
>>> instance Show (OK ctx) where show _ = "OK"
>>> let ok :: ctx => Proxy ctx -> OK ctx; ok _ = OK
>>> type SampleAPI = "hello" :> Get '[JSON] Int :<|> "bye" :> Capture "name" String :> Post '[JSON, PlainText] Bool
>>> let sampleAPI = Proxy :: Proxy SampleAPI

type family Endpoints api where ...

Flatten API into a list of endpoints.

>>> Refl :: Endpoints SampleAPI :~: '["hello" :> Verb 'GET 200 '[JSON] Int, "bye" :> (Capture "name" String :> Verb 'POST 200 '[JSON, PlainText] Bool)]
Refl

Equations

Endpoints (a :<|> b) = AppendList (Endpoints a) (Endpoints b)

Endpoints (e :> a) = MapSub e (Endpoints a)

Endpoints a = '[a]

Lax inclusion

type family IsElem' a s :: Constraint

You may use this type family to tell the type checker that your custom type may be skipped as part of a link. This is useful for things like QueryParam that are optional in a URI and do not affect them if they are omitted.

>>> data CustomThing
>>> type instance IsElem' e (CustomThing :> s) = IsElem e s

Note that IsElem is called, which will mutually recurse back to IsElem' if it exhausts all other options again.

Once you have written a HasLink instance for CustomThing you are ready to go.

type family IsElem endpoint api :: Constraint where ...

Closed type family, check if endpoint is within api. Uses IsElem' if it exhausts all other options.

>>> ok (Proxy :: Proxy (IsElem ("hello" :> Get '[JSON] Int) SampleAPI))
OK

>>> ok (Proxy :: Proxy (IsElem ("bye" :> Get '[JSON] Int) SampleAPI))
...
... Could not deduce...
...

An endpoint is considered within an api even if it is missing combinators that don't affect the URL:

>>> ok (Proxy :: Proxy (IsElem (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int)))
OK

>>> ok (Proxy :: Proxy (IsElem (Get '[JSON] Int) (ReqBody '[JSON] Bool :> Get '[JSON] Int)))
OK

• N.B.:* IsElem a b can be seen as capturing the notion of whether the URL represented by a would match the URL represented by b, *not* whether a request represented by a matches the endpoints serving b (for the latter, use IsIn).

Equations

IsElem e (sa :<|> sb) = Or (IsElem e sa) (IsElem e sb)

IsElem (e :> sa) (e :> sb) = IsElem sa sb

IsElem sa (Header sym x :> sb) = IsElem sa sb

IsElem sa (ReqBody y x :> sb) = IsElem sa sb

IsElem (CaptureAll z y :> sa) (CaptureAll x y :> sb) = IsElem sa sb

IsElem (Capture z y :> sa) (Capture x y :> sb) = IsElem sa sb

IsElem sa (QueryParam x y :> sb) = IsElem sa sb

IsElem sa (QueryParams x y :> sb) = IsElem sa sb

IsElem sa (QueryFlag x :> sb) = IsElem sa sb

IsElem (Verb m s ct typ) (Verb m s ct' typ) = IsSubList ct ct'

IsElem e e = ()

IsElem e a = IsElem' e a

type family IsSubAPI sub api :: Constraint where ...

Check whether sub is a sub-API of api.

>>> ok (Proxy :: Proxy (IsSubAPI SampleAPI (SampleAPI :<|> Get '[JSON] Int)))
OK

>>> ok (Proxy :: Proxy (IsSubAPI (SampleAPI :<|> Get '[JSON] Int) SampleAPI))
...
... Could not deduce...
...

This uses IsElem for checking; thus the note there applies here.

Equations

IsSubAPI sub api = AllIsElem (Endpoints sub) api

type family AllIsElem xs api :: Constraint where ...

Check that every element of xs is an endpoint of api (using IsElem).

Equations

AllIsElem '[] api = ()

AllIsElem (x ': xs) api = (IsElem x api, AllIsElem xs api)

Strict inclusion

type family IsIn (endpoint :: *) (api :: *) :: Constraint where ...

Closed type family, check if endpoint is exactly within api.

>>> ok (Proxy :: Proxy (IsIn ("hello" :> Get '[JSON] Int) SampleAPI))
OK

Unlike IsElem, this requires an *exact* match.

>>> ok (Proxy :: Proxy (IsIn (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int)))
...
... Could not deduce...
...

Equations

IsIn e (sa :<|> sb) = Or (IsIn e sa) (IsIn e sb)

IsIn (e :> sa) (e :> sb) = IsIn sa sb

IsIn e e = ()

type family IsStrictSubAPI sub api :: Constraint where ...

Check whether sub is a sub API of api.

Like IsSubAPI, but uses IsIn rather than IsElem.

Equations

IsStrictSubAPI sub api = AllIsIn (Endpoints sub) api

type family AllIsIn xs api :: Constraint where ...

Check that every element of xs is an endpoint of api (using IsIn).

ok (Proxy :: Proxy (AllIsIn (Endpoints SampleAPI) SampleAPI)) OK

Equations

AllIsIn '[] api = ()

AllIsIn (x ': xs) api = (IsIn x api, AllIsIn xs api)

Helpers

Lists

type family MapSub e xs where ...

Apply (e :>) to every API in xs.

Equations

MapSub e '[] = '[]

MapSub e (x ': xs) = (e :> x) ': MapSub e xs

type family AppendList xs ys where ...

Append two type-level lists.

Equations

AppendList '[] ys = ys

AppendList (x ': xs) ys = x ': AppendList xs ys

type family IsSubList a b :: Constraint where ...

Equations

IsSubList '[] b = ()

IsSubList (x ': xs) y = Elem x y `And` IsSubList xs y

type Elem e es = ElemGo e es es

Check that a value is an element of a list:

>>> ok (Proxy :: Proxy (Elem Bool '[Int, Bool]))
OK

>>> ok (Proxy :: Proxy (Elem String '[Int, Bool]))
...
... [Char]...'[Int, Bool...
...

type family ElemGo e es orig :: Constraint where ...

Equations

ElemGo x (x ': xs) orig = ()

ElemGo y (x ': xs) orig = ElemGo y xs orig

ElemGo x '[] orig = TypeError ((ShowType x :<>: Text " expected in list ") :<>: ShowType orig)

Logic

type family Or (a :: Constraint) (b :: Constraint) :: Constraint where ...

If either a or b produce an empty constraint, produce an empty constraint.

Equations

Or () b = ()

Or a () = ()

type family And (a :: Constraint) (b :: Constraint) :: Constraint where ...

If both a or b produce an empty constraint, produce an empty constraint.

Equations

And () () = ()