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 :: (f ~> g) -> (g ~> f) -> f <~> g
isoF = (f ~> g) -> (g ~> f) -> p (g a) (g a) -> p (f a) (f a)
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap
coercedF :: (forall x. Coercible (f x) (g x), forall x. Coercible (g x) (f x)) => f <~> g
coercedF :: f <~> g
coercedF = (f ~> g) -> (g ~> f) -> f <~> g
forall k (f :: k -> *) (g :: k -> *).
(f ~> g) -> (g ~> f) -> f <~> g
isoF f ~> g
forall a b. Coercible a b => a -> b
coerce g ~> f
forall a b. Coercible a b => a -> b
coerce
viewF :: f <~> g -> f ~> g
viewF :: (f <~> g) -> f ~> g
viewF i :: f <~> g
i = Forget (g x) (f x) (f x) -> f x -> g x
forall r a b. 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 r a b. (a -> r) -> Forget r a b
Forget g x -> g x
forall a. a -> a
id))
reviewF :: f <~> g -> g ~> f
reviewF :: (f <~> g) -> g ~> f
reviewF i :: f <~> g
i x :: 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 :: (f <~> g) -> (g ~> g) -> f ~> f
overF i :: f <~> g
i f :: 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 :: (f <~> g) -> g <~> f
fromF i :: 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 f <~> g
i) ((f <~> g) -> f ~> g
forall k (f :: k -> *) (g :: k -> *). (f <~> g) -> f ~> g
viewF f <~> g
i)