Add functional dependency back to Enter
This commit is contained in:
parent
acbcebc1d3
commit
d4cffe6591
1 changed files with 20 additions and 15 deletions
|
@ -27,41 +27,46 @@ import Prelude.Compat
|
|||
|
||||
import Servant.API
|
||||
|
||||
-- | Helper type family to state the 'Enter' symmetry.
|
||||
type family Entered m n api where
|
||||
Entered m n (m a) = n a
|
||||
Entered m n (a -> api) = a -> Entered m n api
|
||||
Entered m n (m a) = n a
|
||||
Entered m n (api1 :<|> api2) = Entered m n api1 :<|> Entered m n api2
|
||||
|
||||
class ( Entered m n typ ~ ret
|
||||
class
|
||||
( Entered m n typ ~ ret
|
||||
, Entered n m ret ~ typ
|
||||
)
|
||||
=> Enter typ m n ret
|
||||
) => Enter typ m n ret | typ m n -> ret, ret m n -> typ, ret typ m -> n, ret typ n -> m
|
||||
where
|
||||
-- | Map the leafs of an API type.
|
||||
enter :: (m :~> n) -> typ -> ret
|
||||
|
||||
-- ** Servant combinators
|
||||
|
||||
instance
|
||||
( Entered m1 n1 (typ1 :<|> typ2) ~ (ret1 :<|> ret2)
|
||||
, Entered n1 m1 (ret1 :<|> ret2) ~ (typ1 :<|> typ2)
|
||||
, Enter typ1 m1 n1 ret1, Enter typ2 m2 n2 ret2
|
||||
( Enter typ1 m1 n1 ret1, Enter typ2 m2 n2 ret2
|
||||
, m1 ~ m2, n1 ~ n2
|
||||
, Entered m1 n1 (typ1 :<|> typ2) ~ (ret1 :<|> ret2)
|
||||
, Entered n1 m1 (ret1 :<|> ret2) ~ (typ1 :<|> typ2)
|
||||
) => Enter (typ1 :<|> typ2) m1 n1 (ret1 :<|> ret2)
|
||||
where
|
||||
enter e (a :<|> b) = enter e a :<|> enter e b
|
||||
|
||||
instance
|
||||
( Entered m n (a -> typ) ~ (a -> ret)
|
||||
( Enter typ m n ret
|
||||
, Entered m n (a -> typ) ~ (a -> ret)
|
||||
, Entered n m (a -> ret) ~ (a -> typ)
|
||||
, Enter typ m n ret
|
||||
)
|
||||
=> Enter (a -> typ) m n (a -> ret)
|
||||
) => Enter (a -> typ) m n (a -> ret)
|
||||
where
|
||||
enter arg f a = enter arg (f a)
|
||||
|
||||
-- ** Useful instances
|
||||
-- ** Leaf instances
|
||||
|
||||
instance Enter (m a) m n (n a) where
|
||||
instance
|
||||
( Entered m n (m a) ~ n a
|
||||
, Entered n m (n a) ~ m a
|
||||
) => Enter (m a) m n (n a)
|
||||
where
|
||||
enter (NT f) = f
|
||||
|
||||
-- | Like `lift`.
|
||||
|
|
Loading…
Reference in a new issue