on master help sign in
Loads of documetation and doctests.
931e67fJulian K. Arni
servant/src/Servant/API/TypeLevel.hs+129−69
@@ -1,29 +1,51 @@
1−{-# LANGUAGE CPP #-}
1+{-# LANGUAGE CPP #-}
2+{-# LANGUAGE ConstraintKinds #-}
2−{-# LANGUAGE DataKinds #-}
3+{-# LANGUAGE DataKinds #-}
3−{-# LANGUAGE KindSignatures #-}
4+{-# LANGUAGE KindSignatures #-}
4−{-# LANGUAGE PolyKinds #-}
5−{-# LANGUAGE TypeFamilies #-}
6−{-# LANGUAGE TypeOperators #-}
7−{-# LANGUAGE ConstraintKinds #-}
8{-# LANGUAGE MultiParamTypeClasses #-}
5{-# LANGUAGE MultiParamTypeClasses #-}
6+{-# LANGUAGE PolyKinds #-}
7+{-# LANGUAGE TypeFamilies #-}
8+{-# LANGUAGE TypeOperators #-}
9−{-# LANGUAGE UndecidableInstances #-}
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+-}
10module Servant.API.TypeLevel where
21module Servant.API.TypeLevel where
11
22
23+
12−import GHC.Exts(Constraint)
24+import GHC.Exts (Constraint)
13−import Servant.API.Capture ( Capture, CaptureAll )
25+import Servant.API.Alternative (type (:<|>))
26+import Servant.API.Capture (Capture, CaptureAll)
14−import Servant.API.ReqBody ( ReqBody )
27+import Servant.API.Header (Header)
15−import Servant.API.QueryParam ( QueryParam, QueryParams, QueryFlag )
28+import Servant.API.QueryParam (QueryFlag, QueryParam, QueryParams)
16−import Servant.API.Header ( Header )
17−import Servant.API.Verbs ( Verb )
29+import Servant.API.ReqBody (ReqBody)
18−import Servant.API.Sub ( type (:>) )
30+import Servant.API.Sub (type (:>))
19−import Servant.API.Alternative ( type (:<|>) )
31+import Servant.API.Verbs (Verb)
20#if MIN_VERSION_base(4,9,0)
32#if MIN_VERSION_base(4,9,0)
21−import GHC.TypeLits (TypeError, ErrorMessage(..))
33+import GHC.TypeLits (TypeError, ErrorMessage(..))
22#endif
34#endif
23
35
36+
37+
24-- * API predicates
38-- * API predicates
25
39
26-- | Flatten API into a list of endpoints.
40-- | Flatten API into a list of endpoints.
41+--
42+-- >>> :t showType @(Endpoints SampleAPI)
43+-- ...
44+-- ... :: Proxy
45+-- ... '["hello" :> Verb 'GET 200 '[JSON] Int,
46+-- ... "bye"
47+-- ... :> (Capture "name" String
48+-- ... :> Verb 'POST 200 '[JSON, PlainText] Bool)]
27type family Endpoints api where
49type family Endpoints api where
28 Endpoints (a :<|> b) = AppendList (Endpoints a) (Endpoints b)
50 Endpoints (a :<|> b) = AppendList (Endpoints a) (Endpoints b)
29 Endpoints (e :> a) = MapSub e (Endpoints a)
51 Endpoints (e :> a) = MapSub e (Endpoints a)
@@ -47,24 +69,56 @@ type family IsElem' a s :: Constraint
47
69
48-- | Closed type family, check if @endpoint@ is within @api@.
70-- | Closed type family, check if @endpoint@ is within @api@.
49-- Uses @'IsElem''@ if it exhausts all other options.
71-- Uses @'IsElem''@ if it exhausts all other options.
72+--
73+-- >>> ok @(IsElem ("hello" :> Get '[JSON] Int) SampleAPI)
74+-- OK
75+--
76+-- >>> ok @(IsElem ("bye" :> Get '[JSON] Int) SampleAPI)
77+-- ...
78+-- ... Could not deduce: ...
79+-- ...
80+--
81+-- An endpoint is considered within an api even if it is missing combinators
82+-- that don't affect the URL:
83+--
84+-- >>> ok @(IsElem (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int))
85+-- OK
86+--
87+-- >>> ok @(IsElem (Get '[JSON] Int) (ReqBody '[JSON] Bool :> Get '[JSON] Int))
88+-- OK
89+--
90+-- *N.B.:* @IsElem a b@ can be seen as capturing the notion of whether the URL
91+-- represented by @a@ would match the URL represented by @b@, *not* whether a
92+-- request represented by @a@ matches the endpoints serving @b@ (for the
93+-- latter, use 'IsIn').
50type family IsElem endpoint api :: Constraint where
94type family IsElem endpoint api :: Constraint where
51− IsElem e (sa :<|> sb) = Or (IsElem e sa) (IsElem e sb)
95+ IsElem e (sa :<|> sb) = Or (IsElem e sa) (IsElem e sb)
52− IsElem (e :> sa) (e :> sb) = IsElem sa sb
96+ IsElem (e :> sa) (e :> sb) = IsElem sa sb
53− IsElem sa (Header sym x :> sb) = IsElem sa sb
97+ IsElem sa (Header sym x :> sb) = IsElem sa sb
54− IsElem sa (ReqBody y x :> sb) = IsElem sa sb
98+ IsElem sa (ReqBody y x :> sb) = IsElem sa sb
55− IsElem (CaptureAll z y :> sa) (CaptureAll x y :> sb)
99+ IsElem (CaptureAll z y :> sa) (CaptureAll x y :> sb)
56− = IsElem sa sb
100+ = IsElem sa sb
57− IsElem (Capture z y :> sa) (Capture x y :> sb)
101+ IsElem (Capture z y :> sa) (Capture x y :> sb)
58− = IsElem sa sb
102+ = IsElem sa sb
59− IsElem sa (QueryParam x y :> sb) = IsElem sa sb
103+ IsElem sa (QueryParam x y :> sb) = IsElem sa sb
60− IsElem sa (QueryParams x y :> sb) = IsElem sa sb
104+ IsElem sa (QueryParams x y :> sb) = IsElem sa sb
61− IsElem sa (QueryFlag x :> sb) = IsElem sa sb
105+ IsElem sa (QueryFlag x :> sb) = IsElem sa sb
62− IsElem (Verb m s ct typ) (Verb m s ct' typ)
106+ IsElem (Verb m s ct typ) (Verb m s ct' typ)
63− = IsSubList ct ct'
107+ = IsSubList ct ct'
64− IsElem e e = ()
108+ IsElem e e = ()
65− IsElem e a = IsElem' e a
109+ IsElem e a = IsElem' e a
66−
110+
67−-- | Check whether @sub@ is a sub API of @api@.
111+-- | Check whether @sub@ is a sub-API of @api@.
112+--
113+-- >>> ok @(IsSubAPI SampleAPI (SampleAPI :<|> Get '[JSON] Int))
114+-- OK
115+--
116+-- >>> ok @(IsSubAPI (SampleAPI :<|> Get '[JSON] Int) SampleAPI)
117+-- ...
118+-- ... Could not deduce: ...
119+-- ...
120+--
121+-- This uses @IsElem@ for checking; thus the note there applies here.
68type family IsSubAPI sub api :: Constraint where
122type family IsSubAPI sub api :: Constraint where
69 IsSubAPI sub api = AllIsElem (Endpoints sub) api
123 IsSubAPI sub api = AllIsElem (Endpoints sub) api
70
124
@@ -76,18 +130,31 @@ type family AllIsElem xs api :: Constraint where
76-- ** Strict inclusion
130-- ** Strict inclusion
77
131
78-- | Closed type family, check if @endpoint@ is exactly within @api@.
132-- | Closed type family, check if @endpoint@ is exactly within @api@.
79−-- We aren't sure what affects how an endpoint is built up, so we require an
133+--
134+-- >>> ok @(IsIn ("hello" :> Get '[JSON] Int) SampleAPI)
135+-- OK
136+--
80−-- exact match.
137+-- Unlike 'IsElem', this requires an *exact* match.
138+--
139+-- >>> ok @(IsIn (Get '[JSON] Int) (Header "h" Bool :> Get '[JSON] Int))
140+-- ...
141+-- ... Could not deduce: ...
142+-- ...
81type family IsIn (endpoint :: *) (api :: *) :: Constraint where
143type family IsIn (endpoint :: *) (api :: *) :: Constraint where
82− IsIn e (sa :<|> sb) = Or (IsIn e sa) (IsIn e sb)
144+ IsIn e (sa :<|> sb) = Or (IsIn e sa) (IsIn e sb)
83− IsIn (e :> sa) (e :> sb) = IsIn sa sb
145+ IsIn (e :> sa) (e :> sb) = IsIn sa sb
84− IsIn e e = ()
146+ IsIn e e = ()
85
147
86-- | Check whether @sub@ is a sub API of @api@.
148-- | Check whether @sub@ is a sub API of @api@.
149+--
150+-- Like 'IsSubAPI', but uses 'IsIn' rather than 'IsElem'.
87type family IsStrictSubAPI sub api :: Constraint where
151type family IsStrictSubAPI sub api :: Constraint where
88 IsStrictSubAPI sub api = AllIsIn (Endpoints sub) api
152 IsStrictSubAPI sub api = AllIsIn (Endpoints sub) api
89
153
90-- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsIn'@).
154-- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsIn'@).
155+--
156+-- OK @(AllIsIn (Endpoints SampleAPI) SampleAPI)
157+-- OK
91type family AllIsIn xs api :: Constraint where
158type family AllIsIn xs api :: Constraint where
92 AllIsIn '[] api = ()
159 AllIsIn '[] api = ()
93 AllIsIn (x ': xs) api = (IsIn x api, AllIsIn xs api)
160 AllIsIn (x ': xs) api = (IsIn x api, AllIsIn xs api)
@@ -107,45 +174,31 @@ type family AppendList xs ys where
107 AppendList (x ': xs) ys = x ': AppendList xs ys
174 AppendList (x ': xs) ys = x ': AppendList xs ys
108
175
109type family IsSubList a b :: Constraint where
176type family IsSubList a b :: Constraint where
110− IsSubList '[] b = ()
177+ IsSubList '[] b = ()
111− IsSubList (x ': xs) y = Elem x y `And` IsSubList xs y
178+ IsSubList (x ': xs) y = Elem x y `And` IsSubList xs y
112
179
113−#if !MIN_VERSION_base(4,9,0)
114−-- | Check that a value is an element of a list:
115−--
116−-- >>> ok (Proxy :: Proxy (Elem Bool '[Int, Bool]))
117−-- OK
118−--
119−-- >>> ok (Proxy :: Proxy (Elem String '[Int, Bool]))
120−-- ...
121−-- No instance for (ElemNotFoundIn [Char] '[Int, Bool])
122−-- arising from a use of ‘ok’
123−-- ...
124−type Elem e es = ElemGo e es es
125−#else
126-- | Check that a value is an element of a list:
180-- | Check that a value is an element of a list:
127--
181--
128−-- >>> ok (Proxy :: Proxy (Elem Bool '[Int, Bool]))
182+-- >>> ok @(Elem Bool '[Int, Bool])
129-- OK
183-- OK
130--
184--
131−-- >>> ok (Proxy :: Proxy (Elem String '[Int, Bool]))
185+-- >>> ok @(Elem String '[Int, Bool])
132-- ...
186-- ...
133-- ... [Char] expected in list '[Int, Bool]
187-- ... [Char] expected in list '[Int, Bool]
134-- ...
188-- ...
135type Elem e es = ElemGo e es es
189type Elem e es = ElemGo e es es
136−#endif
137
190
138-- 'orig' is used to store original list for better error messages
191-- 'orig' is used to store original list for better error messages
139type family ElemGo e es orig :: Constraint where
192type family ElemGo e es orig :: Constraint where
140− ElemGo x (x ': xs) orig = ()
193+ ElemGo x (x ': xs) orig = ()
141− ElemGo y (x ': xs) orig = ElemGo y xs orig
194+ ElemGo y (x ': xs) orig = ElemGo y xs orig
142#if MIN_VERSION_base(4,9,0)
195#if MIN_VERSION_base(4,9,0)
143− -- Note [Custom Errors]
196+ -- Note [Custom Errors]
144− ElemGo x '[] orig = TypeError ('ShowType x
197+ ElemGo x '[] orig = TypeError ('ShowType x
145− ':<>: 'Text " expected in list "
198+ ':<>: 'Text " expected in list "
146− ':<>: 'ShowType orig)
199+ ':<>: 'ShowType orig)
147#else
200#else
148− ElemGo x '[] orig = ElemNotFoundIn x orig
201+ ElemGo x '[] orig = ElemNotFoundIn x orig
149#endif
202#endif
150
203
151-- ** Logic
204-- ** Logic
@@ -154,12 +207,12 @@ type family ElemGo e es orig :: Constraint where
154type family Or (a :: Constraint) (b :: Constraint) :: Constraint where
207type family Or (a :: Constraint) (b :: Constraint) :: Constraint where
155 -- This works because of:
208 -- This works because of:
156 -- https://ghc.haskell.org/trac/ghc/wiki/NewAxioms/CoincidentOverlap
209 -- https://ghc.haskell.org/trac/ghc/wiki/NewAxioms/CoincidentOverlap
157− Or () b = ()
210+ Or () b = ()
158− Or a () = ()
211+ Or a () = ()
159
212
160-- | If both a or b produce an empty constraint, produce an empty constraint.
213-- | If both a or b produce an empty constraint, produce an empty constraint.
161type family And (a :: Constraint) (b :: Constraint) :: Constraint where
214type family And (a :: Constraint) (b :: Constraint) :: Constraint where
162− And () () = ()
215+ And () () = ()
163
216
164-- * Custom type errors
217-- * Custom type errors
165
218
@@ -173,7 +226,14 @@ We might try to factor these our more cleanly, but the type synonyms and type
173families are not evaluated (see https://ghc.haskell.org/trac/ghc/ticket/12048).
226families are not evaluated (see https://ghc.haskell.org/trac/ghc/ticket/12048).
174-}
227-}
175
228
229+
176-- $setup
230-- $setup
231+-- >>> :set -XTypeApplications
232+-- >>> :set -XPolyKinds
177-- >>> import Data.Proxy
233-- >>> import Data.Proxy
234+-- >>> import Servant.API
178−-- >>> data OK = OK deriving (Show)
235+-- >>> data OK ctx = OK deriving (Show)
179−-- >>> let ok :: ctx => Proxy ctx -> OK; ok _ = OK
236+-- >>> let ok :: ctx => OK ctx; ok = OK
237+-- >>> let showType :: Proxy a ; showType = Proxy
238+-- >>> type SampleAPI = "hello" :> Get '[JSON] Int :<|> "bye" :> Capture "name" String :> Post '[JSON, PlainText] Bool
239+-- >>> let sampleAPI = Proxy :: Proxy SampleAPI