Safe Haskell | None |
---|---|
Language | Haskell2010 |
Servant.API.TypeLevel
Contents
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 ...
- type family FragmentUnique api :: Constraint where ...
- class FragmentUnique api => AtLeastOneFragment api
Documentation
The doctests in this module are run with following preamble:
>>>
:set -XPolyKinds
>>>
:set -XGADTs
>>>
:set -XTypeSynonymInstances -XFlexibleInstances
>>>
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
>>>
type FailAPI = Fragment Bool :> Fragment Int :> Get '[JSON] NoContent
>>>
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
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
that are optional in a URI and do not affect them if they are
omitted.
QueryParam
>>>
data CustomThing
>>>
type instance IsElem' e (CustomThing :> s) = IsElem e s
Note that
is called, which will mutually recurse back to
IsElem
if it exhausts all other options again.
IsElem'
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
if it exhausts all other options.
IsElem'
>>>
ok (Proxy :: Proxy (IsElem ("hello" :> Get '[JSON] Int) SampleAPI))
OK
>>>
ok (Proxy :: Proxy (IsElem ("bye" :> Get '[JSON] Int) SampleAPI))
... ... Could not ... ...
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 bya
would match the URL represented byb
, *not* whether a request represented bya
matches the endpoints servingb
(for the latter, useIsIn
).
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 sa ( Fragment 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 ... ...
This uses
IsElem
for checking; thus the note there applies here.
type family AllIsElem xs api :: Constraint where ... Source #
Check that every element of
xs
is an endpoint of
api
(using
).
IsElem
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 ... ...
type family IsStrictSubAPI sub api :: Constraint where ... Source #
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
Helpers
Lists
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 #
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 #
Logic
type family Or (a :: Constraint ) (b :: Constraint ) :: Constraint where ... Source #
If either a or b produce an empty constraint, produce an empty constraint.
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 () () = () |
Fragment
type family FragmentUnique api :: Constraint where ... Source #
Equations
FragmentUnique (sa :<|> sb) = And ( FragmentUnique sa) ( FragmentUnique sb) | |
FragmentUnique ( Fragment a :> sa) = FragmentNotIn sa ( Fragment a :> sa) | |
FragmentUnique (x :> sa) = FragmentUnique sa | |
FragmentUnique ( Fragment a) = () | |
FragmentUnique x = () |
class FragmentUnique api => AtLeastOneFragment api Source #
Instances
AtLeastOneFragment ( Fragment a) Source # | |
Defined in Servant.API.TypeLevel |
|
AtLeastOneFragment ( UVerb m cts as) Source # | |
Defined in Servant.API.TypeLevel |
|
AtLeastOneFragment ( Verb m s ct typ) Source # |
If fragment appeared in API endpoint twice, compile-time error would be raised.
|
Defined in Servant.API.TypeLevel |