{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE TupleSections #-}
module Data.Profunctor.Cartesian(
  Cartesian(..),
  prodDay,

  Cocartesian(..),
  sumDay,
  
  -- * @Cartesian p@ iff @forall x. Applicative (p x)@
  pureDefault,
  proUnitDefault,
  liftA2Default,
  fanoutDefault,

  -- * Utilities
  describeFinite,
  describeFiniteBits,

  -- * About distributivy laws between 'Cartesian' and 'Cocartesian'
  --
  -- $distributivity
) where

import Control.Applicative

import Data.Void

import Data.Functor.Contravariant.Divisible
import Data.Bifunctor(Bifunctor(..))
import Data.Bifunctor.Clown
import Data.Bifunctor.Joker
import Data.Bifunctor.Product
import Data.Profunctor
import Data.Profunctor.Monad
import Data.Profunctor.Yoneda
import Data.Profunctor.Composition hiding (assoc)
import Data.Profunctor.Day

import Data.Bits
import GHC.TypeNats ( KnownNat, Natural, natVal )
import Data.Finite (Finite, getFinite, finites)
import Data.Finite.Internal qualified as Unsafe

class Profunctor p => Cartesian p where
  {-# MINIMAL proUnit, (proProduct | (***) | (&&&)) #-}

  -- | Unit of the product.
  --
  -- The type of 'proUnit' can be understood as @proUnit' :: p () ()@
  -- treated to have more generally-typed @p a ()@ using 'lmap'.
  -- 
  -- @
  -- const () :: a -> ()
  -- proUnit' :: p () ()
  -- 'lmap' (const ()) proUnit' :: p a ()
  -- @
  proUnit :: p a ()
  
  proProduct :: (a -> (a1,a2)) -> ((b1, b2) -> b) -> p a1 b1 -> p a2 b2 -> p a b
  proProduct a -> (a1, a2)
f (b1, b2) -> b
g p a1 b1
p p a2 b2
q = (a -> (a1, a2)) -> ((b1, b2) -> b) -> p (a1, a2) (b1, b2) -> p a b
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> (a1, a2)
f (b1, b2) -> b
g (p (a1, a2) (b1, b2) -> p a b) -> p (a1, a2) (b1, b2) -> p a b
forall a b. (a -> b) -> a -> b
$ p a1 b1
p p a1 b1 -> p a2 b2 -> p (a1, a2) (b1, b2)
forall a b a' b'. p a b -> p a' b' -> p (a, a') (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** p a2 b2
q
  
  -- | Product of two profunctors
  (***) :: p a b -> p a' b' -> p (a,a') (b,b')
  p a b
p *** p a' b'
q = ((a, a') -> a) -> p a b -> p (a, a') b
forall a b c. (a -> b) -> p b c -> p a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap (a, a') -> a
forall a b. (a, b) -> a
fst p a b
p p (a, a') b -> p (a, a') b' -> p (a, a') (b, b')
forall a b b'. p a b -> p a b' -> p a (b, b')
forall (p :: * -> * -> *) a b b'.
Cartesian p =>
p a b -> p a b' -> p a (b, b')
&&& ((a, a') -> a') -> p a' b' -> p (a, a') b'
forall a b c. (a -> b) -> p b c -> p a c
forall (p :: * -> * -> *) a b c.
Profunctor p =>
(a -> b) -> p b c -> p a c
lmap (a, a') -> a'
forall a b. (a, b) -> b
snd p a' b'
q
  
  -- | Alternative way to define the product (pronounced \"fan-out\")
  (&&&) :: p a b -> p a b' -> p a (b, b')
  (&&&) = (a -> (a, a))
-> ((b, b') -> (b, b')) -> p a b -> p a b' -> p a (b, b')
forall a a1 a2 b1 b2 b.
(a -> (a1, a2)) -> ((b1, b2) -> b) -> p a1 b1 -> p a2 b2 -> p a b
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cartesian p =>
(a -> (a1, a2)) -> ((b1, b2) -> b) -> p a1 b1 -> p a2 b2 -> p a b
proProduct a -> (a, a)
forall a. a -> (a, a)
delta (b, b') -> (b, b')
forall a. a -> a
id

  -- | Function from finite types can be constructed as iterated product.
  --
  -- There is a default implementaion, but it can be more efficient implementation.
  proPower :: KnownNat n => p a b -> p (Finite n -> a) (Finite n -> b)
  proPower p a b
p = Power p (Finite n) (Finite n)
-> forall s t. p s t -> p (Finite n -> s) (Finite n -> t)
forall (p :: * -> * -> *) a b.
Power p a b -> forall s t. p s t -> p (b -> s) (a -> t)
runPower Power p (Finite n) (Finite n)
forall (n :: Nat) (p :: * -> * -> *).
(KnownNat n, Cartesian p, Cocartesian p) =>
p (Finite n) (Finite n)
describeFinite p a b
p

delta :: a -> (a,a)
delta :: forall a. a -> (a, a)
delta a
a = (a
a,a
a)

prodDay :: Cartesian r => (p :-> r) -> (q :-> r) -> Day (,) p q :-> r
prodDay :: forall (r :: * -> * -> *) (p :: * -> * -> *) (q :: * -> * -> *).
Cartesian r =>
(p :-> r) -> (q :-> r) -> Day (,) p q :-> r
prodDay p :-> r
pr q :-> r
qr (Day p a1 b1
p q a2 b2
q a -> (a1, a2)
opA (b1, b2) -> b
opB) = (a -> (a1, a2)) -> ((b1, b2) -> b) -> r a1 b1 -> r a2 b2 -> r a b
forall a a1 a2 b1 b2 b.
(a -> (a1, a2)) -> ((b1, b2) -> b) -> r a1 b1 -> r a2 b2 -> r a b
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cartesian p =>
(a -> (a1, a2)) -> ((b1, b2) -> b) -> p a1 b1 -> p a2 b2 -> p a b
proProduct a -> (a1, a2)
opA (b1, b2) -> b
opB (p a1 b1 -> r a1 b1
p :-> r
pr p a1 b1
p) (q a2 b2 -> r a2 b2
q :-> r
qr q a2 b2
q)

-- * @Cartesian p@ iff @forall x. Applicative (p x)@

pureDefault :: Cartesian p => b -> p a b
pureDefault :: forall (p :: * -> * -> *) b a. Cartesian p => b -> p a b
pureDefault b
b = (() -> b) -> p a () -> p a b
forall b c a. (b -> c) -> p a b -> p a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap (b -> () -> b
forall a b. a -> b -> a
const b
b) p a ()
forall a. p a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit

proUnitDefault :: Applicative (p a) => p a ()
proUnitDefault :: forall (p :: * -> * -> *) a. Applicative (p a) => p a ()
proUnitDefault = () -> p a ()
forall a. a -> p a a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

liftA2Default :: Cartesian p => (a -> b -> c) -> p x a -> p x b -> p x c
liftA2Default :: forall (p :: * -> * -> *) a b c x.
Cartesian p =>
(a -> b -> c) -> p x a -> p x b -> p x c
liftA2Default a -> b -> c
f = (x -> (x, x)) -> ((a, b) -> c) -> p x a -> p x b -> p x c
forall a a1 a2 b1 b2 b.
(a -> (a1, a2)) -> ((b1, b2) -> b) -> p a1 b1 -> p a2 b2 -> p a b
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cartesian p =>
(a -> (a1, a2)) -> ((b1, b2) -> b) -> p a1 b1 -> p a2 b2 -> p a b
proProduct x -> (x, x)
forall a. a -> (a, a)
delta ((a -> b -> c) -> (a, b) -> c
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> b -> c
f)

fanoutDefault :: (Profunctor p, Applicative (p a)) => p a b1 -> p a b2 -> p a (b1, b2)
fanoutDefault :: forall (p :: * -> * -> *) a b1 b2.
(Profunctor p, Applicative (p a)) =>
p a b1 -> p a b2 -> p a (b1, b2)
fanoutDefault = (b1 -> b2 -> (b1, b2)) -> p a b1 -> p a b2 -> p a (b1, b2)
forall a b c. (a -> b -> c) -> p a a -> p a b -> p a c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,)

instance Cartesian (->) where
  proUnit :: forall a. a -> ()
proUnit = () -> a -> ()
forall a b. a -> b -> a
const ()
  a -> b
p1 *** :: forall a b a' b'. (a -> b) -> (a' -> b') -> (a, a') -> (b, b')
*** a' -> b'
p2 = (a -> b) -> (a' -> b') -> (a, a') -> (b, b')
forall a b a' b'. (a -> b) -> (a' -> b') -> (a, a') -> (b, b')
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
p1 a' -> b'
p2
  proPower :: forall (n :: Nat) a b.
KnownNat n =>
(a -> b) -> (Finite n -> a) -> (Finite n -> b)
proPower = (a -> b) -> (Finite n -> a) -> Finite n -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)

instance (Monoid r) => Cartesian (Forget r) where
  proUnit :: forall a. Forget r a ()
proUnit = (a -> r) -> Forget r a ()
forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget (r -> a -> r
forall a b. a -> b -> a
const r
forall a. Monoid a => a
mempty)
  Forget a -> r
f *** :: forall a b a' b'.
Forget r a b -> Forget r a' b' -> Forget r (a, a') (b, b')
*** Forget a' -> r
g = ((a, a') -> r) -> Forget r (a, a') (b, b')
forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget (\(a
a,a'
b) -> a -> r
f a
a r -> r -> r
forall a. Semigroup a => a -> a -> a
<> a' -> r
g a'
b)
  proPower :: forall (n :: Nat) a b.
KnownNat n =>
Forget r a b -> Forget r (Finite n -> a) (Finite n -> b)
proPower (Forget a -> r
f) = ((Finite n -> a) -> r) -> Forget r (Finite n -> a) (Finite n -> b)
forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget (\Finite n -> a
h -> (Finite n -> r) -> [Finite n] -> r
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (a -> r
f (a -> r) -> (Finite n -> a) -> Finite n -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite n -> a
h) [Finite n]
forall (n :: Nat). KnownNat n => [Finite n]
finites)

instance (Applicative f) => Cartesian (Star f) where
  proUnit :: forall a. Star f a ()
proUnit = (a -> f ()) -> Star f a ()
forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (f () -> a -> f ()
forall a b. a -> b -> a
const (() -> f ()
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()))
  Star a -> f b
p1 *** :: forall a b a' b'.
Star f a b -> Star f a' b' -> Star f (a, a') (b, b')
*** Star a' -> f b'
p2 = ((a, a') -> f (b, b')) -> Star f (a, a') (b, b')
forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (((a, a') -> f (b, b')) -> Star f (a, a') (b, b'))
-> ((a, a') -> f (b, b')) -> Star f (a, a') (b, b')
forall a b. (a -> b) -> a -> b
$ \(a
a,a'
a') -> (b -> b' -> (b, b')) -> f b -> f b' -> f (b, b')
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,) (a -> f b
p1 a
a) (a' -> f b'
p2 a'
a')

instance (Applicative f) => Cartesian (Joker f) where
  proUnit :: forall a. Joker f a ()
proUnit = f () -> Joker f a ()
forall {k} {k1} (g :: k -> *) (a :: k1) (b :: k).
g b -> Joker g a b
Joker (() -> f ()
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
  Joker f b
p1 *** :: forall a b a' b'.
Joker f a b -> Joker f a' b' -> Joker f (a, a') (b, b')
*** Joker f b'
p2 = f (b, b') -> Joker f (a, a') (b, b')
forall {k} {k1} (g :: k -> *) (a :: k1) (b :: k).
g b -> Joker g a b
Joker (f (b, b') -> Joker f (a, a') (b, b'))
-> f (b, b') -> Joker f (a, a') (b, b')
forall a b. (a -> b) -> a -> b
$ (b -> b' -> (b, b')) -> f b -> f b' -> f (b, b')
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (,) f b
p1 f b'
p2

instance (Divisible f) => Cartesian (Clown f) where
  proUnit :: forall a. Clown f a ()
proUnit = f a -> Clown f a ()
forall {k} {k1} (f :: k -> *) (a :: k) (b :: k1).
f a -> Clown f a b
Clown f a
forall a. f a
forall (f :: * -> *) a. Divisible f => f a
conquer
  Clown f a
p1 *** :: forall a b a' b'.
Clown f a b -> Clown f a' b' -> Clown f (a, a') (b, b')
*** Clown f a'
p2 = f (a, a') -> Clown f (a, a') (b, b')
forall {k} {k1} (f :: k -> *) (a :: k) (b :: k1).
f a -> Clown f a b
Clown (f (a, a') -> Clown f (a, a') (b, b'))
-> f (a, a') -> Clown f (a, a') (b, b')
forall a b. (a -> b) -> a -> b
$ f a -> f a' -> f (a, a')
forall (f :: * -> *) a b. Divisible f => f a -> f b -> f (a, b)
divided f a
p1 f a'
p2

instance (Cartesian p, Cartesian q) => Cartesian (Product p q) where
  proUnit :: forall a. Product p q a ()
proUnit = p a () -> q a () -> Product p q a ()
forall {k} {k1} (f :: k -> k1 -> *) (g :: k -> k1 -> *) (a :: k)
       (b :: k1).
f a b -> g a b -> Product f g a b
Pair p a ()
forall a. p a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit q a ()
forall a. q a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit
  Pair p a b
p1 q a b
q1 *** :: forall a b a' b'.
Product p q a b -> Product p q a' b' -> Product p q (a, a') (b, b')
*** Pair p a' b'
p2 q a' b'
q2 = p (a, a') (b, b')
-> q (a, a') (b, b') -> Product p q (a, a') (b, b')
forall {k} {k1} (f :: k -> k1 -> *) (g :: k -> k1 -> *) (a :: k)
       (b :: k1).
f a b -> g a b -> Product f g a b
Pair (p a b
p1 p a b -> p a' b' -> p (a, a') (b, b')
forall a b a' b'. p a b -> p a' b' -> p (a, a') (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** p a' b'
p2) (q a b
q1 q a b -> q a' b' -> q (a, a') (b, b')
forall a b a' b'. q a b -> q a' b' -> q (a, a') (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** q a' b'
q2)
  proPower :: forall (n :: Nat) a b.
KnownNat n =>
Product p q a b -> Product p q (Finite n -> a) (Finite n -> b)
proPower (Pair p a b
p q a b
q) = p (Finite n -> a) (Finite n -> b)
-> q (Finite n -> a) (Finite n -> b)
-> Product p q (Finite n -> a) (Finite n -> b)
forall {k} {k1} (f :: k -> k1 -> *) (g :: k -> k1 -> *) (a :: k)
       (b :: k1).
f a b -> g a b -> Product f g a b
Pair (p a b -> p (Finite n -> a) (Finite n -> b)
forall (n :: Nat) a b.
KnownNat n =>
p a b -> p (Finite n -> a) (Finite n -> b)
forall (p :: * -> * -> *) (n :: Nat) a b.
(Cartesian p, KnownNat n) =>
p a b -> p (Finite n -> a) (Finite n -> b)
proPower p a b
p) (q a b -> q (Finite n -> a) (Finite n -> b)
forall (n :: Nat) a b.
KnownNat n =>
q a b -> q (Finite n -> a) (Finite n -> b)
forall (p :: * -> * -> *) (n :: Nat) a b.
(Cartesian p, KnownNat n) =>
p a b -> p (Finite n -> a) (Finite n -> b)
proPower q a b
q)

instance (Cartesian p, Cartesian q) => Cartesian (Procompose p q) where
  proUnit :: forall a. Procompose p q a ()
proUnit = p () () -> q a () -> Procompose p q a ()
forall {k} {k1} {k2} (p :: k -> k1 -> *) (x :: k) (c :: k1)
       (q :: k2 -> k -> *) (d :: k2).
p x c -> q d x -> Procompose p q d c
Procompose p () ()
forall a. p a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit q a ()
forall a. q a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit
  Procompose p x b
p1 q a x
q1 *** :: forall a b a' b'.
Procompose p q a b
-> Procompose p q a' b' -> Procompose p q (a, a') (b, b')
*** Procompose p x b'
p2 q a' x
q2 =
    p (x, x) (b, b')
-> q (a, a') (x, x) -> Procompose p q (a, a') (b, b')
forall {k} {k1} {k2} (p :: k -> k1 -> *) (x :: k) (c :: k1)
       (q :: k2 -> k -> *) (d :: k2).
p x c -> q d x -> Procompose p q d c
Procompose (p x b
p1 p x b -> p x b' -> p (x, x) (b, b')
forall a b a' b'. p a b -> p a' b' -> p (a, a') (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** p x b'
p2) (q a x
q1 q a x -> q a' x -> q (a, a') (x, x)
forall a b a' b'. q a b -> q a' b' -> q (a, a') (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** q a' x
q2)
  proPower :: forall (n :: Nat) a b.
KnownNat n =>
Procompose p q a b
-> Procompose p q (Finite n -> a) (Finite n -> b)
proPower (Procompose p x b
p q a x
q) = p (Finite n -> x) (Finite n -> b)
-> q (Finite n -> a) (Finite n -> x)
-> Procompose p q (Finite n -> a) (Finite n -> b)
forall {k} {k1} {k2} (p :: k -> k1 -> *) (x :: k) (c :: k1)
       (q :: k2 -> k -> *) (d :: k2).
p x c -> q d x -> Procompose p q d c
Procompose (p x b -> p (Finite n -> x) (Finite n -> b)
forall (n :: Nat) a b.
KnownNat n =>
p a b -> p (Finite n -> a) (Finite n -> b)
forall (p :: * -> * -> *) (n :: Nat) a b.
(Cartesian p, KnownNat n) =>
p a b -> p (Finite n -> a) (Finite n -> b)
proPower p x b
p) (q a x -> q (Finite n -> a) (Finite n -> x)
forall (n :: Nat) a b.
KnownNat n =>
q a b -> q (Finite n -> a) (Finite n -> b)
forall (p :: * -> * -> *) (n :: Nat) a b.
(Cartesian p, KnownNat n) =>
p a b -> p (Finite n -> a) (Finite n -> b)
proPower q a x
q)

instance (Cartesian p) => Cartesian (Yoneda p) where
  proUnit :: forall a. Yoneda p a ()
proUnit = p a () -> Yoneda p a ()
p :-> Yoneda p
forall (p :: * -> * -> *). Profunctor p => p :-> Yoneda p
forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorMonad t, Profunctor p) =>
p :-> t p
proreturn p a ()
forall a. p a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit
  Yoneda p a b
p *** :: forall a b a' b'.
Yoneda p a b -> Yoneda p a' b' -> Yoneda p (a, a') (b, b')
*** Yoneda p a' b'
q = p (a, a') (b, b') -> Yoneda p (a, a') (b, b')
p :-> Yoneda p
forall (p :: * -> * -> *). Profunctor p => p :-> Yoneda p
forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorMonad t, Profunctor p) =>
p :-> t p
proreturn (Yoneda p a b -> p a b
Yoneda p :-> p
forall (p :: * -> * -> *). Profunctor p => Yoneda p :-> p
forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorComonad t, Profunctor p) =>
t p :-> p
proextract Yoneda p a b
p p a b -> p a' b' -> p (a, a') (b, b')
forall a b a' b'. p a b -> p a' b' -> p (a, a') (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** Yoneda p a' b' -> p a' b'
Yoneda p :-> p
forall (p :: * -> * -> *). Profunctor p => Yoneda p :-> p
forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorComonad t, Profunctor p) =>
t p :-> p
proextract Yoneda p a' b'
q)

instance (Cartesian p) => Cartesian (Coyoneda p) where
  proUnit :: forall a. Coyoneda p a ()
proUnit = p a () -> Coyoneda p a ()
p :-> Coyoneda p
forall (p :: * -> * -> *). Profunctor p => p :-> Coyoneda p
forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorMonad t, Profunctor p) =>
p :-> t p
proreturn p a ()
forall a. p a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit
  Coyoneda a -> x
l1 y -> b
r1 p x y
p *** :: forall a b a' b'.
Coyoneda p a b -> Coyoneda p a' b' -> Coyoneda p (a, a') (b, b')
*** Coyoneda a' -> x
l2 y -> b'
r2 p x y
q
    = ((a, a') -> (x, x))
-> ((y, y) -> (b, b'))
-> p (x, x) (y, y)
-> Coyoneda p (a, a') (b, b')
forall a x y b (p :: * -> * -> *).
(a -> x) -> (y -> b) -> p x y -> Coyoneda p a b
Coyoneda (a -> x
l1 (a -> x) -> (a' -> x) -> (a, a') -> (x, x)
forall a b a' b'. (a -> b) -> (a' -> b') -> (a, a') -> (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** a' -> x
l2) (y -> b
r1 (y -> b) -> (y -> b') -> (y, y) -> (b, b')
forall a b a' b'. (a -> b) -> (a' -> b') -> (a, a') -> (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** y -> b'
r2) (p x y
p p x y -> p x y -> p (x, x) (y, y)
forall a b a' b'. p a b -> p a' b' -> p (a, a') (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** p x y
q)

class Profunctor p => Cocartesian p where
  {-# MINIMAL proEmpty, (proSum | (+++) | (|||)) #-}

  -- | Unit of the sum.
  --
  -- The type of 'proEmpty' can be understood as @proEmpty' :: p Void 'Void'@
  -- treated to have more generally-typed @p Void b@ using 'rmap'.
  -- 
  -- @
  -- 'absurd'    :: Void -> b
  -- proEmpty' :: p Void Void
  -- 'rmap' absurd proEmpty' :: p Void b
  -- @
  proEmpty :: p Void b
  
  proSum :: (a -> Either a1 a2) -> (Either b1 b2 -> b) -> p a1 b1 -> p a2 b2 -> p a b
  proSum a -> Either a1 a2
f Either b1 b2 -> b
g p a1 b1
p p a2 b2
q = (a -> Either a1 a2)
-> (Either b1 b2 -> b) -> p (Either a1 a2) (Either b1 b2) -> p a b
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> Either a1 a2
f Either b1 b2 -> b
g (p a1 b1
p p a1 b1 -> p a2 b2 -> p (Either a1 a2) (Either b1 b2)
forall a b a' b'. p a b -> p a' b' -> p (Either a a') (Either b b')
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
p a b -> p a' b' -> p (Either a a') (Either b b')
+++ p a2 b2
q)

  -- | Sum of two profunctors
  (+++) :: p a b -> p a' b' -> p (Either a a') (Either b b')
  p a b
p +++ p a' b'
q = (b -> Either b b') -> p a b -> p a (Either b b')
forall b c a. (b -> c) -> p a b -> p a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap b -> Either b b'
forall a b. a -> Either a b
Left p a b
p p a (Either b b')
-> p a' (Either b b') -> p (Either a a') (Either b b')
forall a b a'. p a b -> p a' b -> p (Either a a') b
forall (p :: * -> * -> *) a b a'.
Cocartesian p =>
p a b -> p a' b -> p (Either a a') b
||| (b' -> Either b b') -> p a' b' -> p a' (Either b b')
forall b c a. (b -> c) -> p a b -> p a c
forall (p :: * -> * -> *) b c a.
Profunctor p =>
(b -> c) -> p a b -> p a c
rmap b' -> Either b b'
forall a b. b -> Either a b
Right p a' b'
q

  -- | Alternative way to define the sum (pronounced \"fan-in\")
  (|||) :: p a b -> p a' b -> p (Either a a') b
  (|||) = (Either a a' -> Either a a')
-> (Either b b -> b) -> p a b -> p a' b -> p (Either a a') b
forall a a1 a2 b1 b2 b.
(a -> Either a1 a2)
-> (Either b1 b2 -> b) -> p a1 b1 -> p a2 b2 -> p a b
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cocartesian p =>
(a -> Either a1 a2)
-> (Either b1 b2 -> b) -> p a1 b1 -> p a2 b2 -> p a b
proSum Either a a' -> Either a a'
forall a. a -> a
id Either b b -> b
forall a. Either a a -> a
nabla

  -- | Pairing with finite types can be constructed as iterated sum.
  --
  -- There is a default implementaion, but it can be more efficient implementation.
  proTimes :: KnownNat n => p a b -> p (Finite n, a) (Finite n, b)
  proTimes p a b
p = Copower p (Finite n) (Finite n)
-> forall s t. p s t -> p (Finite n, s) (Finite n, t)
forall (p :: * -> * -> *) a b.
Copower p a b -> forall s t. p s t -> p (a, s) (b, t)
runCopower Copower p (Finite n) (Finite n)
forall (n :: Nat) (p :: * -> * -> *).
(KnownNat n, Cartesian p, Cocartesian p) =>
p (Finite n) (Finite n)
describeFinite p a b
p

nabla :: Either a a -> a
nabla :: forall a. Either a a -> a
nabla = (a -> a) -> (a -> a) -> Either a a -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> a
forall a. a -> a
id a -> a
forall a. a -> a
id

sumDay :: Cocartesian r => (p :-> r) -> (q :-> r) -> Day Either p q :-> r
sumDay :: forall (r :: * -> * -> *) (p :: * -> * -> *) (q :: * -> * -> *).
Cocartesian r =>
(p :-> r) -> (q :-> r) -> Day Either p q :-> r
sumDay p :-> r
pr q :-> r
qr (Day p a1 b1
p q a2 b2
q a -> Either a1 a2
opA Either b1 b2 -> b
opB) = (a -> Either a1 a2)
-> (Either b1 b2 -> b) -> r a1 b1 -> r a2 b2 -> r a b
forall a a1 a2 b1 b2 b.
(a -> Either a1 a2)
-> (Either b1 b2 -> b) -> r a1 b1 -> r a2 b2 -> r a b
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cocartesian p =>
(a -> Either a1 a2)
-> (Either b1 b2 -> b) -> p a1 b1 -> p a2 b2 -> p a b
proSum a -> Either a1 a2
opA Either b1 b2 -> b
opB (p a1 b1 -> r a1 b1
p :-> r
pr p a1 b1
p) (q a2 b2 -> r a2 b2
q :-> r
qr q a2 b2
q)

instance Cocartesian (->) where
  proEmpty :: forall b. Void -> b
proEmpty = Void -> b
forall b. Void -> b
absurd
  a -> b
p1 +++ :: forall a b a' b'.
(a -> b) -> (a' -> b') -> Either a a' -> Either b b'
+++ a' -> b'
p2 = (a -> b) -> (a' -> b') -> Either a a' -> Either b b'
forall a b a' b'.
(a -> b) -> (a' -> b') -> Either a a' -> Either b b'
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
p1 a' -> b'
p2
  proTimes :: forall (n :: Nat) a b.
KnownNat n =>
(a -> b) -> (Finite n, a) -> (Finite n, b)
proTimes = (a -> b) -> (Finite n, a) -> (Finite n, b)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second

instance Cocartesian (Forget r) where
  proEmpty :: forall b. Forget r Void b
proEmpty = (Void -> r) -> Forget r Void b
forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget Void -> r
forall b. Void -> b
absurd
  Forget a -> r
f +++ :: forall a b a' b'.
Forget r a b
-> Forget r a' b' -> Forget r (Either a a') (Either b b')
+++ Forget a' -> r
g = (Either a a' -> r) -> Forget r (Either a a') (Either b b')
forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget ((a -> r) -> (a' -> r) -> Either a a' -> r
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> r
f a' -> r
g)
  proTimes :: forall (n :: Nat) a b.
KnownNat n =>
Forget r a b -> Forget r (Finite n, a) (Finite n, b)
proTimes (Forget a -> r
f) = ((Finite n, a) -> r) -> Forget r (Finite n, a) (Finite n, b)
forall {k} r a (b :: k). (a -> r) -> Forget r a b
Forget (a -> r
f (a -> r) -> ((Finite n, a) -> a) -> (Finite n, a) -> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Finite n, a) -> a
forall a b. (a, b) -> b
snd)

instance (Functor f) => Cocartesian (Star f) where
  proEmpty :: forall b. Star f Void b
proEmpty = (Void -> f b) -> Star f Void b
forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star Void -> f b
forall b. Void -> b
absurd
  Star a -> f b
p1 +++ :: forall a b a' b'.
Star f a b -> Star f a' b' -> Star f (Either a a') (Either b b')
+++ Star a' -> f b'
p2 = (Either a a' -> f (Either b b'))
-> Star f (Either a a') (Either b b')
forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star ((Either a a' -> f (Either b b'))
 -> Star f (Either a a') (Either b b'))
-> (Either a a' -> f (Either b b'))
-> Star f (Either a a') (Either b b')
forall a b. (a -> b) -> a -> b
$ (a -> f (Either b b'))
-> (a' -> f (Either b b')) -> Either a a' -> f (Either b b')
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((b -> Either b b') -> f b -> f (Either b b')
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b -> Either b b'
forall a b. a -> Either a b
Left (f b -> f (Either b b')) -> (a -> f b) -> a -> f (Either b b')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> f b
p1) ((b' -> Either b b') -> f b' -> f (Either b b')
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap b' -> Either b b'
forall a b. b -> Either a b
Right (f b' -> f (Either b b')) -> (a' -> f b') -> a' -> f (Either b b')
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a' -> f b'
p2)
  proTimes :: forall (n :: Nat) a b.
KnownNat n =>
Star f a b -> Star f (Finite n, a) (Finite n, b)
proTimes (Star a -> f b
p) = ((Finite n, a) -> f (Finite n, b))
-> Star f (Finite n, a) (Finite n, b)
forall {k} (f :: k -> *) d (c :: k). (d -> f c) -> Star f d c
Star (((Finite n, a) -> f (Finite n, b))
 -> Star f (Finite n, a) (Finite n, b))
-> ((Finite n, a) -> f (Finite n, b))
-> Star f (Finite n, a) (Finite n, b)
forall a b. (a -> b) -> a -> b
$ \(Finite n
i,a
a) -> (Finite n
i,) (b -> (Finite n, b)) -> f b -> f (Finite n, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f b
p a
a

instance (Alternative f) => Cocartesian (Joker f) where
  proEmpty :: forall b. Joker f Void b
proEmpty = f b -> Joker f Void b
forall {k} {k1} (g :: k -> *) (a :: k1) (b :: k).
g b -> Joker g a b
Joker f b
forall a. f a
forall (f :: * -> *) a. Alternative f => f a
empty
  Joker f b
p1 +++ :: forall a b a' b'.
Joker f a b -> Joker f a' b' -> Joker f (Either a a') (Either b b')
+++ Joker f b'
p2 = f (Either b b') -> Joker f (Either a a') (Either b b')
forall {k} {k1} (g :: k -> *) (a :: k1) (b :: k).
g b -> Joker g a b
Joker (f (Either b b') -> Joker f (Either a a') (Either b b'))
-> f (Either b b') -> Joker f (Either a a') (Either b b')
forall a b. (a -> b) -> a -> b
$ (b -> Either b b'
forall a b. a -> Either a b
Left (b -> Either b b') -> f b -> f (Either b b')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f b
p1) f (Either b b') -> f (Either b b') -> f (Either b b')
forall a. f a -> f a -> f a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (b' -> Either b b'
forall a b. b -> Either a b
Right (b' -> Either b b') -> f b' -> f (Either b b')
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f b'
p2)

instance (Decidable f) => Cocartesian (Clown f) where
  proEmpty :: forall b. Clown f Void b
proEmpty = f Void -> Clown f Void b
forall {k} {k1} (f :: k -> *) (a :: k) (b :: k1).
f a -> Clown f a b
Clown f Void
forall (f :: * -> *). Decidable f => f Void
lost
  Clown f a
p1 +++ :: forall a b a' b'.
Clown f a b -> Clown f a' b' -> Clown f (Either a a') (Either b b')
+++ Clown f a'
p2 = f (Either a a') -> Clown f (Either a a') (Either b b')
forall {k} {k1} (f :: k -> *) (a :: k) (b :: k1).
f a -> Clown f a b
Clown (f (Either a a') -> Clown f (Either a a') (Either b b'))
-> f (Either a a') -> Clown f (Either a a') (Either b b')
forall a b. (a -> b) -> a -> b
$ f a -> f a' -> f (Either a a')
forall (f :: * -> *) b c.
Decidable f =>
f b -> f c -> f (Either b c)
chosen f a
p1 f a'
p2

instance (Cocartesian p, Cocartesian q)
       => Cocartesian (Product p q) where
  proEmpty :: forall b. Product p q Void b
proEmpty = p Void b -> q Void b -> Product p q Void b
forall {k} {k1} (f :: k -> k1 -> *) (g :: k -> k1 -> *) (a :: k)
       (b :: k1).
f a b -> g a b -> Product f g a b
Pair p Void b
forall b. p Void b
forall (p :: * -> * -> *) b. Cocartesian p => p Void b
proEmpty q Void b
forall b. q Void b
forall (p :: * -> * -> *) b. Cocartesian p => p Void b
proEmpty
  Pair p a b
p1 q a b
q1 +++ :: forall a b a' b'.
Product p q a b
-> Product p q a' b' -> Product p q (Either a a') (Either b b')
+++ Pair p a' b'
p2 q a' b'
q2 = p (Either a a') (Either b b')
-> q (Either a a') (Either b b')
-> Product p q (Either a a') (Either b b')
forall {k} {k1} (f :: k -> k1 -> *) (g :: k -> k1 -> *) (a :: k)
       (b :: k1).
f a b -> g a b -> Product f g a b
Pair (p a b
p1 p a b -> p a' b' -> p (Either a a') (Either b b')
forall a b a' b'. p a b -> p a' b' -> p (Either a a') (Either b b')
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
p a b -> p a' b' -> p (Either a a') (Either b b')
+++ p a' b'
p2) (q a b
q1 q a b -> q a' b' -> q (Either a a') (Either b b')
forall a b a' b'. q a b -> q a' b' -> q (Either a a') (Either b b')
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
p a b -> p a' b' -> p (Either a a') (Either b b')
+++ q a' b'
q2)
  proTimes :: forall (n :: Nat) a b.
KnownNat n =>
Product p q a b -> Product p q (Finite n, a) (Finite n, b)
proTimes (Pair p a b
p q a b
q) = p (Finite n, a) (Finite n, b)
-> q (Finite n, a) (Finite n, b)
-> Product p q (Finite n, a) (Finite n, b)
forall {k} {k1} (f :: k -> k1 -> *) (g :: k -> k1 -> *) (a :: k)
       (b :: k1).
f a b -> g a b -> Product f g a b
Pair (p a b -> p (Finite n, a) (Finite n, b)
forall (n :: Nat) a b.
KnownNat n =>
p a b -> p (Finite n, a) (Finite n, b)
forall (p :: * -> * -> *) (n :: Nat) a b.
(Cocartesian p, KnownNat n) =>
p a b -> p (Finite n, a) (Finite n, b)
proTimes p a b
p) (q a b -> q (Finite n, a) (Finite n, b)
forall (n :: Nat) a b.
KnownNat n =>
q a b -> q (Finite n, a) (Finite n, b)
forall (p :: * -> * -> *) (n :: Nat) a b.
(Cocartesian p, KnownNat n) =>
p a b -> p (Finite n, a) (Finite n, b)
proTimes q a b
q)

instance (Cocartesian p, Cocartesian q)
       => Cocartesian (Procompose p q) where
  proEmpty :: forall b. Procompose p q Void b
proEmpty = p Void b -> q Void Void -> Procompose p q Void b
forall {k} {k1} {k2} (p :: k -> k1 -> *) (x :: k) (c :: k1)
       (q :: k2 -> k -> *) (d :: k2).
p x c -> q d x -> Procompose p q d c
Procompose p Void b
forall b. p Void b
forall (p :: * -> * -> *) b. Cocartesian p => p Void b
proEmpty q Void Void
forall b. q Void b
forall (p :: * -> * -> *) b. Cocartesian p => p Void b
proEmpty
  Procompose p x b
p1 q a x
q1 +++ :: forall a b a' b'.
Procompose p q a b
-> Procompose p q a' b'
-> Procompose p q (Either a a') (Either b b')
+++ Procompose p x b'
p2 q a' x
q2 = p (Either x x) (Either b b')
-> q (Either a a') (Either x x)
-> Procompose p q (Either a a') (Either b b')
forall {k} {k1} {k2} (p :: k -> k1 -> *) (x :: k) (c :: k1)
       (q :: k2 -> k -> *) (d :: k2).
p x c -> q d x -> Procompose p q d c
Procompose (p x b
p1 p x b -> p x b' -> p (Either x x) (Either b b')
forall a b a' b'. p a b -> p a' b' -> p (Either a a') (Either b b')
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
p a b -> p a' b' -> p (Either a a') (Either b b')
+++ p x b'
p2) (q a x
q1 q a x -> q a' x -> q (Either a a') (Either x x)
forall a b a' b'. q a b -> q a' b' -> q (Either a a') (Either b b')
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
p a b -> p a' b' -> p (Either a a') (Either b b')
+++ q a' x
q2)
  proTimes :: forall (n :: Nat) a b.
KnownNat n =>
Procompose p q a b -> Procompose p q (Finite n, a) (Finite n, b)
proTimes (Procompose p x b
p q a x
q) = p (Finite n, x) (Finite n, b)
-> q (Finite n, a) (Finite n, x)
-> Procompose p q (Finite n, a) (Finite n, b)
forall {k} {k1} {k2} (p :: k -> k1 -> *) (x :: k) (c :: k1)
       (q :: k2 -> k -> *) (d :: k2).
p x c -> q d x -> Procompose p q d c
Procompose (p x b -> p (Finite n, x) (Finite n, b)
forall (n :: Nat) a b.
KnownNat n =>
p a b -> p (Finite n, a) (Finite n, b)
forall (p :: * -> * -> *) (n :: Nat) a b.
(Cocartesian p, KnownNat n) =>
p a b -> p (Finite n, a) (Finite n, b)
proTimes p x b
p) (q a x -> q (Finite n, a) (Finite n, x)
forall (n :: Nat) a b.
KnownNat n =>
q a b -> q (Finite n, a) (Finite n, b)
forall (p :: * -> * -> *) (n :: Nat) a b.
(Cocartesian p, KnownNat n) =>
p a b -> p (Finite n, a) (Finite n, b)
proTimes q a x
q)

instance (Cocartesian p) => Cocartesian (Yoneda p) where
  proEmpty :: forall b. Yoneda p Void b
proEmpty = p Void b -> Yoneda p Void b
p :-> Yoneda p
forall (p :: * -> * -> *). Profunctor p => p :-> Yoneda p
forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorMonad t, Profunctor p) =>
p :-> t p
proreturn p Void b
forall b. p Void b
forall (p :: * -> * -> *) b. Cocartesian p => p Void b
proEmpty
  Yoneda p a b
p +++ :: forall a b a' b'.
Yoneda p a b
-> Yoneda p a' b' -> Yoneda p (Either a a') (Either b b')
+++ Yoneda p a' b'
q = p (Either a a') (Either b b')
-> Yoneda p (Either a a') (Either b b')
p :-> Yoneda p
forall (p :: * -> * -> *). Profunctor p => p :-> Yoneda p
forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorMonad t, Profunctor p) =>
p :-> t p
proreturn (Yoneda p a b -> p a b
Yoneda p :-> p
forall (p :: * -> * -> *). Profunctor p => Yoneda p :-> p
forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorComonad t, Profunctor p) =>
t p :-> p
proextract Yoneda p a b
p p a b -> p a' b' -> p (Either a a') (Either b b')
forall a b a' b'. p a b -> p a' b' -> p (Either a a') (Either b b')
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
p a b -> p a' b' -> p (Either a a') (Either b b')
+++ Yoneda p a' b' -> p a' b'
Yoneda p :-> p
forall (p :: * -> * -> *). Profunctor p => Yoneda p :-> p
forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorComonad t, Profunctor p) =>
t p :-> p
proextract Yoneda p a' b'
q)

instance (Cocartesian p) => Cocartesian (Coyoneda p) where
  proEmpty :: forall b. Coyoneda p Void b
proEmpty = p Void b -> Coyoneda p Void b
p :-> Coyoneda p
forall (p :: * -> * -> *). Profunctor p => p :-> Coyoneda p
forall (t :: (* -> * -> *) -> * -> * -> *) (p :: * -> * -> *).
(ProfunctorMonad t, Profunctor p) =>
p :-> t p
proreturn p Void b
forall b. p Void b
forall (p :: * -> * -> *) b. Cocartesian p => p Void b
proEmpty
  Coyoneda a -> x
l1 y -> b
r1 p x y
p +++ :: forall a b a' b'.
Coyoneda p a b
-> Coyoneda p a' b' -> Coyoneda p (Either a a') (Either b b')
+++ Coyoneda a' -> x
l2 y -> b'
r2 p x y
q
    = (Either a a' -> Either x x)
-> (Either y y -> Either b b')
-> p (Either x x) (Either y y)
-> Coyoneda p (Either a a') (Either b b')
forall a x y b (p :: * -> * -> *).
(a -> x) -> (y -> b) -> p x y -> Coyoneda p a b
Coyoneda (a -> x
l1 (a -> x) -> (a' -> x) -> Either a a' -> Either x x
forall a b a' b'.
(a -> b) -> (a' -> b') -> Either a a' -> Either b b'
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
p a b -> p a' b' -> p (Either a a') (Either b b')
+++ a' -> x
l2) (y -> b
r1 (y -> b) -> (y -> b') -> Either y y -> Either b b'
forall a b a' b'.
(a -> b) -> (a' -> b') -> Either a a' -> Either b b'
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
p a b -> p a' b' -> p (Either a a') (Either b b')
+++ y -> b'
r2) (p x y
p p x y -> p x y -> p (Either x x) (Either y y)
forall a b a' b'. p a b -> p a' b' -> p (Either a a') (Either b b')
forall (p :: * -> * -> *) a b a' b'.
Cocartesian p =>
p a b -> p a' b' -> p (Either a a') (Either b b')
+++ p x y
q)

--

newtype Power p a b = Power { forall (p :: * -> * -> *) a b.
Power p a b -> forall s t. p s t -> p (b -> s) (a -> t)
runPower :: forall s t. p s t -> p (b -> s) (a -> t) }

instance Profunctor p => Profunctor (Power p) where
    dimap :: forall a b c d. (a -> b) -> (c -> d) -> Power p b c -> Power p a d
dimap a -> b
f c -> d
g (Power forall s t. p s t -> p (c -> s) (b -> t)
k) = (forall s t. p s t -> p (d -> s) (a -> t)) -> Power p a d
forall (p :: * -> * -> *) a b.
(forall s t. p s t -> p (b -> s) (a -> t)) -> Power p a b
Power (((d -> s) -> c -> s)
-> ((b -> t) -> a -> t)
-> p (c -> s) (b -> t)
-> p (d -> s) (a -> t)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((d -> s) -> (c -> d) -> c -> s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. c -> d
g) ((b -> t) -> (a -> b) -> a -> t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) (p (c -> s) (b -> t) -> p (d -> s) (a -> t))
-> (p s t -> p (c -> s) (b -> t)) -> p s t -> p (d -> s) (a -> t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p s t -> p (c -> s) (b -> t)
forall s t. p s t -> p (c -> s) (b -> t)
k)

instance Profunctor p => Cartesian (Power p) where
    proUnit :: forall a. Power p a ()
proUnit = (forall s t. p s t -> p (() -> s) (a -> t)) -> Power p a ()
forall (p :: * -> * -> *) a b.
(forall s t. p s t -> p (b -> s) (a -> t)) -> Power p a b
Power ((forall s t. p s t -> p (() -> s) (a -> t)) -> Power p a ())
-> (forall s t. p s t -> p (() -> s) (a -> t)) -> Power p a ()
forall a b. (a -> b) -> a -> b
$ ((() -> s) -> s) -> (t -> a -> t) -> p s t -> p (() -> s) (a -> t)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((() -> s) -> () -> s
forall a b. (a -> b) -> a -> b
$ ()) t -> a -> t
forall a b. a -> b -> a
const
    Power p a b
ep *** :: forall a b a' b'.
Power p a b -> Power p a' b' -> Power p (a, a') (b, b')
*** Power p a' b'
eq = (forall s t. p s t -> p ((b, b') -> s) ((a, a') -> t))
-> Power p (a, a') (b, b')
forall (p :: * -> * -> *) a b.
(forall s t. p s t -> p (b -> s) (a -> t)) -> Power p a b
Power ((forall s t. p s t -> p ((b, b') -> s) ((a, a') -> t))
 -> Power p (a, a') (b, b'))
-> (forall s t. p s t -> p ((b, b') -> s) ((a, a') -> t))
-> Power p (a, a') (b, b')
forall a b. (a -> b) -> a -> b
$ \p s t
e -> (((b, b') -> s) -> b -> b' -> s)
-> ((a -> a' -> t) -> (a, a') -> t)
-> p (b -> b' -> s) (a -> a' -> t)
-> p ((b, b') -> s) ((a, a') -> t)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((b, b') -> s) -> b -> b' -> s
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (a -> a' -> t) -> (a, a') -> t
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (p (b -> b' -> s) (a -> a' -> t)
 -> p ((b, b') -> s) ((a, a') -> t))
-> p (b -> b' -> s) (a -> a' -> t)
-> p ((b, b') -> s) ((a, a') -> t)
forall a b. (a -> b) -> a -> b
$ Power p a b -> forall s t. p s t -> p (b -> s) (a -> t)
forall (p :: * -> * -> *) a b.
Power p a b -> forall s t. p s t -> p (b -> s) (a -> t)
runPower Power p a b
ep (Power p a' b' -> forall s t. p s t -> p (b' -> s) (a' -> t)
forall (p :: * -> * -> *) a b.
Power p a b -> forall s t. p s t -> p (b -> s) (a -> t)
runPower Power p a' b'
eq p s t
e)

instance Cartesian p => Cocartesian (Power p) where
    proEmpty :: forall b. Power p Void b
proEmpty = (forall s t. p s t -> p (b -> s) (Void -> t)) -> Power p Void b
forall (p :: * -> * -> *) a b.
(forall s t. p s t -> p (b -> s) (a -> t)) -> Power p a b
Power ((forall s t. p s t -> p (b -> s) (Void -> t)) -> Power p Void b)
-> (forall s t. p s t -> p (b -> s) (Void -> t)) -> Power p Void b
forall a b. (a -> b) -> a -> b
$ \p s t
_ -> ((b -> s) -> b -> s)
-> (() -> Void -> t) -> p (b -> s) () -> p (b -> s) (Void -> t)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (b -> s) -> b -> s
forall a. a -> a
id ((Void -> t) -> () -> Void -> t
forall a b. a -> b -> a
const Void -> t
forall b. Void -> b
absurd) p (b -> s) ()
forall a. p a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit
    Power p a b
ep +++ :: forall a b a' b'.
Power p a b -> Power p a' b' -> Power p (Either a a') (Either b b')
+++ Power p a' b'
eq = (forall s t. p s t -> p (Either b b' -> s) (Either a a' -> t))
-> Power p (Either a a') (Either b b')
forall (p :: * -> * -> *) a b.
(forall s t. p s t -> p (b -> s) (a -> t)) -> Power p a b
Power ((forall s t. p s t -> p (Either b b' -> s) (Either a a' -> t))
 -> Power p (Either a a') (Either b b'))
-> (forall s t. p s t -> p (Either b b' -> s) (Either a a' -> t))
-> Power p (Either a a') (Either b b')
forall a b. (a -> b) -> a -> b
$ \p s t
e -> ((Either b b' -> s) -> (b -> s, b' -> s))
-> ((a -> t, a' -> t) -> Either a a' -> t)
-> p (b -> s) (a -> t)
-> p (b' -> s) (a' -> t)
-> p (Either b b' -> s) (Either a a' -> t)
forall a a1 a2 b1 b2 b.
(a -> (a1, a2)) -> ((b1, b2) -> b) -> p a1 b1 -> p a2 b2 -> p a b
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cartesian p =>
(a -> (a1, a2)) -> ((b1, b2) -> b) -> p a1 b1 -> p a2 b2 -> p a b
proProduct (\Either b b' -> s
f -> (Either b b' -> s
f (Either b b' -> s) -> (b -> Either b b') -> b -> s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> Either b b'
forall a b. a -> Either a b
Left, Either b b' -> s
f (Either b b' -> s) -> (b' -> Either b b') -> b' -> s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b' -> Either b b'
forall a b. b -> Either a b
Right)) (((a -> t) -> (a' -> t) -> Either a a' -> t)
-> (a -> t, a' -> t) -> Either a a' -> t
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (a -> t) -> (a' -> t) -> Either a a' -> t
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either) (Power p a b -> forall s t. p s t -> p (b -> s) (a -> t)
forall (p :: * -> * -> *) a b.
Power p a b -> forall s t. p s t -> p (b -> s) (a -> t)
runPower Power p a b
ep p s t
e) (Power p a' b' -> forall s t. p s t -> p (b' -> s) (a' -> t)
forall (p :: * -> * -> *) a b.
Power p a b -> forall s t. p s t -> p (b -> s) (a -> t)
runPower Power p a' b'
eq p s t
e)
    proTimes :: forall (n :: Nat) a b.
KnownNat n =>
Power p a b -> Power p (Finite n, a) (Finite n, b)
proTimes Power p a b
p = (forall s t. p s t -> p ((Finite n, b) -> s) ((Finite n, a) -> t))
-> Power p (Finite n, a) (Finite n, b)
forall (p :: * -> * -> *) a b.
(forall s t. p s t -> p (b -> s) (a -> t)) -> Power p a b
Power ((forall s t. p s t -> p ((Finite n, b) -> s) ((Finite n, a) -> t))
 -> Power p (Finite n, a) (Finite n, b))
-> (forall s t.
    p s t -> p ((Finite n, b) -> s) ((Finite n, a) -> t))
-> Power p (Finite n, a) (Finite n, b)
forall a b. (a -> b) -> a -> b
$ \p s t
e -> (((Finite n, b) -> s) -> Finite n -> b -> s)
-> ((Finite n -> a -> t) -> (Finite n, a) -> t)
-> p (Finite n -> b -> s) (Finite n -> a -> t)
-> p ((Finite n, b) -> s) ((Finite n, a) -> t)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((Finite n, b) -> s) -> Finite n -> b -> s
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (Finite n -> a -> t) -> (Finite n, a) -> t
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (p (Finite n -> b -> s) (Finite n -> a -> t)
 -> p ((Finite n, b) -> s) ((Finite n, a) -> t))
-> p (Finite n -> b -> s) (Finite n -> a -> t)
-> p ((Finite n, b) -> s) ((Finite n, a) -> t)
forall a b. (a -> b) -> a -> b
$ p (b -> s) (a -> t) -> p (Finite n -> b -> s) (Finite n -> a -> t)
forall (n :: Nat) a b.
KnownNat n =>
p a b -> p (Finite n -> a) (Finite n -> b)
forall (p :: * -> * -> *) (n :: Nat) a b.
(Cartesian p, KnownNat n) =>
p a b -> p (Finite n -> a) (Finite n -> b)
proPower (Power p a b -> forall s t. p s t -> p (b -> s) (a -> t)
forall (p :: * -> * -> *) a b.
Power p a b -> forall s t. p s t -> p (b -> s) (a -> t)
runPower Power p a b
p p s t
e)

--

newtype Copower p a b = Copower { forall (p :: * -> * -> *) a b.
Copower p a b -> forall s t. p s t -> p (a, s) (b, t)
runCopower :: forall s t. p s t -> p (a,s) (b,t) }

instance Profunctor p => Profunctor (Copower p) where
  dimap :: forall a b c d.
(a -> b) -> (c -> d) -> Copower p b c -> Copower p a d
dimap a -> b
f c -> d
g (Copower forall s t. p s t -> p (b, s) (c, t)
k) = (forall s t. p s t -> p (a, s) (d, t)) -> Copower p a d
forall (p :: * -> * -> *) a b.
(forall s t. p s t -> p (a, s) (b, t)) -> Copower p a b
Copower ((forall s t. p s t -> p (a, s) (d, t)) -> Copower p a d)
-> (forall s t. p s t -> p (a, s) (d, t)) -> Copower p a d
forall a b. (a -> b) -> a -> b
$ \p s t
p -> ((a, s) -> (b, s))
-> ((c, t) -> (d, t)) -> p (b, s) (c, t) -> p (a, s) (d, t)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((a -> b) -> (a, s) -> (b, s)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first a -> b
f) ((c -> d) -> (c, t) -> (d, t)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first c -> d
g) (p s t -> p (b, s) (c, t)
forall s t. p s t -> p (b, s) (c, t)
k p s t
p)

instance Profunctor p => Cartesian (Copower p) where
  proUnit :: forall a. Copower p a ()
proUnit = (forall s t. p s t -> p (a, s) ((), t)) -> Copower p a ()
forall (p :: * -> * -> *) a b.
(forall s t. p s t -> p (a, s) (b, t)) -> Copower p a b
Copower ((forall s t. p s t -> p (a, s) ((), t)) -> Copower p a ())
-> (forall s t. p s t -> p (a, s) ((), t)) -> Copower p a ()
forall a b. (a -> b) -> a -> b
$ \p s t
p -> ((a, s) -> s) -> (t -> ((), t)) -> p s t -> p (a, s) ((), t)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (a, s) -> s
forall a b. (a, b) -> b
snd ((),) p s t
p
  Copower p a b
cp *** :: forall a b a' b'.
Copower p a b -> Copower p a' b' -> Copower p (a, a') (b, b')
*** Copower p a' b'
cq = (forall s t. p s t -> p ((a, a'), s) ((b, b'), t))
-> Copower p (a, a') (b, b')
forall (p :: * -> * -> *) a b.
(forall s t. p s t -> p (a, s) (b, t)) -> Copower p a b
Copower ((forall s t. p s t -> p ((a, a'), s) ((b, b'), t))
 -> Copower p (a, a') (b, b'))
-> (forall s t. p s t -> p ((a, a'), s) ((b, b'), t))
-> Copower p (a, a') (b, b')
forall a b. (a -> b) -> a -> b
$ \p s t
p -> (((a, a'), s) -> (a, (a', s)))
-> ((b, (b', t)) -> ((b, b'), t))
-> p (a, (a', s)) (b, (b', t))
-> p ((a, a'), s) ((b, b'), t)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((a, a'), s) -> (a, (a', s))
forall a1 a2 b. ((a1, a2), b) -> (a1, (a2, b))
assoc (b, (b', t)) -> ((b, b'), t)
forall a b1 b2. (a, (b1, b2)) -> ((a, b1), b2)
unassoc (p (a, (a', s)) (b, (b', t)) -> p ((a, a'), s) ((b, b'), t))
-> p (a, (a', s)) (b, (b', t)) -> p ((a, a'), s) ((b, b'), t)
forall a b. (a -> b) -> a -> b
$ Copower p a b -> forall s t. p s t -> p (a, s) (b, t)
forall (p :: * -> * -> *) a b.
Copower p a b -> forall s t. p s t -> p (a, s) (b, t)
runCopower Copower p a b
cp (Copower p a' b' -> forall s t. p s t -> p (a', s) (b', t)
forall (p :: * -> * -> *) a b.
Copower p a b -> forall s t. p s t -> p (a, s) (b, t)
runCopower Copower p a' b'
cq p s t
p)

assoc :: ((a1, a2), b) -> (a1, (a2, b))
assoc :: forall a1 a2 b. ((a1, a2), b) -> (a1, (a2, b))
assoc ((a1
a,a2
b),b
c) = (a1
a,(a2
b,b
c))
unassoc :: (a, (b1, b2)) -> ((a, b1), b2)
unassoc :: forall a b1 b2. (a, (b1, b2)) -> ((a, b1), b2)
unassoc (a
a,(b1
b,b2
c)) = ((a
a,b1
b),b2
c)

instance Cocartesian p => Cocartesian (Copower p) where
  proEmpty :: forall b. Copower p Void b
proEmpty = (forall s t. p s t -> p (Void, s) (b, t)) -> Copower p Void b
forall (p :: * -> * -> *) a b.
(forall s t. p s t -> p (a, s) (b, t)) -> Copower p a b
Copower ((forall s t. p s t -> p (Void, s) (b, t)) -> Copower p Void b)
-> (forall s t. p s t -> p (Void, s) (b, t)) -> Copower p Void b
forall a b. (a -> b) -> a -> b
$ \p s t
_ -> ((Void, s) -> Void)
-> (Void -> (b, t)) -> p Void Void -> p (Void, s) (b, t)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (Void, s) -> Void
forall a b. (a, b) -> a
fst Void -> (b, t)
forall b. Void -> b
absurd p Void Void
forall b. p Void b
forall (p :: * -> * -> *) b. Cocartesian p => p Void b
proEmpty
  Copower p a b
p +++ :: forall a b a' b'.
Copower p a b
-> Copower p a' b' -> Copower p (Either a a') (Either b b')
+++ Copower p a' b'
q = (forall s t. p s t -> p (Either a a', s) (Either b b', t))
-> Copower p (Either a a') (Either b b')
forall (p :: * -> * -> *) a b.
(forall s t. p s t -> p (a, s) (b, t)) -> Copower p a b
Copower ((forall s t. p s t -> p (Either a a', s) (Either b b', t))
 -> Copower p (Either a a') (Either b b'))
-> (forall s t. p s t -> p (Either a a', s) (Either b b', t))
-> Copower p (Either a a') (Either b b')
forall a b. (a -> b) -> a -> b
$ \p s t
c -> ((Either a a', s) -> Either (a, s) (a', s))
-> (Either (b, t) (b', t) -> (Either b b', t))
-> p (a, s) (b, t)
-> p (a', s) (b', t)
-> p (Either a a', s) (Either b b', t)
forall a a1 a2 b1 b2 b.
(a -> Either a1 a2)
-> (Either b1 b2 -> b) -> p a1 b1 -> p a2 b2 -> p a b
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cocartesian p =>
(a -> Either a1 a2)
-> (Either b1 b2 -> b) -> p a1 b1 -> p a2 b2 -> p a b
proSum (Either a a', s) -> Either (a, s) (a', s)
forall {p :: * -> * -> *} {a} {c} {t}.
Bifunctor p =>
(p a c, t) -> p (a, t) (c, t)
distrib Either (b, t) (b', t) -> (Either b b', t)
forall {a} {c} {b}. Either (a, c) (b, c) -> (Either a b, c)
undistrib (Copower p a b -> forall s t. p s t -> p (a, s) (b, t)
forall (p :: * -> * -> *) a b.
Copower p a b -> forall s t. p s t -> p (a, s) (b, t)
runCopower Copower p a b
p p s t
c) (Copower p a' b' -> forall s t. p s t -> p (a', s) (b', t)
forall (p :: * -> * -> *) a b.
Copower p a b -> forall s t. p s t -> p (a, s) (b, t)
runCopower Copower p a' b'
q p s t
c)
    where
      distrib :: (p a c, t) -> p (a, t) (c, t)
distrib (p a c
ab,t
c) = (a -> (a, t)) -> (c -> (c, t)) -> p a c -> p (a, t) (c, t)
forall a b c d. (a -> b) -> (c -> d) -> p a c -> p b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (,t
c) (,t
c) p a c
ab
      undistrib :: Either (a, c) (b, c) -> (Either a b, c)
undistrib = ((a, c) -> (Either a b, c))
-> ((b, c) -> (Either a b, c))
-> Either (a, c) (b, c)
-> (Either a b, c)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((a -> Either a b) -> (a, c) -> (Either a b, c)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first a -> Either a b
forall a b. a -> Either a b
Left) ((b -> Either a b) -> (b, c) -> (Either a b, c)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first b -> Either a b
forall a b. b -> Either a b
Right)
  proTimes :: forall (n :: Nat) a b.
KnownNat n =>
Copower p a b -> Copower p (Finite n, a) (Finite n, b)
proTimes Copower p a b
p = (forall s t. p s t -> p ((Finite n, a), s) ((Finite n, b), t))
-> Copower p (Finite n, a) (Finite n, b)
forall (p :: * -> * -> *) a b.
(forall s t. p s t -> p (a, s) (b, t)) -> Copower p a b
Copower ((forall s t. p s t -> p ((Finite n, a), s) ((Finite n, b), t))
 -> Copower p (Finite n, a) (Finite n, b))
-> (forall s t. p s t -> p ((Finite n, a), s) ((Finite n, b), t))
-> Copower p (Finite n, a) (Finite n, b)
forall a b. (a -> b) -> a -> b
$ \p s t
c -> (((Finite n, a), s) -> (Finite n, (a, s)))
-> ((Finite n, (b, t)) -> ((Finite n, b), t))
-> p (Finite n, (a, s)) (Finite n, (b, t))
-> p ((Finite n, a), s) ((Finite n, b), t)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ((Finite n, a), s) -> (Finite n, (a, s))
forall a1 a2 b. ((a1, a2), b) -> (a1, (a2, b))
assoc (Finite n, (b, t)) -> ((Finite n, b), t)
forall a b1 b2. (a, (b1, b2)) -> ((a, b1), b2)
unassoc (p (Finite n, (a, s)) (Finite n, (b, t))
 -> p ((Finite n, a), s) ((Finite n, b), t))
-> p (Finite n, (a, s)) (Finite n, (b, t))
-> p ((Finite n, a), s) ((Finite n, b), t)
forall a b. (a -> b) -> a -> b
$ p (a, s) (b, t) -> p (Finite n, (a, s)) (Finite n, (b, t))
forall (n :: Nat) a b.
KnownNat n =>
p a b -> p (Finite n, a) (Finite n, b)
forall (p :: * -> * -> *) (n :: Nat) a b.
(Cocartesian p, KnownNat n) =>
p a b -> p (Finite n, a) (Finite n, b)
proTimes (Copower p a b -> forall s t. p s t -> p (a, s) (b, t)
forall (p :: * -> * -> *) a b.
Copower p a b -> forall s t. p s t -> p (a, s) (b, t)
runCopower Copower p a b
p p s t
c)

--

describeFinite :: forall n p. (KnownNat n, Cartesian p, Cocartesian p) => p (Finite n) (Finite n)
describeFinite :: forall (n :: Nat) (p :: * -> * -> *).
(KnownNat n, Cartesian p, Cocartesian p) =>
p (Finite n) (Finite n)
describeFinite = (Finite n -> Nat)
-> (Nat -> Finite n) -> p Nat Nat -> p (Finite n) (Finite n)
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap Finite n -> Nat
forall {n :: Nat}. Finite n -> Nat
finiteToNatural Nat -> Finite n
forall {n :: Nat}. Nat -> Finite n
unsafeNaturalToFinite (Nat -> p Nat Nat
forall (p :: * -> * -> *).
(Cartesian p, Cocartesian p) =>
Nat -> p Nat Nat
dNatural (forall (n :: Nat) (proxy :: Nat -> *). KnownNat n => proxy n -> Nat
natVal @n Any n
forall a. HasCallStack => a
undefined))
  where
    finiteToNatural :: Finite n -> Nat
finiteToNatural = Integer -> Nat
forall a. Num a => Integer -> a
fromInteger (Integer -> Nat) -> (Finite n -> Integer) -> Finite n -> Nat
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Finite n -> Integer
forall (n :: Nat). Finite n -> Integer
getFinite
    unsafeNaturalToFinite :: Nat -> Finite n
unsafeNaturalToFinite = Integer -> Finite n
forall (n :: Nat). Integer -> Finite n
Unsafe.Finite (Integer -> Finite n) -> (Nat -> Integer) -> Nat -> Finite n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Integer
forall a. Integral a => a -> Integer
toInteger

dNatural :: (Cartesian p, Cocartesian p) => Natural -> p Natural Natural
dNatural :: forall (p :: * -> * -> *).
(Cartesian p, Cocartesian p) =>
Nat -> p Nat Nat
dNatural Nat
0 = (Nat -> Void) -> (Void -> Nat) -> p Void Void -> p Nat Nat
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap ([Char] -> Nat -> Void
forall a. HasCallStack => [Char] -> a
error [Char]
"here no value should come") Void -> Nat
forall b. Void -> b
absurd p Void Void
forall b. p Void b
forall (p :: * -> * -> *) b. Cocartesian p => p Void b
proEmpty
dNatural Nat
1 = (Nat -> ()) -> (() -> Nat) -> p () () -> p Nat Nat
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap (() -> Nat -> ()
forall a b. a -> b -> a
const ()) (Nat -> () -> Nat
forall a b. a -> b -> a
const Nat
0) p () ()
forall a. p a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit
dNatural Nat
2 = p Nat Nat
forall a (p :: * -> * -> *).
(Bits a, Cartesian p, Cocartesian p) =>
p a a
dBit
dNatural Nat
n = case Nat
n Nat -> Nat -> (Nat, Nat)
forall a. Integral a => a -> a -> (a, a)
`divMod` Nat
2 of
  (Nat
n',Nat
0) -> (Nat -> (Nat, Nat))
-> ((Nat, Nat) -> Nat) -> p Nat Nat -> p Nat Nat -> p Nat Nat
forall a a1 a2 b1 b2 b.
(a -> (a1, a2)) -> ((b1, b2) -> b) -> p a1 b1 -> p a2 b2 -> p a b
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cartesian p =>
(a -> (a1, a2)) -> ((b1, b2) -> b) -> p a1 b1 -> p a2 b2 -> p a b
proProduct Nat -> (Nat, Nat)
forall {a}. Integral a => a -> (a, a)
div2 (Nat, Nat) -> Nat
forall {a}. Num a => (a, a) -> a
undiv2 (Nat -> p Nat Nat
forall (p :: * -> * -> *).
(Cartesian p, Cocartesian p) =>
Nat -> p Nat Nat
dNatural Nat
n') p Nat Nat
forall a (p :: * -> * -> *).
(Bits a, Cartesian p, Cocartesian p) =>
p a a
dBit
  (Nat
n',Nat
_) -> (Nat -> Either () Nat)
-> (Either () Nat -> Nat) -> p () () -> p Nat Nat -> p Nat Nat
forall a a1 a2 b1 b2 b.
(a -> Either a1 a2)
-> (Either b1 b2 -> b) -> p a1 b1 -> p a2 b2 -> p a b
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cocartesian p =>
(a -> Either a1 a2)
-> (Either b1 b2 -> b) -> p a1 b1 -> p a2 b2 -> p a b
proSum Nat -> Either () Nat
forall {b}. (Eq b, Num b, Enum b) => b -> Either () b
unshiftNat Either () Nat -> Nat
forall {a}. Either a Nat -> Nat
shiftNat p () ()
forall a. p a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit ((Nat -> (Nat, Nat))
-> ((Nat, Nat) -> Nat) -> p Nat Nat -> p Nat Nat -> p Nat Nat
forall a a1 a2 b1 b2 b.
(a -> (a1, a2)) -> ((b1, b2) -> b) -> p a1 b1 -> p a2 b2 -> p a b
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cartesian p =>
(a -> (a1, a2)) -> ((b1, b2) -> b) -> p a1 b1 -> p a2 b2 -> p a b
proProduct Nat -> (Nat, Nat)
forall {a}. Integral a => a -> (a, a)
div2 (Nat, Nat) -> Nat
forall {a}. Num a => (a, a) -> a
undiv2 (Nat -> p Nat Nat
forall (p :: * -> * -> *).
(Cartesian p, Cocartesian p) =>
Nat -> p Nat Nat
dNatural Nat
n') p Nat Nat
forall a (p :: * -> * -> *).
(Bits a, Cartesian p, Cocartesian p) =>
p a a
dBit)
  where
    div2 :: a -> (a, a)
div2 a
x = a
x a -> a -> (a, a)
forall a. Integral a => a -> a -> (a, a)
`divMod` a
2
    undiv2 :: (a, a) -> a
undiv2 (a
q,a
r) = a
2 a -> a -> a
forall a. Num a => a -> a -> a
* a
q a -> a -> a
forall a. Num a => a -> a -> a
+ a
r
    unshiftNat :: b -> Either () b
unshiftNat b
0 = () -> Either () b
forall a b. a -> Either a b
Left ()
    unshiftNat b
x = b -> Either () b
forall a b. b -> Either a b
Right (b -> b
forall a. Enum a => a -> a
pred b
x)
    shiftNat :: Either a Nat -> Nat
shiftNat = (a -> Nat) -> (Nat -> Nat) -> Either a Nat -> Nat
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Nat -> a -> Nat
forall a b. a -> b -> a
const Nat
0) Nat -> Nat
forall a. Enum a => a -> a
succ

describeFiniteBits :: forall a p. (FiniteBits a, Cartesian p, Cocartesian p) => p a a
describeFiniteBits :: forall a (p :: * -> * -> *).
(FiniteBits a, Cartesian p, Cocartesian p) =>
p a a
describeFiniteBits = Int -> p a a
forall a (p :: * -> * -> *).
(Bits a, Cartesian p, Cocartesian p) =>
Int -> p a a
dBits (a -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize (a
forall a. Bits a => a
zeroBits :: a))

dBit :: (Bits a, Cartesian p, Cocartesian p) => p a a
dBit :: forall a (p :: * -> * -> *).
(Bits a, Cartesian p, Cocartesian p) =>
p a a
dBit = (a -> Either () ())
-> (Either () () -> a) -> p () () -> p () () -> p a a
forall a a1 a2 b1 b2 b.
(a -> Either a1 a2)
-> (Either b1 b2 -> b) -> p a1 b1 -> p a2 b2 -> p a b
forall (p :: * -> * -> *) a a1 a2 b1 b2 b.
Cocartesian p =>
(a -> Either a1 a2)
-> (Either b1 b2 -> b) -> p a1 b1 -> p a2 b2 -> p a b
proSum a -> Either () ()
forall {a}. Bits a => a -> Either () ()
i2b Either () () -> a
forall {a} {a} {b}. Bits a => Either a b -> a
b2i p () ()
forall a. p a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit p () ()
forall a. p a ()
forall (p :: * -> * -> *) a. Cartesian p => p a ()
proUnit
  where
    i2b :: a -> Either () ()
i2b a
x = if a -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit a
x Int
0 then () -> Either () ()
forall a b. b -> Either a b
Right () else () -> Either () ()
forall a b. a -> Either a b
Left ()
    b2i :: Either a b -> a
b2i (Left a
_) = a
forall a. Bits a => a
zeroBits
    b2i (Right b
_)  = Int -> a
forall a. Bits a => Int -> a
bit Int
0

dBits :: (Bits a, Cartesian p, Cocartesian p) => Int -> p a a
dBits :: forall a (p :: * -> * -> *).
(Bits a, Cartesian p, Cocartesian p) =>
Int -> p a a
dBits Int
n
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = [Char] -> p a a
forall a. HasCallStack => [Char] -> a
error [Char]
"bad!"
  | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = p a a
forall a (p :: * -> * -> *).
(Bits a, Cartesian p, Cocartesian p) =>
p a a
dBit
  | Bool
otherwise =
      case Int -> (Int, Int)
separate Int
n of
        (Int
0, Int
p) -> Int -> p a a
forall a (p :: * -> * -> *).
(Bits a, Cartesian p, Cocartesian p) =>
Int -> p a a
dBitsPow2 Int
p
        (Int
m, Int
p) ->
          let l :: b -> (b, b)
l b
x = (b
x b -> Int -> b
forall a. Bits a => a -> Int -> a
`shiftR` Int
p, b
x)
              r :: (a, a) -> a
r (a
a,a
b) = a
a a -> Int -> a
forall a. Bits a => a -> Int -> a
`shiftL` Int
p a -> a -> a
forall a. Bits a => a -> a -> a
.|. a
b
          in (a -> (a, a)) -> ((a, a) -> a) -> p (a, a) (a, a) -> p a a
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> (a, a)
forall {b}. Bits b => b -> (b, b)
l (a, a) -> a
forall {a}. Bits a => (a, a) -> a
r (p (a, a) (a, a) -> p a a) -> p (a, a) (a, a) -> p a a
forall a b. (a -> b) -> a -> b
$ Int -> p a a
forall a (p :: * -> * -> *).
(Bits a, Cartesian p, Cocartesian p) =>
Int -> p a a
dBits Int
m p a a -> p a a -> p (a, a) (a, a)
forall a b a' b'. p a b -> p a' b' -> p (a, a') (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** Int -> p a a
forall a (p :: * -> * -> *).
(Bits a, Cartesian p, Cocartesian p) =>
Int -> p a a
dBitsPow2 Int
p

separate :: Int -> (Int, Int)
-- must be x > 1
separate :: Int -> (Int, Int)
separate Int
x = (Int
r, Int -> Int
forall a. Bits a => Int -> a
bit Int
p)
  where
    p :: Int
p = Int -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize (Int
0 :: Int) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int -> Int
forall b. FiniteBits b => b -> Int
countLeadingZeros Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1
    r :: Int
r = Int -> Int -> Int
forall a. Bits a => a -> Int -> a
clearBit Int
x Int
p

dBitsPow2 :: (Bits a, Cartesian p, Cocartesian p) => Int -> p a a
dBitsPow2 :: forall a (p :: * -> * -> *).
(Bits a, Cartesian p, Cocartesian p) =>
Int -> p a a
dBitsPow2 Int
1 = p a a
forall a (p :: * -> * -> *).
(Bits a, Cartesian p, Cocartesian p) =>
p a a
dBit
dBitsPow2 Int
n =
  let m :: Int
m = Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2
      halfBits :: p a a
halfBits = Int -> p a a
forall a (p :: * -> * -> *).
(Bits a, Cartesian p, Cocartesian p) =>
Int -> p a a
dBitsPow2 Int
m
      l :: b -> (b, b)
l b
x = (b
x b -> Int -> b
forall a. Bits a => a -> Int -> a
`shift` (-Int
m), b
x)
      r :: (a, a) -> a
r (a
a,a
b) = a
a a -> Int -> a
forall a. Bits a => a -> Int -> a
`shift` Int
m a -> a -> a
forall a. Bits a => a -> a -> a
.|. a
b
  in (a -> (a, a)) -> ((a, a) -> a) -> p (a, a) (a, a) -> p a a
forall a b c d. (a -> b) -> (c -> d) -> p b c -> p a d
forall (p :: * -> * -> *) a b c d.
Profunctor p =>
(a -> b) -> (c -> d) -> p b c -> p a d
dimap a -> (a, a)
forall {b}. Bits b => b -> (b, b)
l (a, a) -> a
forall {a}. Bits a => (a, a) -> a
r (p (a, a) (a, a) -> p a a) -> p (a, a) (a, a) -> p a a
forall a b. (a -> b) -> a -> b
$ p a a
halfBits p a a -> p a a -> p (a, a) (a, a)
forall a b a' b'. p a b -> p a' b' -> p (a, a') (b, b')
forall (p :: * -> * -> *) a b a' b'.
Cartesian p =>
p a b -> p a' b' -> p (a, a') (b, b')
*** p a a
halfBits