@@ -0,0 +1,264 @@
1+{-# LANGUAGE CPP #-}
2+{-# LANGUAGE ConstraintKinds #-}
3+{-# LANGUAGE DataKinds #-}
4+{-# LANGUAGE KindSignatures #-}
5+{-# LANGUAGE MultiParamTypeClasses #-}
6+{-# LANGUAGE PolyKinds #-}
7+{-# LANGUAGE TypeFamilies #-}
8+{-# LANGUAGE TypeOperators #-}
9+{-# LANGUAGE UndecidableInstances #-}
10+
11+{-|
12+This module collects utilities for manipulating @servant@ API types. The
13+functionality in this module is for advanced usage.
14+
15+The code samples in this module use the following type synonym:
16+
17+> type SampleAPI = "hello" :> Get '[JSON] Int
18+> :<|> "bye" :> Capture "name" String :> Post '[JSON, PlainText] Bool
19+
20+-}
21+module Servant.API.TypeLevel (
22+ -- $setup
23+ -- * API predicates
24+ Endpoints,
25+ -- ** Lax inclusion
26+ IsElem',
27+ IsElem,
28+ IsSubAPI,
29+ AllIsElem,
30+ -- ** Strict inclusion
31+ IsIn,
32+ IsStrictSubAPI,
33+ AllIsIn,
34+ -- * Helpers
35+ -- ** Lists
36+ MapSub,
37+ AppendList,
38+ IsSubList,
39+ Elem,
40+ ElemGo,
41+ -- ** Logic
42+ Or,
43+ And,
44+ -- * Custom type errors
45+ -- | Before @base-4.9.0.0@ we use non-exported 'ElemNotFoundIn' class,
46+ -- which cannot be instantiated.
47+ ) where
48+
49+
50+import GHC.Exts (Constraint)
51+import Servant.API.Alternative (type (:<|>))
52+import Servant.API.Capture (Capture, CaptureAll)
53+import Servant.API.Header (Header)
54+import Servant.API.QueryParam (QueryFlag, QueryParam, QueryParams)
55+import Servant.API.ReqBody (ReqBody)
56+import Servant.API.Sub (type (:>))
57+import Servant.API.Verbs (Verb)
58+#if MIN_VERSION_base(4,9,0)
59+import GHC.TypeLits (TypeError, ErrorMessage(..))
60+#endif
61+
62+
63+
64+-- * API predicates
65+
66+-- | Flatten API into a list of endpoints.
67+--
68+-- >>> Refl :: Endpoints SampleAPI :~: '["hello" :> Verb 'GET 200 '[JSON] Int, "bye" :> (Capture "name" String :> Verb 'POST 200 '[JSON, PlainText] Bool)]
69+-- Refl
70+type family Endpoints api where
71+ Endpoints (a :<|> b) = AppendList (Endpoints a) (Endpoints b)
72+ Endpoints (e :> a) = MapSub e (Endpoints a)
73+ Endpoints a = '[a]
74+
75+-- ** Lax inclusion
76+
77+-- | You may use this type family to tell the type checker that your custom
78+-- type may be skipped as part of a link. This is useful for things like
79+-- @'QueryParam'@ that are optional in a URI and do not affect them if they are
80+-- omitted.
81+--
82+-- >>> data CustomThing
83+-- >>> type instance IsElem' e (CustomThing :> s) = IsElem e s
84+--
85+-- Note that @'IsElem'@ is called, which will mutually recurse back to @'IsElem''@
86+-- if it exhausts all other options again.
87+--
88+-- Once you have written a @HasLink@ instance for @CustomThing@ you are ready to go.
89+type family IsElem' a s :: Constraint
90+
91+-- | Closed type family, check if @endpoint@ is within @api@.
92+-- Uses @'IsElem''@ if it exhausts all other options.
93+--
94+-- >>> ok (Proxy :: Proxy (IsElem ("hello" :> Get '[JSON] Int) SampleAPI))
95+-- OK
96+--
97+-- >>> ok (Proxy :: Proxy (IsElem ("bye" :> Get '[JSON] Int) SampleAPI))
98+-- ...
99+-- ... Could not deduce...
100+-- ...
101+--
102+-- An endpoint is considered within an api even if it is missing combinators
103+-- that don't affect the URL:
104+--
105+-- >>> ok (Proxy :: Proxy (IsElem (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int)))
106+-- OK
107+--
108+-- >>> ok (Proxy :: Proxy (IsElem (Get '[JSON] Int) (ReqBody '[JSON] Bool :> Get '[JSON] Int)))
109+-- OK
110+--
111+-- *N.B.:* @IsElem a b@ can be seen as capturing the notion of whether the URL
112+-- represented by @a@ would match the URL represented by @b@, *not* whether a
113+-- request represented by @a@ matches the endpoints serving @b@ (for the
114+-- latter, use 'IsIn').
115+type family IsElem endpoint api :: Constraint where
116+ IsElem e (sa :<|> sb) = Or (IsElem e sa) (IsElem e sb)
117+ IsElem (e :> sa) (e :> sb) = IsElem sa sb
118+ IsElem sa (Header sym x :> sb) = IsElem sa sb
119+ IsElem sa (ReqBody y x :> sb) = IsElem sa sb
120+ IsElem (CaptureAll z y :> sa) (CaptureAll x y :> sb)
121+ = IsElem sa sb
122+ IsElem (Capture z y :> sa) (Capture x y :> sb)
123+ = IsElem sa sb
124+ IsElem sa (QueryParam x y :> sb) = IsElem sa sb
125+ IsElem sa (QueryParams x y :> sb) = IsElem sa sb
126+ IsElem sa (QueryFlag x :> sb) = IsElem sa sb
127+ IsElem (Verb m s ct typ) (Verb m s ct' typ)
128+ = IsSubList ct ct'
129+ IsElem e e = ()
130+ IsElem e a = IsElem' e a
131+
132+-- | Check whether @sub@ is a sub-API of @api@.
133+--
134+-- >>> ok (Proxy :: Proxy (IsSubAPI SampleAPI (SampleAPI :<|> Get '[JSON] Int)))
135+-- OK
136+--
137+-- >>> ok (Proxy :: Proxy (IsSubAPI (SampleAPI :<|> Get '[JSON] Int) SampleAPI))
138+-- ...
139+-- ... Could not deduce...
140+-- ...
141+--
142+-- This uses @IsElem@ for checking; thus the note there applies here.
143+type family IsSubAPI sub api :: Constraint where
144+ IsSubAPI sub api = AllIsElem (Endpoints sub) api
145+
146+-- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsElem'@).
147+type family AllIsElem xs api :: Constraint where
148+ AllIsElem '[] api = ()
149+ AllIsElem (x ': xs) api = (IsElem x api, AllIsElem xs api)
150+
151+-- ** Strict inclusion
152+
153+-- | Closed type family, check if @endpoint@ is exactly within @api@.
154+--
155+-- >>> ok (Proxy :: Proxy (IsIn ("hello" :> Get '[JSON] Int) SampleAPI))
156+-- OK
157+--
158+-- Unlike 'IsElem', this requires an *exact* match.
159+--
160+-- >>> ok (Proxy :: Proxy (IsIn (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int)))
161+-- ...
162+-- ... Could not deduce...
163+-- ...
164+type family IsIn (endpoint :: *) (api :: *) :: Constraint where
165+ IsIn e (sa :<|> sb) = Or (IsIn e sa) (IsIn e sb)
166+ IsIn (e :> sa) (e :> sb) = IsIn sa sb
167+ IsIn e e = ()
168+
169+-- | Check whether @sub@ is a sub API of @api@.
170+--
171+-- Like 'IsSubAPI', but uses 'IsIn' rather than 'IsElem'.
172+type family IsStrictSubAPI sub api :: Constraint where
173+ IsStrictSubAPI sub api = AllIsIn (Endpoints sub) api
174+
175+-- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsIn'@).
176+--
177+-- ok (Proxy :: Proxy (AllIsIn (Endpoints SampleAPI) SampleAPI))
178+-- OK
179+type family AllIsIn xs api :: Constraint where
180+ AllIsIn '[] api = ()
181+ AllIsIn (x ': xs) api = (IsIn x api, AllIsIn xs api)
182+
183+-- * Helpers
184+
185+-- ** Lists
186+
187+-- | Apply @(e :>)@ to every API in @xs@.
188+type family MapSub e xs where
189+ MapSub e '[] = '[]
190+ MapSub e (x ': xs) = (e :> x) ': MapSub e xs
191+
192+-- | Append two type-level lists.
193+type family AppendList xs ys where
194+ AppendList '[] ys = ys
195+ AppendList (x ': xs) ys = x ': AppendList xs ys
196+
197+type family IsSubList a b :: Constraint where
198+ IsSubList '[] b = ()
199+ IsSubList (x ': xs) y = Elem x y `And` IsSubList xs y
200+
201+-- | Check that a value is an element of a list:
202+--
203+-- >>> ok (Proxy :: Proxy (Elem Bool '[Int, Bool]))
204+-- OK
205+--
206+-- >>> ok (Proxy :: Proxy (Elem String '[Int, Bool]))
207+-- ...
208+-- ... [Char]...'[Int, Bool...
209+-- ...
210+type Elem e es = ElemGo e es es
211+
212+-- 'orig' is used to store original list for better error messages
213+type family ElemGo e es orig :: Constraint where
214+ ElemGo x (x ': xs) orig = ()
215+ ElemGo y (x ': xs) orig = ElemGo y xs orig
216+#if MIN_VERSION_base(4,9,0)
217+ -- Note [Custom Errors]
218+ ElemGo x '[] orig = TypeError ('ShowType x
219+ ':<>: 'Text " expected in list "
220+ ':<>: 'ShowType orig)
221+#else
222+ ElemGo x '[] orig = ElemNotFoundIn x orig
223+#endif
224+
225+-- ** Logic
226+
227+-- | If either a or b produce an empty constraint, produce an empty constraint.
228+type family Or (a :: Constraint) (b :: Constraint) :: Constraint where
229+ -- This works because of:
230+ -- https://ghc.haskell.org/trac/ghc/wiki/NewAxioms/CoincidentOverlap
231+ Or () b = ()
232+ Or a () = ()
233+
234+-- | If both a or b produce an empty constraint, produce an empty constraint.
235+type family And (a :: Constraint) (b :: Constraint) :: Constraint where
236+ And () () = ()
237+
238+-- * Custom type errors
239+
240+#if !MIN_VERSION_base(4,9,0)
241+class ElemNotFoundIn val list
242+#endif
243+
244+{- Note [Custom Errors]
245+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
246+We might try to factor these our more cleanly, but the type synonyms and type
247+families are not evaluated (see https://ghc.haskell.org/trac/ghc/ticket/12048).
248+-}
249+
250+
251+-- $setup
252+--
253+-- The doctests in this module are run with following preamble:
254+--
255+-- >>> :set -XPolyKinds
256+-- >>> :set -XGADTs
257+-- >>> import Data.Proxy
258+-- >>> import Data.Type.Equality
259+-- >>> import Servant.API
260+-- >>> data OK ctx where OK :: ctx => OK ctx
261+-- >>> instance Show (OK ctx) where show _ = "OK"
262+-- >>> let ok :: ctx => Proxy ctx -> OK ctx; ok _ = OK
263+-- >>> type SampleAPI = "hello" :> Get '[JSON] Int :<|> "bye" :> Capture "name" String :> Post '[JSON, PlainText] Bool
264+-- >>> let sampleAPI = Proxy :: Proxy SampleAPI