on master help sign in
Add IsIn and IsSubAPI constraints
commite9b281f3cc972ea61757fa06b3a9e3d16465a628 authorNickolay Kudasov <nickolay.kudasov@gmail.com> dateWed 20 Jan 2016, 17:53 (11 years ago) parent09c8464
1 file changed+50−5
servant/src/Servant/API/TypeLevel.hs+50−5
servant/src/Servant/API/TypeLevel.hs+50−5
@@ -17,23 +17,30 @@ import Servant.API.Alternative ( type (:<|>) )
1717
1818-- * API predicates
1919
20+-- | Flatten API into a list of endpoints.
21+type family Endpoints api where
22+ Endpoints (a :<|> b) = AppendList (Endpoints a) (Endpoints b)
23+ Endpoints (e :> a) = MapSub e (Endpoints a)
24+ Endpoints a = '[a]
25+
26+-- ** Lax inclusion
27+
2028-- | You may use this type family to tell the type checker that your custom
2129-- type may be skipped as part of a link. This is useful for things like
22−-- 'QueryParam' that are optional in a URI and do not affect them if they are
30+-- @'QueryParam'@ that are optional in a URI and do not affect them if they are
2331-- omitted.
2432--
2533-- >>> data CustomThing
2634-- >>> type instance IsElem' e (CustomThing :> s) = IsElem e s
2735--
28−-- Note that 'IsElem' is called, which will mutually recurse back to `IsElem'`
36+-- Note that @'IsElem'@ is called, which will mutually recurse back to @'IsElem''@
2937-- if it exhausts all other options again.
3038--
31−-- Once you have written a HasLink instance for CustomThing you are ready to
32−-- go.
39+-- Once you have written a @HasLink@ instance for @CustomThing@ you are ready to go.
3340type family IsElem' a s :: Constraint
3441
3542-- | Closed type family, check if @endpoint@ is within @api@.
36−-- Uses @'IsElem''@.
43+-- Uses @'IsElem''@ if it exhausts all other options.
3744type family IsElem endpoint api :: Constraint where
3845 IsElem e (sa :<|> sb) = Or (IsElem e sa) (IsElem e sb)
3946 IsElem (e :> sa) (e :> sb) = IsElem sa sb
@@ -51,10 +58,48 @@ type family IsElem endpoint api :: Constraint where
5158 IsElem e e = ()
5259 IsElem e a = IsElem' e a
5360
61+-- | Check whether @sub@ is a sub API of @api@.
62+type family IsSubAPI sub api :: Constraint where
63+ IsSubAPI sub api = AllIsElem (Endpoints sub) api
64+
65+-- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsElem'@).
66+type family AllIsElem xs api :: Constraint where
67+ AllIsElem '[] api = ()
68+ AllIsElem (x ': xs) api = (IsElem x api, AllIsElem xs api)
69+
70+-- ** Strict inclusion
71+
72+-- | Closed type family, check if @endpoint@ is exactly within @api@.
73+-- We aren't sure what affects how an endpoint is built up, so we require an
74+-- exact match.
75+type family IsIn (endpoint :: *) (api :: *) :: Constraint where
76+ IsIn e (sa :<|> sb) = Or (IsIn e sa) (IsIn e sb)
77+ IsIn (e :> sa) (e :> sb) = IsIn sa sb
78+ IsIn e e = ()
79+
80+-- | Check whether @sub@ is a sub API of @api@.
81+type family IsStrictSubAPI sub api :: Constraint where
82+ IsStrictSubAPI sub api = AllIsIn (Endpoints sub) api
83+
84+-- | Check that every element of @xs@ is an endpoint of @api@ (using @'IsIn'@).
85+type family AllIsIn xs api :: Constraint where
86+ AllIsIn '[] api = ()
87+ AllIsIn (x ': xs) api = (IsIn x api, AllIsIn xs api)
88+
5489-- * Helpers
5590
5691-- ** Lists
5792
93+-- | Apply @(e :>)@ to every API in @xs@.
94+type family MapSub e xs where
95+ MapSub e '[] = '[]
96+ MapSub e (x ': xs) = (e :> x) ': MapSub e xs
97+
98+-- | Append two type-level lists.
99+type family AppendList xs ys where
100+ AppendList '[] ys = ys
101+ AppendList (x ': xs) ys = x ': AppendList xs ys
102+
58103type family IsSubList a b :: Constraint where
59104 IsSubList '[] b = ()
60105 IsSubList (x ': xs) y = Elem x y `And` IsSubList xs y