servant-0.18.1: A family of combinators for defining webservices APIs
Safe HaskellNone
LanguageHaskell2010

Servant.API.TypeLevel

Description

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
Synopsis

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 ... Source #

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 Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

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 ... Source #

Append two type-level lists.

Equations

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

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

Equations

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

type Elem e es = ElemGo e es es Source #

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 ... Source #

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 ... Source #

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 ... Source #

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

Equations

And () () = ()