module Data.Functor.Invariant.Night (
Night(..)
, Not(..), refuted
, night
, runNight
, nerve
, runNightAlt
, runNightDecide
, toCoNight
, toCoNight_
, toContraNight
, assoc, unassoc
, intro1, intro2
, elim1, elim2
, swapped
, trans1, trans2
) where
import Control.Natural
import Data.Bifunctor
import Data.Functor.Alt
import Data.Functor.Contravariant.Decide
import Data.Functor.Contravariant.Night (Not(..), refuted)
import Data.Functor.Invariant
import Data.Functor.Invariant.Internative
import Data.Kind
import Data.Void
import GHC.Generics
import qualified Data.Bifunctor.Assoc as B
import qualified Data.Bifunctor.Swap as B
import qualified Data.Functor.Contravariant.Night as CN
import qualified Data.Functor.Coyoneda as CY
data Night :: (Type -> Type) -> (Type -> Type) -> (Type -> Type) where
Night :: f b
-> g c
-> (b -> a)
-> (c -> a)
-> (a -> Either b c)
-> Night f g a
instance Invariant (Night f g) where
invmap :: (a -> b) -> (b -> a) -> Night f g a -> Night f g b
invmap a -> b
f b -> a
g (Night f b
x g c
y b -> a
h c -> a
j a -> Either b c
k) = f b
-> g c -> (b -> b) -> (c -> b) -> (b -> Either b c) -> Night f g b
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night f b
x g c
y (a -> b
f (a -> b) -> (b -> a) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
h) (a -> b
f (a -> b) -> (c -> a) -> c -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> a
j) (a -> Either b c
k (a -> Either b c) -> (b -> a) -> b -> Either b c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
g)
night :: f a -> g b -> Night f g (Either a b)
night :: f a -> g b -> Night f g (Either a b)
night f a
x g b
y = f a
-> g b
-> (a -> Either a b)
-> (b -> Either a b)
-> (Either a b -> Either a b)
-> Night f g (Either a b)
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night f a
x g b
y a -> Either a b
forall a b. a -> Either a b
Left b -> Either a b
forall a b. b -> Either a b
Right Either a b -> Either a b
forall a. a -> a
id
runNightAlt
:: forall f g h. Alt h
=> f ~> h
-> g ~> h
-> Night f g ~> h
runNightAlt :: (f ~> h) -> (g ~> h) -> Night f g ~> h
runNightAlt f ~> h
f g ~> h
g (Night f b
x g c
y b -> x
h c -> x
j x -> Either b c
_) = (b -> x) -> h b -> h x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> x
h (f b -> h b
f ~> h
f f b
x) h x -> h x -> h x
forall (f :: * -> *) a. Alt f => f a -> f a -> f a
<!> (c -> x) -> h c -> h x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> x
j (g c -> h c
g ~> h
g g c
y)
runNightDecide
:: forall f g h. Decide h
=> f ~> h
-> g ~> h
-> Night f g ~> h
runNightDecide :: (f ~> h) -> (g ~> h) -> Night f g ~> h
runNightDecide f ~> h
f g ~> h
g (Night f b
x g c
y b -> x
_ c -> x
_ x -> Either b c
k) = (x -> Either b c) -> h b -> h c -> h x
forall (f :: * -> *) a b c.
Decide f =>
(a -> Either b c) -> f b -> f c -> f a
decide x -> Either b c
k (f b -> h b
f ~> h
f f b
x) (g c -> h c
g ~> h
g g c
y)
toCoNight :: (Functor f, Functor g) => Night f g ~> f :*: g
toCoNight :: Night f g ~> (f :*: g)
toCoNight (Night f b
x g c
y b -> x
f c -> x
g x -> Either b c
_) = (b -> x) -> f b -> f x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> x
f f b
x f x -> g x -> (:*:) f g x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (c -> x) -> g c -> g x
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap c -> x
g g c
y
toCoNight_ :: Night f g ~> CY.Coyoneda f :*: CY.Coyoneda g
toCoNight_ :: Night f g x -> (:*:) (Coyoneda f) (Coyoneda g) x
toCoNight_ (Night f b
x g c
y b -> x
f c -> x
g x -> Either b c
_) = (b -> x) -> f b -> Coyoneda f x
forall b a (f :: * -> *). (b -> a) -> f b -> Coyoneda f a
CY.Coyoneda b -> x
f f b
x Coyoneda f x -> Coyoneda g x -> (:*:) (Coyoneda f) (Coyoneda g) x
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (c -> x) -> g c -> Coyoneda g x
forall b a (f :: * -> *). (b -> a) -> f b -> Coyoneda f a
CY.Coyoneda c -> x
g g c
y
toContraNight :: Night f g ~> CN.Night f g
toContraNight :: Night f g x -> Night f g x
toContraNight (Night f b
x g c
y b -> x
_ c -> x
_ x -> Either b c
h) = f b -> g c -> (x -> Either b c) -> Night f g x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> Either b c) -> Night f g a
CN.Night f b
x g c
y x -> Either b c
h
runNight
:: Inalt h
=> (f ~> h)
-> (g ~> h)
-> Night f g ~> h
runNight :: (f ~> h) -> (g ~> h) -> Night f g ~> h
runNight f ~> h
f g ~> h
g (Night f b
x g c
y b -> x
a c -> x
b x -> Either b c
c) = (b -> x) -> (c -> x) -> (x -> Either b c) -> h b -> h c -> h x
forall (f :: * -> *) b a c.
Inalt f =>
(b -> a) -> (c -> a) -> (a -> Either b c) -> f b -> f c -> f a
swerve b -> x
a c -> x
b x -> Either b c
c (f b -> h b
f ~> h
f f b
x) (g c -> h c
g ~> h
g g c
y)
nerve
:: Inalt f
=> Night f f ~> f
nerve :: Night f f ~> f
nerve (Night f b
x f c
y b -> x
a c -> x
b x -> Either b c
c) = (b -> x) -> (c -> x) -> (x -> Either b c) -> f b -> f c -> f x
forall (f :: * -> *) b a c.
Inalt f =>
(b -> a) -> (c -> a) -> (a -> Either b c) -> f b -> f c -> f a
swerve b -> x
a c -> x
b x -> Either b c
c f b
x f c
y
assoc :: Night f (Night g h) ~> Night (Night f g) h
assoc :: Night f (Night g h) x -> Night (Night f g) h x
assoc (Night f b
x (Night g b
y h c
z b -> c
f c -> c
g c -> Either b c
h) b -> x
j c -> x
k x -> Either b c
l) =
Night f g (Either b b)
-> h c
-> (Either b b -> x)
-> (c -> x)
-> (x -> Either (Either b b) c)
-> Night (Night f g) h x
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night (f b
-> g b
-> (b -> Either b b)
-> (b -> Either b b)
-> (Either b b -> Either b b)
-> Night f g (Either b b)
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night f b
x g b
y b -> Either b b
forall a b. a -> Either a b
Left b -> Either b b
forall a b. b -> Either a b
Right Either b b -> Either b b
forall a. a -> a
id) h c
z
((b -> x) -> (b -> x) -> Either b b -> x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> x
j (c -> x
k (c -> x) -> (b -> c) -> b -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> c
f))
(c -> x
k (c -> x) -> (c -> c) -> c -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> c
g)
(Either b (Either b c) -> Either (Either b b) c
forall (p :: * -> * -> *) a b c.
Assoc p =>
p a (p b c) -> p (p a b) c
B.unassoc (Either b (Either b c) -> Either (Either b b) c)
-> (x -> Either b (Either b c)) -> x -> Either (Either b b) c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (c -> Either b c) -> Either b c -> Either b (Either b c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second c -> Either b c
h (Either b c -> Either b (Either b c))
-> (x -> Either b c) -> x -> Either b (Either b c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b c
l)
unassoc :: Night (Night f g) h ~> Night f (Night g h)
unassoc :: Night (Night f g) h x -> Night f (Night g h) x
unassoc (Night (Night f b
x g c
y b -> b
f c -> b
g b -> Either b c
h) h c
z b -> x
j c -> x
k x -> Either b c
l) =
f b
-> Night g h (Either c c)
-> (b -> x)
-> (Either c c -> x)
-> (x -> Either b (Either c c))
-> Night f (Night g h) x
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night f b
x (g c
-> h c
-> (c -> Either c c)
-> (c -> Either c c)
-> (Either c c -> Either c c)
-> Night g h (Either c c)
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night g c
y h c
z c -> Either c c
forall a b. a -> Either a b
Left c -> Either c c
forall a b. b -> Either a b
Right Either c c -> Either c c
forall a. a -> a
id)
(b -> x
j (b -> x) -> (b -> b) -> b -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> b
f)
((c -> x) -> (c -> x) -> Either c c -> x
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (b -> x
j (b -> x) -> (c -> b) -> c -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> b
g) c -> x
k)
(Either (Either b c) c -> Either b (Either c c)
forall (p :: * -> * -> *) a b c.
Assoc p =>
p (p a b) c -> p a (p b c)
B.assoc (Either (Either b c) c -> Either b (Either c c))
-> (x -> Either (Either b c) c) -> x -> Either b (Either c c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> Either b c) -> Either b c -> Either (Either b c) c
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first b -> Either b c
h (Either b c -> Either (Either b c) c)
-> (x -> Either b c) -> x -> Either (Either b c) c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b c
l)
intro1 :: g ~> Night Not g
intro1 :: g x -> Night Not g x
intro1 g x
y = Not Void
-> g x
-> (Void -> x)
-> (x -> x)
-> (x -> Either Void x)
-> Night Not g x
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night Not Void
refuted g x
y Void -> x
forall a. Void -> a
absurd x -> x
forall a. a -> a
id x -> Either Void x
forall a b. b -> Either a b
Right
intro2 :: f ~> Night f Not
intro2 :: f x -> Night f Not x
intro2 f x
x = f x
-> Not Void
-> (x -> x)
-> (Void -> x)
-> (x -> Either x Void)
-> Night f Not x
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night f x
x Not Void
refuted x -> x
forall a. a -> a
id Void -> x
forall a. Void -> a
absurd x -> Either x Void
forall a b. a -> Either a b
Left
elim1 :: Invariant g => Night Not g ~> g
elim1 :: Night Not g ~> g
elim1 (Night Not b
x g c
y b -> x
_ c -> x
g x -> Either b c
h) = (c -> x) -> (x -> c) -> g c -> g x
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap c -> x
g ((b -> c) -> (c -> c) -> Either b c -> c
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Void -> c
forall a. Void -> a
absurd (Void -> c) -> (b -> Void) -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Not b -> b -> Void
forall a. Not a -> a -> Void
refute Not b
x) c -> c
forall a. a -> a
id (Either b c -> c) -> (x -> Either b c) -> x -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b c
h) g c
y
elim2 :: Invariant f => Night f Not ~> f
elim2 :: Night f Not ~> f
elim2 (Night f b
x Not c
y b -> x
f c -> x
_ x -> Either b c
h) = (b -> x) -> (x -> b) -> f b -> f x
forall (f :: * -> *) a b.
Invariant f =>
(a -> b) -> (b -> a) -> f a -> f b
invmap b -> x
f ((b -> b) -> (c -> b) -> Either b c -> b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either b -> b
forall a. a -> a
id (Void -> b
forall a. Void -> a
absurd (Void -> b) -> (c -> Void) -> c -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Not c -> c -> Void
forall a. Not a -> a -> Void
refute Not c
y) (Either b c -> b) -> (x -> Either b c) -> x -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b c
h) f b
x
swapped :: Night f g ~> Night g f
swapped :: Night f g x -> Night g f x
swapped (Night f b
x g c
y b -> x
f c -> x
g x -> Either b c
h) = g c
-> f b -> (c -> x) -> (b -> x) -> (x -> Either c b) -> Night g f x
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night g c
y f b
x c -> x
g b -> x
f (Either b c -> Either c b
forall (p :: * -> * -> *) a b. Swap p => p a b -> p b a
B.swap (Either b c -> Either c b) -> (x -> Either b c) -> x -> Either c b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either b c
h)
trans1 :: f ~> h -> Night f g ~> Night h g
trans1 :: (f ~> h) -> Night f g ~> Night h g
trans1 f ~> h
f (Night f b
x g c
y b -> x
g c -> x
h x -> Either b c
j) = h b
-> g c -> (b -> x) -> (c -> x) -> (x -> Either b c) -> Night h g x
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night (f b -> h b
f ~> h
f f b
x) g c
y b -> x
g c -> x
h x -> Either b c
j
trans2 :: g ~> h -> Night f g ~> Night f h
trans2 :: (g ~> h) -> Night f g ~> Night f h
trans2 g ~> h
f (Night f b
x g c
y b -> x
g c -> x
h x -> Either b c
j) = f b
-> h c -> (b -> x) -> (c -> x) -> (x -> Either b c) -> Night f h x
forall (f :: * -> *) b (g :: * -> *) c a.
f b
-> g c -> (b -> a) -> (c -> a) -> (a -> Either b c) -> Night f g a
Night f b
x (g c -> h c
g ~> h
f g c
y) b -> x
g c -> x
h x -> Either b c
j