-- | -- Module : Control.Natural.IsoF -- Copyright : (c) Justin Le 2019 -- License : BSD3 -- -- Maintainer : justin@jle.im -- Stability : experimental -- Portability : non-portable -- -- Types describing isomorphisms between two functors, and functions to -- manipulate them. 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 -- | The type of an isomorphism between two functors. @f '<~>' g@ means that -- @f@ and @g@ are isomorphic to each other. -- -- We can effectively /use/ an @f \<~\> g@ with: -- -- @ -- 'viewF' :: (f \<~\> g) -> f a -> g a -- 'reviewF' :: (f \<~\> g) -> g a -> a a -- @ -- -- Use 'viewF' to extract the "@f@ to @g@" function, and 'reviewF' to -- extract the "@g@ to @f@" function. Reviewing and viewing the same value -- (or vice versa) leaves the value unchanged. -- -- One nice thing is that we can compose isomorphisms using '.' from -- "Prelude": -- -- @ -- ('.') :: f \<~\> g -- -> g \<~\> h -- -> f \<~\> h -- @ -- -- Another nice thing about this representation is that we have the -- "identity" isomorphism by using 'id' from "Prelude". -- -- @ -- 'id' :: f '<~>' g -- @ -- -- As a convention, most isomorphisms have form "X-ing", where the -- forwards function is "ing". For example, we have: -- -- @ -- 'Data.HBifunctor.Tensor.splittingSF' :: 'Data.HBifunctor.Tensor.Monoidal' t => 'Data.HBifunctor.Associative.SF' t a '<~>' t f ('Data.HBifunctor.Tensor.MF' t f) -- 'Data.HBifunctor.Tensor.splitSF' :: Monoidal t => SF t a '~>' t f (MF t f) -- @ type f <~> g = forall p a. Profunctor p => p (g a) (g a) -> p (f a) (f a) infixr 0 <~> -- | Create an @f '<~>' g@ by providing both legs of the isomorphism (the -- @f a -> g a@ and the @g a -> f a@. 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 -- | An isomorphism between two functors that are coercible/have the same -- internal representation. Useful for newtype wrappers. coercedF :: forall f g. (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 -- | Use a '<~>' by retrieving the "forward" function: -- -- @ -- 'viewF' :: (f <~> g) -> f a -> g a -- @ 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)) -- | Use a '<~>' by retrieving the "backwards" function: -- -- @ -- 'viewF' :: (f <~> g) -> f a -> g a -- @ 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)) -- | Lift a function @g a ~> g a@ to be a function @f a -> f a@, given an -- isomorphism between the two. -- -- One neat thing is that @'overF' i id == id@. 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 -- | Reverse an isomorphism. -- -- @ -- 'viewF' ('fromF' i) == 'reviewF' i -- 'reviewF' ('fromF' i) == 'viewF' i -- @ 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)