Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #345 from haskell-servant/fizruk/type-level-#305
Servant.API.TypeLevel
- Loading branch information
Showing
6 changed files
with
276 additions
and
80 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,264 @@ | ||
{-# LANGUAGE CPP #-} | ||
{-# LANGUAGE ConstraintKinds #-} | ||
{-# LANGUAGE DataKinds #-} | ||
{-# LANGUAGE KindSignatures #-} | ||
{-# LANGUAGE MultiParamTypeClasses #-} | ||
{-# LANGUAGE PolyKinds #-} | ||
{-# LANGUAGE TypeFamilies #-} | ||
{-# LANGUAGE TypeOperators #-} | ||
{-# LANGUAGE UndecidableInstances #-} | ||
|
||
{-| | ||
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 | ||
-} | ||
module Servant.API.TypeLevel ( | ||
-- $setup | ||
-- * API predicates | ||
Endpoints, | ||
-- ** Lax inclusion | ||
IsElem', | ||
IsElem, | ||
IsSubAPI, | ||
AllIsElem, | ||
-- ** Strict inclusion | ||
IsIn, | ||
IsStrictSubAPI, | ||
AllIsIn, | ||
-- * Helpers | ||
-- ** Lists | ||
MapSub, | ||
AppendList, | ||
IsSubList, | ||
Elem, | ||
ElemGo, | ||
-- ** Logic | ||
Or, | ||
And, | ||
-- * Custom type errors | ||
-- | Before @base-4.9.0.0@ we use non-exported 'ElemNotFoundIn' class, | ||
-- which cannot be instantiated. | ||
) where | ||
|
||
|
||
import GHC.Exts (Constraint) | ||
import Servant.API.Alternative (type (:<|>)) | ||
import Servant.API.Capture (Capture, CaptureAll) | ||
import Servant.API.Header (Header) | ||
import Servant.API.QueryParam (QueryFlag, QueryParam, QueryParams) | ||
import Servant.API.ReqBody (ReqBody) | ||
import Servant.API.Sub (type (:>)) | ||
import Servant.API.Verbs (Verb) | ||
#if MIN_VERSION_base(4,9,0) | ||
import GHC.TypeLits (TypeError, ErrorMessage(..)) | ||
#endif | ||
|
||
|
||
|
||
-- * API predicates | ||
|
||
-- | 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 | ||
type family Endpoints api where | ||
Endpoints (a :<|> b) = AppendList (Endpoints a) (Endpoints b) | ||
Endpoints (e :> a) = MapSub e (Endpoints a) | ||
Endpoints a = '[a] | ||
|
||
-- ** Lax inclusion | ||
|
||
-- | 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' a s :: Constraint | ||
|
||
-- | 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'). | ||
type family IsElem endpoint api :: Constraint where | ||
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 | ||
|
||
-- | 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. | ||
type family IsSubAPI sub api :: Constraint where | ||
IsSubAPI sub api = AllIsElem (Endpoints sub) api | ||
|
||
-- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsElem'@). | ||
type family AllIsElem xs api :: Constraint where | ||
AllIsElem '[] api = () | ||
AllIsElem (x ': xs) api = (IsElem x api, AllIsElem xs api) | ||
|
||
-- ** Strict inclusion | ||
|
||
-- | 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... | ||
-- ... | ||
type family IsIn (endpoint :: *) (api :: *) :: Constraint where | ||
IsIn e (sa :<|> sb) = Or (IsIn e sa) (IsIn e sb) | ||
IsIn (e :> sa) (e :> sb) = IsIn sa sb | ||
IsIn e e = () | ||
|
||
-- | Check whether @sub@ is a sub API of @api@. | ||
-- | ||
-- Like 'IsSubAPI', but uses 'IsIn' rather than 'IsElem'. | ||
type family IsStrictSubAPI sub api :: Constraint where | ||
IsStrictSubAPI sub api = AllIsIn (Endpoints sub) api | ||
|
||
-- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsIn'@). | ||
-- | ||
-- ok (Proxy :: Proxy (AllIsIn (Endpoints SampleAPI) SampleAPI)) | ||
-- OK | ||
type family AllIsIn xs api :: Constraint where | ||
AllIsIn '[] api = () | ||
AllIsIn (x ': xs) api = (IsIn x api, AllIsIn xs api) | ||
|
||
-- * Helpers | ||
|
||
-- ** Lists | ||
|
||
-- | Apply @(e :>)@ to every API in @xs@. | ||
type family MapSub e xs where | ||
MapSub e '[] = '[] | ||
MapSub e (x ': xs) = (e :> x) ': MapSub e xs | ||
|
||
-- | Append two type-level lists. | ||
type family AppendList xs ys where | ||
AppendList '[] ys = ys | ||
AppendList (x ': xs) ys = x ': AppendList xs ys | ||
|
||
type family IsSubList a b :: Constraint where | ||
IsSubList '[] b = () | ||
IsSubList (x ': xs) y = Elem x y `And` IsSubList xs y | ||
|
||
-- | 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 Elem e es = ElemGo e es es | ||
|
||
-- 'orig' is used to store original list for better error messages | ||
type family ElemGo e es orig :: Constraint where | ||
ElemGo x (x ': xs) orig = () | ||
ElemGo y (x ': xs) orig = ElemGo y xs orig | ||
#if MIN_VERSION_base(4,9,0) | ||
-- Note [Custom Errors] | ||
ElemGo x '[] orig = TypeError ('ShowType x | ||
':<>: 'Text " expected in list " | ||
':<>: 'ShowType orig) | ||
#else | ||
ElemGo x '[] orig = ElemNotFoundIn x orig | ||
#endif | ||
|
||
-- ** Logic | ||
|
||
-- | If either a or b produce an empty constraint, produce an empty constraint. | ||
type family Or (a :: Constraint) (b :: Constraint) :: Constraint where | ||
-- This works because of: | ||
-- https://ghc.haskell.org/trac/ghc/wiki/NewAxioms/CoincidentOverlap | ||
Or () b = () | ||
Or a () = () | ||
|
||
-- | If both a or b produce an empty constraint, produce an empty constraint. | ||
type family And (a :: Constraint) (b :: Constraint) :: Constraint where | ||
And () () = () | ||
|
||
-- * Custom type errors | ||
|
||
#if !MIN_VERSION_base(4,9,0) | ||
class ElemNotFoundIn val list | ||
#endif | ||
|
||
{- Note [Custom Errors] | ||
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ | ||
We might try to factor these our more cleanly, but the type synonyms and type | ||
families are not evaluated (see https://ghc.haskell.org/trac/ghc/ticket/12048). | ||
-} | ||
|
||
|
||
-- $setup | ||
-- | ||
-- 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 |
Oops, something went wrong.