servant-0.16.2: A family of combinators for defining webservices APIs

Safe Haskell | None
Language | Haskell2010

Servant.API.TypeLevel

Contents

- Lax inclusion
- Strict inclusion
- Helpers
  - Lists
  - Logic

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

- type family Endpoints api where ...
- type family IsElem' a s :: Constraint
- type family IsElem endpoint api :: Constraint where ...
- type family IsSubAPI sub api :: Constraint where ...
- type family AllIsElem xs api :: Constraint where ...
- type family IsIn (endpoint :: *) (api :: *) :: Constraint where ...
- type family IsStrictSubAPI sub api :: Constraint where ...
- type family AllIsIn xs api :: Constraint where ...
- type family MapSub e xs where ...
- type family AppendList xs ys where ...
- type family IsSubList a b :: Constraint where ...
- type Elem e es = ElemGo e es es
- type family ElemGo e es orig :: Constraint where ...
- type family Or (a :: Constraint) (b :: Constraint) :: Constraint where ...
- type family And (a :: Constraint) (b :: Constraint) :: Constraint where ...

# 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 () () = () |