    {-# LANGUAGE ExistentialQuantification #-}
    {-# LANGUAGE RankNTypes                #-}
    -----------------------------------------------------------------------------
    -- |
    -- Copyright   :  (C) 2018 Brian Mckenna
    -- License     :  BSD-style (see the file LICENSE)
    --
    -- Maintainer  :  Edward Kmett <ekmett@gmail.com>
    -- Stability   :  provisional
    -- Portability :  portable
    --
    -- The Day convolution of two invariant functors is an invariant
    -- functor.
    --
    -- <http://ncatlab.org/nlab/show/Day+convolution>
    ----------------------------------------------------------------------------

    module Data.Functor.Invariant.Day
      ( Day(..)
      , day
      , assoc, disassoc
      , swapped
      , intro1, intro2
      , elim1, elim2
      , trans1, trans2
      , toContravariant, toCovariant
      ) where

    import qualified Data.Functor.Contravariant.Day as Contravariant
    import qualified Data.Functor.Day               as Covariant
    import           Data.Functor.Identity
    import           Data.Functor.Invariant

    -- | The Day convolution of two invariant functors.
    data Day f g a = forall b c. Day (f b) (g c) (b -> c -> a) (a -> (b, c))

    instance Invariant (Day f g) where
      invmap :: forall a b. (a -> b) -> (b -> a) -> Day f g a -> Day f g b
    invmap a -> b
    f b -> a
    g (Day f b
    fb g c
    gc b -> c -> a
    bca a -> (b, c)
    abc) = f b -> g c -> (b -> c -> b) -> (b -> (b, c)) -> Day f g b
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
    Day f b
    fb g c
    gc ((a -> b
    f (a -> b) -> (c -> a) -> c -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    .) ((c -> a) -> c -> b) -> (b -> c -> a) -> b -> c -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b -> c -> a
    bca) (a -> (b, c)
    abc (a -> (b, c)) -> (b -> a) -> b -> (b, c)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . b -> a
    g)

    -- | Construct the Day convolution
    day :: f a -> g b -> Day f g (a, b)
    day :: forall (f :: * -> *) a (g :: * -> *) b.
    f a -> g b -> Day f g (a, b)
    day f a
    fa g b
    gb = f a
    -> g b
    -> (a -> b -> (a, b))
    -> ((a, b) -> (a, b))
    -> Day f g (a, b)
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
    Day f a
    fa g b
    gb (,) (a, b) -> (a, b)
    forall a. a -> a
    id

    -- | Day convolution provides a monoidal product. The associativity
    -- of this monoid is witnessed by 'assoc' and 'disassoc'.
    --
    -- @
    -- 'assoc' . 'disassoc' = 'id'
    -- 'disassoc' . 'assoc' = 'id'
    -- 'invmap' f g '.' 'assoc' = 'assoc' '.' 'invmap' f g
    -- @
    assoc :: Day f (Day g h) a -> Day (Day f g) h a
    assoc :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a.
    Day f (Day g h) a -> Day (Day f g) h a
    assoc (Day f b
    fb (Day g b
    gd h c
    he b -> c -> c
    dec c -> (b, c)
    cde) b -> c -> a
    bca a -> (b, c)
    abc) = (((b, b) -> c -> a) -> (a -> ((b, b), c)) -> Day (Day f g) h a)
    -> (a -> ((b, b), c)) -> ((b, b) -> c -> a) -> Day (Day f g) h a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (Day f g (b, b)
    -> h c
    -> ((b, b) -> c -> a)
    -> (a -> ((b, b), c))
    -> Day (Day f g) h a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
    Day (f b
    -> g b
    -> (b -> b -> (b, b))
    -> ((b, b) -> (b, b))
    -> Day f g (b, b)
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
    Day f b
    fb g b
    gd (,) (b, b) -> (b, b)
    forall a. a -> a
    id) h c
    he) a -> ((b, b), c)
    f (b, b) -> c -> a
    g
      where
        f :: a -> ((b, b), c)
    f a
    a =
          let (b
    b,c
    c) = a -> (b, c)
    abc a
    a
              (b
    d,c
    e) = c -> (b, c)
    cde c
    c
          in ((b
    b,b
    d),c
    e)
        g :: (b, b) -> c -> a
    g (b
    b,b
    d) c
    e =
          b -> c -> a
    bca b
    b (b -> c -> c
    dec b
    d c
    e)

    -- | Day convolution provides a monoidal product. The associativity
    -- of this monoid is witnessed by 'assoc' and 'disassoc'.
    --
    -- @
    -- 'assoc' . 'disassoc' = 'id'
    -- 'disassoc' . 'assoc' = 'id'
    -- 'invmap' f g '.' 'disassoc' = 'disassoc' '.' 'invmap' f g
    -- @
    disassoc :: Day (Day f g) h a -> Day f (Day g h) a
    disassoc :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a.
    Day (Day f g) h a -> Day f (Day g h) a
    disassoc (Day (Day f b
    fb g c
    gc b -> c -> b
    deb b -> (b, c)
    bde) h c
    hd b -> c -> a
    bca a -> (b, c)
    abc) = f b
    -> Day g h (c, c)
    -> (b -> (c, c) -> a)
    -> (a -> (b, (c, c)))
    -> Day f (Day g h) a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
    Day f b
    fb (g c
    -> h c
    -> (c -> c -> (c, c))
    -> ((c, c) -> (c, c))
    -> Day g h (c, c)
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
    Day g c
    gc h c
    hd (,) (c, c) -> (c, c)
    forall a. a -> a
    id) b -> (c, c) -> a
    f a -> (b, (c, c))
    g
      where
        f :: b -> (c, c) -> a
    f b
    e (c
    d,c
    c) =
          b -> c -> a
    bca (b -> c -> b
    deb b
    e c
    d) c
    c
        g :: a -> (b, (c, c))
    g a
    a =
          let (b
    b,c
    c) = a -> (b, c)
    abc a
    a
              (b
    d,c
    e) = b -> (b, c)
    bde b
    b
          in (b
    d,(c
    e,c
    c))

    -- | The monoid for 'Day' convolution on the cartesian monoidal structure is symmetric.
    --
    -- @
    -- 'invmap' f g '.' 'swapped' = 'swapped' '.' 'invmap' f g
    -- @
    swapped :: Day f g a -> Day g f a
    swapped :: forall (f :: * -> *) (g :: * -> *) a. Day f g a -> Day g f a
    swapped (Day f b
    fb g c
    gc b -> c -> a
    bca a -> (b, c)
    abc) = g c -> f b -> (c -> b -> a) -> (a -> (c, b)) -> Day g f a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
    Day g c
    gc f b
    fb ((b -> c -> a) -> c -> b -> a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip b -> c -> a
    bca) (\a
    a -> let (b
    b, c
    c) = a -> (b, c)
    abc a
    a in (c
    c, b
    b))

    -- | 'Identity' is the unit of 'Day' convolution
    --
    -- @
    -- 'intro1' '.' 'elim1' = 'id'
    -- 'elim1' '.' 'intro1' = 'id'
    -- @
    intro1 :: f a -> Day Identity f a
    intro1 :: forall (f :: * -> *) a. f a -> Day Identity f a
    intro1 f a
    fa = Identity ()
    -> f a -> (() -> a -> a) -> (a -> ((), a)) -> Day Identity f a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
    Day (() -> Identity ()
    forall a. a -> Identity a
    Identity ()) f a
    fa (\()
    _ a
    a -> a
    a) ((,) ())

    -- | 'Identity' is the unit of 'Day' convolution
    --
    -- @
    -- 'intro2' '.' 'elim2' = 'id'
    -- 'elim2' '.' 'intro2' = 'id'
    -- @
    intro2 :: f a -> Day f Identity a
    intro2 :: forall (f :: * -> *) a. f a -> Day f Identity a
    intro2 f a
    fa = f a
    -> Identity ()
    -> (a -> () -> a)
    -> (a -> (a, ()))
    -> Day f Identity a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
    Day f a
    fa (() -> Identity ()
    forall a. a -> Identity a
    Identity ()) a -> () -> a
    forall a b. a -> b -> a
    const ((a -> () -> (a, ())) -> () -> a -> (a, ())
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (,) ())

    -- | 'Identity' is the unit of 'Day' convolution
    --
    -- @
    -- 'intro1' '.' 'elim1' = 'id'
    -- 'elim1' '.' 'intro1' = 'id'
    -- @
    elim1 :: Invariant f => Day Identity f a -> f a
    elim1 :: forall (f :: * -> *) a. Invariant f => Day Identity f a -> f a
    elim1 (Day (Identity b
    b) f c
    fc b -> c -> a
    bca a -> (b, c)
    abc) = (c -> a) -> (a -> c) -> f c -> f a
    forall a b. (a -> b) -> (b -> a) -> f a -> f b
    forall (f :: * -> *) a b.
    Invariant f =>
    (a -> b) -> (b -> a) -> f a -> f b
    invmap (b -> c -> a
    bca b
    b) ((b, c) -> c
    forall a b. (a, b) -> b
    snd ((b, c) -> c) -> (a -> (b, c)) -> a -> c
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> (b, c)
    abc) f c
    fc

    -- | 'Identity' is the unit of 'Day' convolution
    --
    -- @
    -- 'intro2' '.' 'elim2' = 'id'
    -- 'elim2' '.' 'intro2' = 'id'
    -- @
    elim2 :: Invariant f => Day f Identity a -> f a
    elim2 :: forall (f :: * -> *) a. Invariant f => Day f Identity a -> f a
    elim2 (Day f b
    fb (Identity c
    c) b -> c -> a
    bca a -> (b, c)
    abc) = (b -> a) -> (a -> b) -> f b -> f a
    forall a b. (a -> b) -> (b -> a) -> f a -> f b
    forall (f :: * -> *) a b.
    Invariant f =>
    (a -> b) -> (b -> a) -> f a -> f b
    invmap ((b -> c -> a) -> c -> b -> a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip b -> c -> a
    bca c
    c) ((b, c) -> b
    forall a b. (a, b) -> a
    fst ((b, c) -> b) -> (a -> (b, c)) -> a -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> (b, c)
    abc) f b
    fb

    -- | Apply a natural transformation to the left-hand side of a Day convolution.
    --
    -- This respects the naturality of the natural transformation you supplied:
    --
    -- @
    -- 'invmap' f g '.' 'trans1' fg = 'trans1' fg '.' 'invmap' f g
    -- @
    trans1 :: (forall x. f x -> g x) -> Day f h a -> Day g h a
    trans1 :: forall (f :: * -> *) (g :: * -> *) (h :: * -> *) a.
    (forall x. f x -> g x) -> Day f h a -> Day g h a
    trans1 forall x. f x -> g x
    fg (Day f b
    fb h c
    hc b -> c -> a
    bca a -> (b, c)
    abc) = g b -> h c -> (b -> c -> a) -> (a -> (b, c)) -> Day g h a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
    Day (f b -> g b
    forall x. f x -> g x
    fg f b
    fb) h c
    hc b -> c -> a
    bca a -> (b, c)
    abc

    -- | Apply a natural transformation to the right-hand side of a Day convolution.
    --
    -- This respects the naturality of the natural transformation you supplied:
    --
    -- @
    -- 'invmap' f g '.' 'trans2' fg = 'trans2' fg '.' 'invmap' f g
    -- @
    trans2 :: (forall x. g x -> h x) -> Day f g a -> Day f h a
    trans2 :: forall (g :: * -> *) (h :: * -> *) (f :: * -> *) a.
    (forall x. g x -> h x) -> Day f g a -> Day f h a
    trans2 forall x. g x -> h x
    gh (Day f b
    fb g c
    gc b -> c -> a
    bca a -> (b, c)
    abc) = f b -> h c -> (b -> c -> a) -> (a -> (b, c)) -> Day f h a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> (a -> (b, c)) -> Day f g a
    Day f b
    fb (g c -> h c
    forall x. g x -> h x
    gh g c
    gc) b -> c -> a
    bca a -> (b, c)
    abc

    -- | Drop the covariant part of the Day convolution.
    toContravariant :: Day f g a -> Contravariant.Day f g a
    toContravariant :: forall (f :: * -> *) (g :: * -> *) a. Day f g a -> Day f g a
    toContravariant (Day f b
    fb g c
    gc b -> c -> a
    _ a -> (b, c)
    abc) = f b -> g c -> (a -> (b, c)) -> Day f g a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (a -> (b, c)) -> Day f g a
    Contravariant.Day f b
    fb g c
    gc a -> (b, c)
    abc

    -- | Drop the contravariant part of the Day convolution.
    toCovariant :: Day f g a -> Covariant.Day f g a
    toCovariant :: forall (f :: * -> *) (g :: * -> *) a. Day f g a -> Day f g a
    toCovariant (Day f b
    fb g c
    gc b -> c -> a
    bca a -> (b, c)
    _) = f b -> g c -> (b -> c -> a) -> Day f g a
    forall (f :: * -> *) (g :: * -> *) a b c.
    f b -> g c -> (b -> c -> a) -> Day f g a
    Covariant.Day f b
    fb g c
    gc b -> c -> a
    bca