-- |
-- Module      : Data.Functor.Contravariant.Night
-- Copyright   : (c) Justin Le 2019
-- License     : BSD3
--
-- Maintainer  : justin@jle.im
-- Stability   : experimental
-- Portability : non-portable
--
-- Provides 'Night', a form of the day convolution that is contravariant
-- and splits on 'Either'.
--
-- @since 0.3.0.0
module Data.Functor.Contravariant.Night (
    Night(..)
  , night
  , runNight
  , assoc, unassoc
  , swapped
  , trans1, trans2
  , intro1, intro2
  , elim1, elim2
  , Not(..), refuted
  ) where

import           Control.Natural
import           Data.Bifunctor
import           Data.Functor.Contravariant
import           Data.Functor.Contravariant.Decide
import           Data.Functor.Invariant
import           Data.Kind
import           Data.Void
import qualified Data.Bifunctor.Assoc              as B
import qualified Data.Bifunctor.Swap               as B

-- | A pairing of contravariant functors to create a new contravariant
-- functor that represents the "choice" between the two.
--
-- A @'Night' f g a@ is a contravariant "consumer" of @a@, and it does this
-- by either feeding the @a@ to @f@, or feeding the @a@ to @g@.  Which one
-- it gives it to happens at runtime depending /what/ @a@ is actually
-- given.
--
-- For example, if we have @x :: f a@ (a consumer of @a@s) and @y :: g b@
-- (a consumer of @b@s), then @'night' x y :: 'Night' f g ('Either' a b)@.
-- This is a consumer of @'Either' a b@s, and it consumes 'Left' branches
-- by feeding it to @x@, and 'Right' branches by feeding it to @y@.
--
-- Mathematically, this is a contravariant day convolution, except with
-- a different choice of bifunctor ('Either') than the typical one we talk
-- about in Haskell (which uses @(,)@).  Therefore, it is an alternative to
-- the typical 'Data.Functor.Day' convolution --- hence, the name 'Night'.
data Night :: (Type -> Type) -> (Type -> Type) -> (Type -> Type) where
    Night :: f b
          -> g c
          -> (a -> Either b c)
          -> Night f g a

instance Contravariant (Night f g) where
    contramap :: (a -> b) -> Night f g b -> Night f g a
contramap f :: a -> b
f (Night x :: f b
x y :: g c
y g :: b -> Either b c
g) = f b -> g c -> (a -> Either b c) -> Night f g a
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> Either b c) -> Night f g a
Night f b
x g c
y (b -> Either b c
g (b -> Either b c) -> (a -> b) -> a -> Either b c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f)

instance Invariant (Night f g) where
    invmap :: (a -> b) -> (b -> a) -> Night f g a -> Night f g b
invmap _ f :: b -> a
f (Night x :: f b
x y :: g c
y g :: a -> Either b c
g) = f b -> g c -> (b -> Either b c) -> Night f g b
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> Either b c) -> Night f g a
Night f b
x g c
y (a -> Either b c
g (a -> Either b c) -> (b -> a) -> b -> Either b c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> a
f)

-- | Inject into a 'Night'.
--
-- @'night' x y@ is a consumer of @'Either' a b@; 'Left' will be passed
-- to @x@, and 'Right' will be passed to @y@.
night
    :: f a
    -> g b
    -> Night f g (Either a b)
night :: f a -> g b -> Night f g (Either a b)
night x :: f a
x y :: g b
y = f a -> g b -> (Either a b -> Either a b) -> Night f g (Either a b)
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> Either b c) -> Night f g a
Night f a
x g b
y Either a b -> Either a b
forall a. a -> a
id

-- | Interpret out of a 'Night' into any instance of 'Decide' by providing
-- two interpreting functions.
runNight
    :: Decide h
    => (f ~> h)
    -> (g ~> h)
    -> Night f g ~> h
runNight :: (f ~> h) -> (g ~> h) -> Night f g ~> h
runNight f :: f ~> h
f g :: g ~> h
g (Night x :: f b
x y :: g c
y z :: x -> Either b c
z) = (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
z (f b -> h b
f ~> h
f f b
x) (g c -> h c
g ~> h
g g c
y)

-- | 'Night' is associative.
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 x :: f b
x (Night y :: g b
y z :: h c
z f :: c -> Either b c
f) g :: x -> Either b c
g) = Night f g (Either b b)
-> h c -> (x -> Either (Either b b) c) -> Night (Night f g) h x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> Either b c) -> Night f g a
Night (f b -> g b -> (Either b b -> Either b b) -> Night f g (Either b b)
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> Either b c) -> Night f g a
Night f b
x g b
y Either b b -> Either b b
forall a. a -> a
id) h c
z (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
f (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
g)

-- | 'Night' is associative.
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 x :: f b
x y :: g c
y f :: b -> Either b c
f) z :: h c
z g :: x -> Either b c
g) = f b
-> Night g h (Either c c)
-> (x -> Either b (Either c c))
-> Night f (Night g h) x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> Either b c) -> Night f g a
Night f b
x (g c -> h c -> (Either c c -> Either c c) -> Night g h (Either c c)
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> Either b c) -> Night f g a
Night g c
y h c
z Either c c -> Either c c
forall a. a -> a
id) (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
f (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
g)

-- | The two sides of a 'Night' can be swapped.
swapped :: Night f g ~> Night g f
swapped :: Night f g x -> Night g f x
swapped (Night x :: f b
x y :: g c
y f :: x -> Either b c
f) = g c -> f b -> (x -> Either c b) -> Night g f x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> Either b c) -> Night f g a
Night g c
y f b
x (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
f)

-- | Hoist a function over the left side of a 'Night'.
trans1 :: f ~> h -> Night f g ~> Night h g
trans1 :: (f ~> h) -> Night f g ~> Night h g
trans1 f :: f ~> h
f (Night x :: f b
x y :: g c
y z :: x -> Either b c
z) = h b -> g c -> (x -> Either b c) -> Night h g x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> Either b c) -> Night f g a
Night (f b -> h b
f ~> h
f f b
x) g c
y x -> Either b c
z

-- | Hoist a function over the right side of a 'Night'.
trans2 :: g ~> h -> Night f g ~> Night f h
trans2 :: (g ~> h) -> Night f g ~> Night f h
trans2 f :: g ~> h
f (Night x :: f b
x y :: g c
y z :: x -> Either b c
z) = f b -> h c -> (x -> Either b c) -> Night f h x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> Either b c) -> Night f g a
Night f b
x (g c -> h c
g ~> h
f g c
y) x -> Either b c
z

-- | A value of type @'Not' a@ is "proof" that @a@ is uninhabited.
newtype Not a = Not { Not a -> a -> Void
refute :: a -> Void }

-- | A useful shortcut for a common usage: 'Void' is always not so.
--
-- @since 0.3.1.0
refuted :: Not Void
refuted :: Not Void
refuted = (Void -> Void) -> Not Void
forall a. (a -> Void) -> Not a
Not Void -> Void
forall a. a -> a
id

instance Contravariant Not where
    contramap :: (a -> b) -> Not b -> Not a
contramap f :: a -> b
f (Not g :: b -> Void
g) = (a -> Void) -> Not a
forall a. (a -> Void) -> Not a
Not (b -> Void
g (b -> Void) -> (a -> b) -> a -> Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f)
-- | @since 0.3.1.0
instance Invariant Not where
    invmap :: (a -> b) -> (b -> a) -> Not a -> Not b
invmap _ = (b -> a) -> Not a -> Not b
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap

instance Semigroup (Not a) where
    Not f :: a -> Void
f <> :: Not a -> Not a -> Not a
<> Not g :: a -> Void
g = (a -> Void) -> Not a
forall a. (a -> Void) -> Not a
Not (a -> Void
f (a -> Void) -> (a -> Void) -> a -> Void
forall a. Semigroup a => a -> a -> a
<> a -> Void
g)

-- | The left identity of 'Night' is 'Not'; this is one side of that
-- isomorphism.
intro1 :: g ~> Night Not g
intro1 :: g x -> Night Not g x
intro1 x :: g x
x = Not Void -> g x -> (x -> Either Void x) -> Night Not g x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> Either b c) -> Night f g a
Night Not Void
refuted g x
x x -> Either Void x
forall a b. b -> Either a b
Right

-- | The right identity of 'Night' is 'Not'; this is one side of that
-- isomorphism.
intro2 :: f ~> Night f Not
intro2 :: f x -> Night f Not x
intro2 x :: f x
x = f x -> Not Void -> (x -> Either x Void) -> Night f Not x
forall (f :: * -> *) b (g :: * -> *) c a.
f b -> g c -> (a -> Either b c) -> Night f g a
Night f x
x Not Void
refuted x -> Either x Void
forall a b. a -> Either a b
Left

-- | The left identity of 'Night' is 'Not'; this is one side of that
-- isomorphism.
elim1 :: Contravariant g => Night Not g ~> g
elim1 :: Night Not g ~> g
elim1 (Night x :: Not b
x y :: g c
y z :: x -> Either b c
z) = (x -> c) -> g c -> g x
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap ((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
z) g c
y

-- | The right identity of 'Night' is 'Not'; this is one side of that
-- isomorphism.
elim2 :: Contravariant f => Night f Not ~> f
elim2 :: Night f Not ~> f
elim2 (Night x :: f b
x y :: Not c
y z :: x -> Either b c
z) = (x -> b) -> f b -> f x
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap ((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
z) f b
x