Merge pull request #345 from haskell-servant/fizruk/type-level-#305
Servant.API.TypeLevel
This commit is contained in:
Oleg Grenrus
GitHub
commit
555b60ea06
6 changed files with 276 additions and 80 deletions
|
|
@ -37,12 +37,11 @@ import Data.Ord (comparing)
|
|||
import Data.Proxy (Proxy(Proxy))
|
||||
import Data.String.Conversions (cs)
|
||||
import Data.Text (Text, unpack)
|
||||
import GHC.Exts (Constraint)
|
||||
import GHC.Generics
|
||||
import GHC.TypeLits
|
||||
import Servant.API
|
||||
import Servant.API.ContentTypes
|
||||
import Servant.Utils.Links
|
||||
import Servant.API.TypeLevel
|
||||
|
||||
import qualified Data.HashMap.Strict as HM
|
||||
import qualified Data.Text as T
|
||||
|
|
@ -306,15 +305,6 @@ docs p = docsWithOptions p defaultDocOptions
|
|||
docsWithOptions :: HasDocs api => Proxy api -> DocOptions -> API
|
||||
docsWithOptions p = docsFor p (defEndpoint, defAction)
|
||||
|
||||
-- | Closed type family, check if endpoint is exactly within API.
|
||||
|
||||
-- We aren't sure what affects how an Endpoint is built up, so we require an
|
||||
-- exact match.
|
||||
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 = ()
|
||||
|
||||
-- | Create an 'ExtraInfo' that is guaranteed to be within the given API layout.
|
||||
--
|
||||
-- The safety here is to ensure that you only add custom documentation to an
|
||||
|
|
|
|||
|
|
@ -16,11 +16,11 @@ import Data.Proxy
|
|||
import Data.String
|
||||
import Data.Text
|
||||
import Data.Text.Encoding (decodeUtf8)
|
||||
import GHC.Exts (Constraint)
|
||||
import GHC.TypeLits
|
||||
import qualified Network.HTTP.Types as HTTP
|
||||
import Prelude hiding (concat)
|
||||
import Servant.API
|
||||
import Servant.API.TypeLevel
|
||||
|
||||
|
||||
newtype FunctionName = FunctionName { unFunctionName :: [Text] }
|
||||
|
|
@ -135,15 +135,6 @@ makeLenses ''Req
|
|||
defReq :: Req ftype
|
||||
defReq = Req defUrl "GET" [] Nothing Nothing (FunctionName [])
|
||||
|
||||
-- | To be used exclusively as a "negative" return type/constraint
|
||||
-- by @'Elem`@ type family.
|
||||
class NotFound
|
||||
|
||||
type family Elem (a :: *) (ls::[*]) :: Constraint where
|
||||
Elem a '[] = NotFound
|
||||
Elem a (a ': list) = ()
|
||||
Elem a (b ': list) = Elem a list
|
||||
|
||||
-- | 'HasForeignType' maps Haskell types with types in the target
|
||||
-- language of your backend. For example, let's say you're
|
||||
-- implementing a backend to some language __X__, and you want
|
||||
|
|
|
|||
|
|
@ -8,6 +8,10 @@
|
|||
use its `ToHttpApiData` instance or `linkURI`.
|
||||
([#527](https://github.com/haskell-servant/servant/issues/527))
|
||||
|
||||
* Add `Servant.API.TypeLevel` module with type families to work with API types.
|
||||
([#345](https://github.com/haskell-servant/servant/pull/345))
|
||||
([#305](https://github.com/haskell-servant/servant/issues/305))
|
||||
|
||||
0.9.1
|
||||
------
|
||||
|
||||
|
|
@ -24,6 +28,8 @@
|
|||
----
|
||||
|
||||
* Add `CaptureAll` combinator. Captures all of the remaining segments in a URL.
|
||||
* Add `Servant.API.TypeLevel` module, with frequently used type-level
|
||||
functionaliy.
|
||||
|
||||
0.8
|
||||
---
|
||||
|
|
|
|||
|
|
@ -47,6 +47,7 @@ library
|
|||
Servant.API.ReqBody
|
||||
Servant.API.ResponseHeaders
|
||||
Servant.API.Sub
|
||||
Servant.API.TypeLevel
|
||||
Servant.API.Vault
|
||||
Servant.API.Verbs
|
||||
Servant.API.WithNamedContext
|
||||
|
|
|
|||
264
servant/src/Servant/API/TypeLevel.hs
Normal file
264
servant/src/Servant/API/TypeLevel.hs
Normal file
|
|
@ -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
|
||||
|
|
@ -6,7 +6,6 @@
|
|||
{-# LANGUAGE ScopedTypeVariables #-}
|
||||
{-# LANGUAGE TypeFamilies #-}
|
||||
{-# LANGUAGE TypeOperators #-}
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
{-# OPTIONS_HADDOCK not-home #-}
|
||||
|
||||
-- | Type safe generation of internal links.
|
||||
|
|
@ -79,6 +78,8 @@
|
|||
-- bad_link under api after trying the open (but empty) type family
|
||||
-- `IsElem'` as a last resort.
|
||||
module Servant.Utils.Links (
|
||||
module Servant.API.TypeLevel,
|
||||
|
||||
-- * Building and using safe links
|
||||
--
|
||||
-- | Note that 'URI' is Network.URI.URI from the network-uri package.
|
||||
|
|
@ -88,10 +89,6 @@ module Servant.Utils.Links (
|
|||
, HasLink(..)
|
||||
, linkURI
|
||||
, Link
|
||||
, IsElem'
|
||||
-- * Illustrative exports
|
||||
, IsElem
|
||||
, Or
|
||||
) where
|
||||
|
||||
import Data.List
|
||||
|
|
@ -99,7 +96,6 @@ import Data.Monoid.Compat ( (<>) )
|
|||
import Data.Proxy ( Proxy(..) )
|
||||
import qualified Data.Text as Text
|
||||
import qualified Data.Text.Encoding as TE
|
||||
import GHC.Exts (Constraint)
|
||||
import GHC.TypeLits ( KnownSymbol, symbolVal )
|
||||
import Network.URI ( URI(..), escapeURIString, isUnreserved )
|
||||
import Prelude ()
|
||||
|
|
@ -115,7 +111,7 @@ import Servant.API.RemoteHost ( RemoteHost )
|
|||
import Servant.API.Verbs ( Verb )
|
||||
import Servant.API.Sub ( type (:>) )
|
||||
import Servant.API.Raw ( Raw )
|
||||
import Servant.API.Alternative ( type (:<|>) )
|
||||
import Servant.API.TypeLevel
|
||||
|
||||
-- | A safe link datatype.
|
||||
-- The only way of constructing a 'Link' is using 'safeLink', which means any
|
||||
|
|
@ -131,58 +127,6 @@ instance ToHttpApiData Link where
|
|||
let uri = linkURI l
|
||||
in Text.pack $ uriPath uri ++ uriQuery uri
|
||||
|
||||
-- | 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 () () = ()
|
||||
|
||||
-- | 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
|
||||
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 (Capture z y :> sa) (Capture x y :> sb)
|
||||
= IsElem sa sb
|
||||
IsElem (CaptureAll z y :> sa) (CaptureAll 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 IsSubList a b :: Constraint where
|
||||
IsSubList '[] b = ()
|
||||
IsSubList (x ': xs) y = Elem x y `And` IsSubList xs y
|
||||
|
||||
type family Elem e es :: Constraint where
|
||||
Elem x (x ': xs) = ()
|
||||
Elem y (x ': xs) = Elem y xs
|
||||
|
||||
-- Phantom types for Param
|
||||
data Query
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue