module Control.Natural.IsoF (
type (~>)
, type (<~>)
, isoF
, coercedF
, viewF, reviewF, overF
, fromF
) where
import Control.Natural
import Data.Coerce
import Data.Kind
import Data.Profunctor
import Data.Tagged
type f <~> g = forall p a. Profunctor p => p (g a) (g a) -> p (f a) (f a)
infixr 0 <~>
isoF
:: f ~> g
-> g ~> f
-> f <~> g
isoF :: forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF f ~> g
f g ~> f
g p (g a) (g a)
a = (f a -> g a) -> (g a -> f a) -> p (g a) (g a) -> p (f a) (f a)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap f a -> g a
f ~> g
f g a -> f a
g ~> f
g p (g a) (g a)
a
coercedF :: forall f g. (forall x. Coercible (f x) (g x), forall x. Coercible (g x) (f x)) => f <~> g
coercedF :: forall {k} (f :: k -> *) (g :: k -> *).
(forall (x :: k). Coercible (f x) (g x),
forall (x :: k). Coercible (g x) (f x)) =>
f <~> g
coercedF = (f ~> g) -> (g ~> f) -> f <~> g
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF f x -> g x
f ~> g
forall a b. Coercible a b => a -> b
coerce g x -> f x
g ~> f
forall a b. Coercible a b => a -> b
coerce
viewF :: f <~> g -> f ~> g
viewF :: forall {k} (f :: k -> *) (g :: k -> *). (f <~> g) -> f ~> g
viewF f <~> g
i = Forget (g x) (f x) (f x) -> f x -> g x
forall {k} r a (b :: k). Forget r a b -> a -> r
runForget (Forget (g x) (g x) (g x) -> Forget (g x) (f x) (f x)
f <~> g
i ((g x -> g x) -> Forget (g x) (g x) (g x)
forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget g x -> g x
forall a. a -> a
id))
reviewF :: f <~> g -> g ~> f
reviewF :: forall {k} (f :: k -> *) (g :: k -> *). (f <~> g) -> g ~> f
reviewF f <~> g
i g x
x = Tagged (f x) (f x) -> f x
forall {k} (s :: k) b. Tagged s b -> b
unTagged (Tagged (g x) (g x) -> Tagged (f x) (f x)
f <~> g
i (g x -> Tagged (g x) (g x)
forall {k} (s :: k) b. b -> Tagged s b
Tagged g x
x))
overF :: f <~> g -> g ~> g -> f ~> f
overF :: forall {k} (f :: k -> *) (g :: k -> *).
(f <~> g) -> (g ~> g) -> f ~> f
overF f <~> g
i g ~> g
f = (g x -> g x) -> f x -> f x
f <~> g
i g x -> g x
g ~> g
f
fromF
:: forall (f :: Type -> Type) (g :: Type -> Type). ()
=> f <~> g
-> g <~> f
fromF :: forall (f :: * -> *) (g :: * -> *). (f <~> g) -> g <~> f
fromF f <~> g
i = (g ~> f) -> (f ~> g) -> g <~> f
forall {k} (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF ((f <~> g) -> g ~> f
forall {k} (f :: k -> *) (g :: k -> *). (f <~> g) -> g ~> f
reviewF p (g a) (g a) -> p (f a) (f a)
f <~> g
i) ((f <~> g) -> f ~> g
forall {k} (f :: k -> *) (g :: k -> *). (f <~> g) -> f ~> g
viewF p (g a) (g a) -> p (f a) (f a)
f <~> g
i)