{-# LANGUAGE DerivingVia #-}
module Data.Functor.Contravariant.Divisible.Free (
Div(.., Conquer, Divide)
, hoistDiv, liftDiv, runDiv
, divListF, listFDiv
, Div1(.., Div1_)
, hoistDiv1, liftDiv1, toDiv, runDiv1
, div1NonEmptyF, nonEmptyFDiv1
, Dec(..)
, hoistDec, liftDec, runDec
, Dec1(..)
, hoistDec1, liftDec1, toDec, runDec1
) where
import Control.Applicative.ListF
import Control.Natural
import Data.Bifunctor
import Data.Bifunctor.Assoc
import Data.Foldable
import Data.Functor.Contravariant
import Data.Functor.Contravariant.Conclude
import Data.Functor.Contravariant.Coyoneda
import Data.Functor.Contravariant.Decide
import Data.Functor.Contravariant.Divise
import Data.Functor.Contravariant.Divisible
import Data.Functor.Invariant
import Data.HFunctor
import Data.HFunctor.Interpret
import Data.Kind
import Data.List.NonEmpty (NonEmpty(..))
import Data.Void
import qualified Control.Monad.Trans.Compose as CT
import qualified Data.Functor.Contravariant.Day as CD
newtype Div f a = Div { Div f a -> [Coyoneda f a]
unDiv :: [Coyoneda f a] }
deriving (b -> Div f b -> Div f a
(a -> b) -> Div f b -> Div f a
(forall a b. (a -> b) -> Div f b -> Div f a)
-> (forall b a. b -> Div f b -> Div f a) -> Contravariant (Div f)
forall b a. b -> Div f b -> Div f a
forall a b. (a -> b) -> Div f b -> Div f a
forall (f :: * -> *).
(forall a b. (a -> b) -> f b -> f a)
-> (forall b a. b -> f b -> f a) -> Contravariant f
forall (f :: * -> *) b a. b -> Div f b -> Div f a
forall (f :: * -> *) a b. (a -> b) -> Div f b -> Div f a
>$ :: b -> Div f b -> Div f a
$c>$ :: forall (f :: * -> *) b a. b -> Div f b -> Div f a
contramap :: (a -> b) -> Div f b -> Div f a
$ccontramap :: forall (f :: * -> *) a b. (a -> b) -> Div f b -> Div f a
Contravariant, Contravariant (Div f)
Contravariant (Div f) =>
(forall a b c. (a -> (b, c)) -> Div f b -> Div f c -> Div f a)
-> Divise (Div f)
(a -> (b, c)) -> Div f b -> Div f c -> Div f a
forall a b c. (a -> (b, c)) -> Div f b -> Div f c -> Div f a
forall (f :: * -> *). Contravariant (Div f)
forall (f :: * -> *).
Contravariant f =>
(forall a b c. (a -> (b, c)) -> f b -> f c -> f a) -> Divise f
forall (f :: * -> *) a b c.
(a -> (b, c)) -> Div f b -> Div f c -> Div f a
divise :: (a -> (b, c)) -> Div f b -> Div f c -> Div f a
$cdivise :: forall (f :: * -> *) a b c.
(a -> (b, c)) -> Div f b -> Div f c -> Div f a
$cp1Divise :: forall (f :: * -> *). Contravariant (Div f)
Divise, Contravariant (Div f)
Div f a
Contravariant (Div f) =>
(forall a b c. (a -> (b, c)) -> Div f b -> Div f c -> Div f a)
-> (forall a. Div f a) -> Divisible (Div f)
(a -> (b, c)) -> Div f b -> Div f c -> Div f a
forall a. Div f a
forall a b c. (a -> (b, c)) -> Div f b -> Div f c -> Div f a
forall (f :: * -> *). Contravariant (Div f)
forall (f :: * -> *).
Contravariant f =>
(forall a b c. (a -> (b, c)) -> f b -> f c -> f a)
-> (forall a. f a) -> Divisible f
forall (f :: * -> *) a. Div f a
forall (f :: * -> *) a b c.
(a -> (b, c)) -> Div f b -> Div f c -> Div f a
conquer :: Div f a
$cconquer :: forall (f :: * -> *) a. Div f a
divide :: (a -> (b, c)) -> Div f b -> Div f c -> Div f a
$cdivide :: forall (f :: * -> *) a b c.
(a -> (b, c)) -> Div f b -> Div f c -> Div f a
$cp1Divisible :: forall (f :: * -> *). Contravariant (Div f)
Divisible) via (ListF (Coyoneda f))
deriving ((f ~> g) -> Div f ~> Div g
(forall (f :: * -> *) (g :: * -> *). (f ~> g) -> Div f ~> Div g)
-> HFunctor Div
forall k k (t :: (k -> *) -> k -> *).
(forall (f :: k -> *) (g :: k -> *). (f ~> g) -> t f ~> t g)
-> HFunctor t
forall (f :: * -> *) (g :: * -> *). (f ~> g) -> Div f ~> Div g
hmap :: (f ~> g) -> Div f ~> Div g
$chmap :: forall (f :: * -> *) (g :: * -> *). (f ~> g) -> Div f ~> Div g
HFunctor, HFunctor Div
f x -> Div f x
HFunctor Div => (forall (f :: * -> *). f ~> Div f) -> Inject Div
forall k (t :: (k -> *) -> k -> *).
HFunctor t =>
(forall (f :: k -> *). f ~> t f) -> Inject t
forall (f :: * -> *). f ~> Div f
inject :: f x -> Div f x
$cinject :: forall (f :: * -> *). f ~> Div f
$cp1Inject :: HFunctor Div
Inject) via (CT.ComposeT ListF Coyoneda)
instance Invariant (Div f) where
invmap :: (a -> b) -> (b -> a) -> Div f a -> Div f b
invmap _ = (b -> a) -> Div f a -> Div f b
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap
pattern Conquer :: Div f a
pattern $bConquer :: Div f a
$mConquer :: forall r (f :: * -> *) a.
Div f a -> (Void# -> r) -> (Void# -> r) -> r
Conquer = Div []
pattern Divide :: (a -> (b, c)) -> f b -> Div f c -> Div f a
pattern $bDivide :: (a -> (b, c)) -> f b -> Div f c -> Div f a
$mDivide :: forall r a (f :: * -> *).
Div f a
-> (forall b c. (a -> (b, c)) -> f b -> Div f c -> r)
-> (Void# -> r)
-> r
Divide f x xs <- (divDay_ -> Just (CD.Day x xs f))
where
Divide f :: a -> (b, c)
f x :: f b
x (Div xs :: [Coyoneda f c]
xs) = [Coyoneda f a] -> Div f a
forall (f :: * -> *) a. [Coyoneda f a] -> Div f a
Div ([Coyoneda f a] -> Div f a) -> [Coyoneda f a] -> Div f a
forall a b. (a -> b) -> a -> b
$ (a -> b) -> f b -> Coyoneda f a
forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
Coyoneda ((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)
f) f b
x Coyoneda f a -> [Coyoneda f a] -> [Coyoneda f a]
forall a. a -> [a] -> [a]
: ((Coyoneda f c -> Coyoneda f a) -> [Coyoneda f c] -> [Coyoneda f a]
forall a b. (a -> b) -> [a] -> [b]
map ((Coyoneda f c -> Coyoneda f a)
-> [Coyoneda f c] -> [Coyoneda f a])
-> ((a -> c) -> Coyoneda f c -> Coyoneda f a)
-> (a -> c)
-> [Coyoneda f c]
-> [Coyoneda f a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> c) -> Coyoneda f c -> Coyoneda f a
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap) ((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)
f) [Coyoneda f c]
xs
{-# COMPLETE Conquer, Divide #-}
divDay_ :: Div f a -> Maybe (CD.Day f (Div f) a)
divDay_ :: Div f a -> Maybe (Day f (Div f) a)
divDay_ (Div []) = Maybe (Day f (Div f) a)
forall a. Maybe a
Nothing
divDay_ (Div (Coyoneda f :: a -> b
f x :: f b
x : xs :: [Coyoneda f a]
xs)) = Day f (Div f) a -> Maybe (Day f (Div f) a)
forall a. a -> Maybe a
Just (Day f (Div f) a -> Maybe (Day f (Div f) a))
-> Day f (Div f) a -> Maybe (Day f (Div f) a)
forall a b. (a -> b) -> a -> b
$ f b -> Div f a -> (a -> (b, a)) -> Day f (Div f) a
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
CD.Day f b
x ([Coyoneda f a] -> Div f a
forall (f :: * -> *) a. [Coyoneda f a] -> Div f a
Div [Coyoneda f a]
xs) (\y :: a
y -> (a -> b
f a
y, a
y))
divListF :: forall f. Contravariant f => Div f ~> ListF f
divListF :: Div f ~> ListF f
divListF = [f x] -> ListF f x
forall k (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF ([f x] -> ListF f x) -> (Div f x -> [f x]) -> Div f x -> ListF f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Coyoneda f x -> f x) -> [Coyoneda f x] -> [f x]
forall a b. (a -> b) -> [a] -> [b]
map Coyoneda f x -> f x
forall (f :: * -> *) a. Contravariant f => Coyoneda f a -> f a
lowerCoyoneda ([Coyoneda f x] -> [f x])
-> (Div f x -> [Coyoneda f x]) -> Div f x -> [f x]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Div f x -> [Coyoneda f x]
forall (f :: * -> *) a. Div f a -> [Coyoneda f a]
unDiv
listFDiv :: ListF f ~> Div f
listFDiv :: ListF f x -> Div f x
listFDiv = [Coyoneda f x] -> Div f x
forall (f :: * -> *) a. [Coyoneda f a] -> Div f a
Div ([Coyoneda f x] -> Div f x)
-> (ListF f x -> [Coyoneda f x]) -> ListF f x -> Div f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f x -> Coyoneda f x) -> [f x] -> [Coyoneda f x]
forall a b. (a -> b) -> [a] -> [b]
map f x -> Coyoneda f x
forall (f :: * -> *) a. f a -> Coyoneda f a
liftCoyoneda ([f x] -> [Coyoneda f x])
-> (ListF f x -> [f x]) -> ListF f x -> [Coyoneda f x]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ListF f x -> [f x]
forall k (f :: k -> *) (a :: k). ListF f a -> [f a]
runListF
hoistDiv :: forall f g. (f ~> g) -> Div f ~> Div g
hoistDiv :: (f ~> g) -> Div f ~> Div g
hoistDiv = (f ~> g) -> Div f x -> Div g x
forall k k (t :: (k -> *) -> k -> *) (f :: k -> *) (g :: k -> *).
HFunctor t =>
(f ~> g) -> t f ~> t g
hmap
liftDiv :: f ~> Div f
liftDiv :: f x -> Div f x
liftDiv = f x -> Div f x
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
runDiv :: forall f g. Divisible g => (f ~> g) -> Div f ~> g
runDiv :: (f ~> g) -> Div f ~> g
runDiv f :: f ~> g
f = (Coyoneda f x -> g x -> g x) -> g x -> [Coyoneda f x] -> g x
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Coyoneda f x -> g x -> g x
go g x
forall (f :: * -> *) a. Divisible f => f a
conquer ([Coyoneda f x] -> g x)
-> (Div f x -> [Coyoneda f x]) -> Div f x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Div f x -> [Coyoneda f x]
forall (f :: * -> *) a. Div f a -> [Coyoneda f a]
unDiv
where
go :: Coyoneda f x -> g x -> g x
go (Coyoneda g :: x -> b
g x :: f b
x) = (x -> (x, x)) -> g x -> g x -> g x
forall (f :: * -> *) a b c.
Divisible f =>
(a -> (b, c)) -> f b -> f c -> f a
divide (\y :: x
y -> (x
y,x
y)) ((x -> b) -> g b -> g x
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap x -> b
g (f b -> g b
f ~> g
f f b
x))
instance Divisible f => Interpret Div f where
interpret :: (g ~> f) -> Div g ~> f
interpret = (g ~> f) -> Div g x -> f x
forall (f :: * -> *) (g :: * -> *).
Divisible g =>
(f ~> g) -> Div f ~> g
runDiv
newtype Div1 f a = Div1 { Div1 f a -> NonEmpty (Coyoneda f a)
unDiv1 :: NonEmpty (Coyoneda f a) }
deriving (b -> Div1 f b -> Div1 f a
(a -> b) -> Div1 f b -> Div1 f a
(forall a b. (a -> b) -> Div1 f b -> Div1 f a)
-> (forall b a. b -> Div1 f b -> Div1 f a)
-> Contravariant (Div1 f)
forall b a. b -> Div1 f b -> Div1 f a
forall a b. (a -> b) -> Div1 f b -> Div1 f a
forall (f :: * -> *).
(forall a b. (a -> b) -> f b -> f a)
-> (forall b a. b -> f b -> f a) -> Contravariant f
forall (f :: * -> *) b a. b -> Div1 f b -> Div1 f a
forall (f :: * -> *) a b. (a -> b) -> Div1 f b -> Div1 f a
>$ :: b -> Div1 f b -> Div1 f a
$c>$ :: forall (f :: * -> *) b a. b -> Div1 f b -> Div1 f a
contramap :: (a -> b) -> Div1 f b -> Div1 f a
$ccontramap :: forall (f :: * -> *) a b. (a -> b) -> Div1 f b -> Div1 f a
Contravariant, Contravariant (Div1 f)
Contravariant (Div1 f) =>
(forall a b c. (a -> (b, c)) -> Div1 f b -> Div1 f c -> Div1 f a)
-> Divise (Div1 f)
(a -> (b, c)) -> Div1 f b -> Div1 f c -> Div1 f a
forall a b c. (a -> (b, c)) -> Div1 f b -> Div1 f c -> Div1 f a
forall (f :: * -> *). Contravariant (Div1 f)
forall (f :: * -> *).
Contravariant f =>
(forall a b c. (a -> (b, c)) -> f b -> f c -> f a) -> Divise f
forall (f :: * -> *) a b c.
(a -> (b, c)) -> Div1 f b -> Div1 f c -> Div1 f a
divise :: (a -> (b, c)) -> Div1 f b -> Div1 f c -> Div1 f a
$cdivise :: forall (f :: * -> *) a b c.
(a -> (b, c)) -> Div1 f b -> Div1 f c -> Div1 f a
$cp1Divise :: forall (f :: * -> *). Contravariant (Div1 f)
Divise) via (NonEmptyF (Coyoneda f))
deriving ((f ~> g) -> Div1 f ~> Div1 g
(forall (f :: * -> *) (g :: * -> *). (f ~> g) -> Div1 f ~> Div1 g)
-> HFunctor Div1
forall k k (t :: (k -> *) -> k -> *).
(forall (f :: k -> *) (g :: k -> *). (f ~> g) -> t f ~> t g)
-> HFunctor t
forall (f :: * -> *) (g :: * -> *). (f ~> g) -> Div1 f ~> Div1 g
hmap :: (f ~> g) -> Div1 f ~> Div1 g
$chmap :: forall (f :: * -> *) (g :: * -> *). (f ~> g) -> Div1 f ~> Div1 g
HFunctor, HFunctor Div1
f x -> Div1 f x
HFunctor Div1 => (forall (f :: * -> *). f ~> Div1 f) -> Inject Div1
forall k (t :: (k -> *) -> k -> *).
HFunctor t =>
(forall (f :: k -> *). f ~> t f) -> Inject t
forall (f :: * -> *). f ~> Div1 f
inject :: f x -> Div1 f x
$cinject :: forall (f :: * -> *). f ~> Div1 f
$cp1Inject :: HFunctor Div1
Inject) via (CT.ComposeT NonEmptyF Coyoneda)
instance Invariant (Div1 f) where
invmap :: (a -> b) -> (b -> a) -> Div1 f a -> Div1 f b
invmap _ = (b -> a) -> Div1 f a -> Div1 f b
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap
instance Divise f => Interpret Div1 f where
interpret :: (g ~> f) -> Div1 g ~> f
interpret = (g ~> f) -> Div1 g x -> f x
forall (g :: * -> *) (f :: * -> *).
Divise g =>
(f ~> g) -> Div1 f ~> g
runDiv1
pattern Div1_ :: (a -> (b, c)) -> f b -> Div f c -> Div1 f a
pattern $bDiv1_ :: (a -> (b, c)) -> f b -> Div f c -> Div1 f a
$mDiv1_ :: forall r a (f :: * -> *).
Div1 f a
-> (forall b c. (a -> (b, c)) -> f b -> Div f c -> r)
-> (Void# -> r)
-> r
Div1_ f x xs <- (div1_->CD.Day x xs f)
where
Div1_ f :: a -> (b, c)
f x :: f b
x (Div xs :: [Coyoneda f c]
xs) = NonEmpty (Coyoneda f a) -> Div1 f a
forall (f :: * -> *) a. NonEmpty (Coyoneda f a) -> Div1 f a
Div1 (NonEmpty (Coyoneda f a) -> Div1 f a)
-> NonEmpty (Coyoneda f a) -> Div1 f a
forall a b. (a -> b) -> a -> b
$ (a -> b) -> f b -> Coyoneda f a
forall a b (f :: * -> *). (a -> b) -> f b -> Coyoneda f a
Coyoneda ((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)
f) f b
x Coyoneda f a -> [Coyoneda f a] -> NonEmpty (Coyoneda f a)
forall a. a -> [a] -> NonEmpty a
:| ((Coyoneda f c -> Coyoneda f a) -> [Coyoneda f c] -> [Coyoneda f a]
forall a b. (a -> b) -> [a] -> [b]
map ((Coyoneda f c -> Coyoneda f a)
-> [Coyoneda f c] -> [Coyoneda f a])
-> ((a -> c) -> Coyoneda f c -> Coyoneda f a)
-> (a -> c)
-> [Coyoneda f c]
-> [Coyoneda f a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> c) -> Coyoneda f c -> Coyoneda f a
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap) ((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)
f) [Coyoneda f c]
xs
{-# COMPLETE Div1_ #-}
div1_ :: Div1 f ~> CD.Day f (Div f)
div1_ :: Div1 f x -> Day f (Div f) x
div1_ (Div1 (Coyoneda g :: x -> b
g x :: f b
x :| xs :: [Coyoneda f x]
xs)) = f b -> Div f x -> (x -> (b, x)) -> Day f (Div f) x
forall (f :: * -> *) (g :: * -> *) a b c.
f b -> g c -> (a -> (b, c)) -> Day f g a
CD.Day f b
x ([Coyoneda f x] -> Div f x
forall (f :: * -> *) a. [Coyoneda f a] -> Div f a
Div [Coyoneda f x]
xs) (\y :: x
y -> (x -> b
g x
y, x
y))
toDiv :: Div1 f ~> Div f
toDiv :: Div1 f x -> Div f x
toDiv = [Coyoneda f x] -> Div f x
forall (f :: * -> *) a. [Coyoneda f a] -> Div f a
Div ([Coyoneda f x] -> Div f x)
-> (Div1 f x -> [Coyoneda f x]) -> Div1 f x -> Div f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmpty (Coyoneda f x) -> [Coyoneda f x]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (NonEmpty (Coyoneda f x) -> [Coyoneda f x])
-> (Div1 f x -> NonEmpty (Coyoneda f x))
-> Div1 f x
-> [Coyoneda f x]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Div1 f x -> NonEmpty (Coyoneda f x)
forall (f :: * -> *) a. Div1 f a -> NonEmpty (Coyoneda f a)
unDiv1
hoistDiv1 :: (f ~> g) -> Div1 f ~> Div1 g
hoistDiv1 :: (f ~> g) -> Div1 f ~> Div1 g
hoistDiv1 = (f ~> g) -> Div1 f x -> Div1 g x
forall k k (t :: (k -> *) -> k -> *) (f :: k -> *) (g :: k -> *).
HFunctor t =>
(f ~> g) -> t f ~> t g
hmap
liftDiv1 :: f ~> Div1 f
liftDiv1 :: f x -> Div1 f x
liftDiv1 = f x -> Div1 f x
forall k (t :: (k -> *) -> k -> *) (f :: k -> *).
Inject t =>
f ~> t f
inject
runDiv1 :: Divise g => (f ~> g) -> Div1 f ~> g
runDiv1 :: (f ~> g) -> Div1 f ~> g
runDiv1 f :: f ~> g
f = (g x -> g x -> g x) -> NonEmpty (g x) -> g x
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ((x -> (x, x)) -> g x -> g x -> g x
forall (f :: * -> *) a b c.
Divise f =>
(a -> (b, c)) -> f b -> f c -> f a
divise (\y :: x
y->(x
y,x
y))) (NonEmpty (g x) -> g x)
-> (Div1 f x -> NonEmpty (g x)) -> Div1 f x -> g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Coyoneda f x -> g x) -> NonEmpty (Coyoneda f x) -> NonEmpty (g x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Coyoneda f x -> g x
go (NonEmpty (Coyoneda f x) -> NonEmpty (g x))
-> (Div1 f x -> NonEmpty (Coyoneda f x))
-> Div1 f x
-> NonEmpty (g x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Div1 f x -> NonEmpty (Coyoneda f x)
forall (f :: * -> *) a. Div1 f a -> NonEmpty (Coyoneda f a)
unDiv1
where
go :: Coyoneda f x -> g x
go (Coyoneda g :: x -> b
g x :: f b
x) = (x -> b) -> g b -> g x
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap x -> b
g (f b -> g b
f ~> g
f f b
x)
div1NonEmptyF :: Contravariant f => Div1 f ~> NonEmptyF f
div1NonEmptyF :: Div1 f ~> NonEmptyF f
div1NonEmptyF = NonEmpty (f x) -> NonEmptyF f x
forall k (f :: k -> *) (a :: k). NonEmpty (f a) -> NonEmptyF f a
NonEmptyF (NonEmpty (f x) -> NonEmptyF f x)
-> (Div1 f x -> NonEmpty (f x)) -> Div1 f x -> NonEmptyF f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Coyoneda f x -> f x) -> NonEmpty (Coyoneda f x) -> NonEmpty (f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Coyoneda f x -> f x
forall (f :: * -> *) a. Contravariant f => Coyoneda f a -> f a
lowerCoyoneda (NonEmpty (Coyoneda f x) -> NonEmpty (f x))
-> (Div1 f x -> NonEmpty (Coyoneda f x))
-> Div1 f x
-> NonEmpty (f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Div1 f x -> NonEmpty (Coyoneda f x)
forall (f :: * -> *) a. Div1 f a -> NonEmpty (Coyoneda f a)
unDiv1
nonEmptyFDiv1 :: NonEmptyF f ~> Div1 f
nonEmptyFDiv1 :: NonEmptyF f x -> Div1 f x
nonEmptyFDiv1 = NonEmpty (Coyoneda f x) -> Div1 f x
forall (f :: * -> *) a. NonEmpty (Coyoneda f a) -> Div1 f a
Div1 (NonEmpty (Coyoneda f x) -> Div1 f x)
-> (NonEmptyF f x -> NonEmpty (Coyoneda f x))
-> NonEmptyF f x
-> Div1 f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f x -> Coyoneda f x) -> NonEmpty (f x) -> NonEmpty (Coyoneda f x)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f x -> Coyoneda f x
forall (f :: * -> *) a. f a -> Coyoneda f a
liftCoyoneda (NonEmpty (f x) -> NonEmpty (Coyoneda f x))
-> (NonEmptyF f x -> NonEmpty (f x))
-> NonEmptyF f x
-> NonEmpty (Coyoneda f x)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NonEmptyF f x -> NonEmpty (f x)
forall k (f :: k -> *) (a :: k). NonEmptyF f a -> NonEmpty (f a)
runNonEmptyF
data Dec :: (Type -> Type) -> Type -> Type where
Lose :: (a -> Void) -> Dec f a
Choose :: (a -> Either b c) -> f b -> Dec f c -> Dec f a
instance Contravariant (Dec f) where
contramap :: (a -> b) -> Dec f b -> Dec f a
contramap f :: a -> b
f = \case
Lose g :: b -> Void
g -> (a -> Void) -> Dec f a
forall a (f :: * -> *). (a -> Void) -> Dec f a
Lose (b -> Void
g (b -> Void) -> (a -> b) -> a -> Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f)
Choose g :: b -> Either b c
g x :: f b
x xs :: Dec f c
xs -> (a -> Either b c) -> f b -> Dec f c -> Dec f a
forall a b c (f :: * -> *).
(a -> Either b c) -> f b -> Dec f c -> Dec f a
Choose (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) f b
x Dec f c
xs
instance Invariant (Dec f) where
invmap :: (a -> b) -> (b -> a) -> Dec f a -> Dec f b
invmap _ = (b -> a) -> Dec f a -> Dec f b
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap
instance Decide (Dec f) where
decide :: (a -> Either b c) -> Dec f b -> Dec f c -> Dec f a
decide f :: a -> Either b c
f = \case
Lose g :: b -> Void
g -> (a -> c) -> Dec f c -> Dec f a
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
. b -> Void
g) c -> c
forall a. a -> a
id (Either b c -> c) -> (a -> Either b c) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either b c
f)
Choose g :: b -> Either b c
g x :: f b
x xs :: Dec f c
xs -> (a -> Either b (Either c c))
-> f b -> Dec f (Either c c) -> Dec f a
forall a b c (f :: * -> *).
(a -> Either b c) -> f b -> Dec f c -> Dec f a
Choose (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)
assoc (Either (Either b c) c -> Either b (Either c c))
-> (a -> Either (Either b c) c) -> a -> 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
g (Either b c -> Either (Either b c) c)
-> (a -> Either b c) -> a -> Either (Either b c) c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either b c
f) f b
x
(Dec f (Either c c) -> Dec f a)
-> (Dec f c -> Dec f (Either c c)) -> Dec f c -> Dec f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either c c -> Either c c)
-> Dec f c -> Dec f c -> Dec f (Either c c)
forall (f :: * -> *) a b c.
Decide f =>
(a -> Either b c) -> f b -> f c -> f a
decide Either c c -> Either c c
forall a. a -> a
id Dec f c
xs
instance Conclude (Dec f) where
conclude :: (a -> Void) -> Dec f a
conclude = (a -> Void) -> Dec f a
forall a (f :: * -> *). (a -> Void) -> Dec f a
Lose
instance HFunctor Dec where
hmap :: (f ~> g) -> Dec f ~> Dec g
hmap = (f ~> g) -> Dec f x -> Dec g x
forall (f :: * -> *) (g :: * -> *). (f ~> g) -> Dec f ~> Dec g
hoistDec
instance Inject Dec where
inject :: f x -> Dec f x
inject = f x -> Dec f x
forall (f :: * -> *). f ~> Dec f
liftDec
instance Conclude f => Interpret Dec f where
interpret :: (g ~> f) -> Dec g ~> f
interpret = (g ~> f) -> Dec g x -> f x
forall (f :: * -> *) (g :: * -> *).
Conclude g =>
(f ~> g) -> Dec f ~> g
runDec
hoistDec :: forall f g. (f ~> g) -> Dec f ~> Dec g
hoistDec :: (f ~> g) -> Dec f ~> Dec g
hoistDec f :: f ~> g
f = Dec f x -> Dec g x
Dec f ~> Dec g
go
where
go :: Dec f ~> Dec g
go :: Dec f x -> Dec g x
go = \case
Lose g :: x -> Void
g -> (x -> Void) -> Dec g x
forall a (f :: * -> *). (a -> Void) -> Dec f a
Lose x -> Void
g
Choose g :: x -> Either b c
g x :: f b
x xs :: Dec f c
xs -> (x -> Either b c) -> g b -> Dec g c -> Dec g x
forall a b c (f :: * -> *).
(a -> Either b c) -> f b -> Dec f c -> Dec f a
Choose x -> Either b c
g (f b -> g b
f ~> g
f f b
x) (Dec f c -> Dec g c
Dec f ~> Dec g
go Dec f c
xs)
liftDec :: f ~> Dec f
liftDec :: f x -> Dec f x
liftDec x :: f x
x = (x -> Either x Void) -> f x -> Dec f Void -> Dec f x
forall a b c (f :: * -> *).
(a -> Either b c) -> f b -> Dec f c -> Dec f a
Choose x -> Either x Void
forall a b. a -> Either a b
Left f x
x ((Void -> Void) -> Dec f Void
forall a (f :: * -> *). (a -> Void) -> Dec f a
Lose Void -> Void
forall a. a -> a
id)
runDec :: forall f g. Conclude g => (f ~> g) -> Dec f ~> g
runDec :: (f ~> g) -> Dec f ~> g
runDec f :: f ~> g
f = Dec f x -> g x
Dec f ~> g
go
where
go :: Dec f ~> g
go :: Dec f x -> g x
go = \case
Lose g :: x -> Void
g -> (x -> Void) -> g x
forall (f :: * -> *) a. Conclude f => (a -> Void) -> f a
conclude x -> Void
g
Choose g :: x -> Either b c
g x :: f b
x xs :: Dec f c
xs -> (x -> Either b c) -> g b -> g c -> g x
forall (f :: * -> *) a b c.
Decide f =>
(a -> Either b c) -> f b -> f c -> f a
decide x -> Either b c
g (f b -> g b
f ~> g
f f b
x) (Dec f c -> g c
Dec f ~> g
go Dec f c
xs)
data Dec1 :: (Type -> Type) -> Type -> Type where
Dec1 :: (a -> Either b c) -> f b -> Dec f c -> Dec1 f a
toDec :: Dec1 f a -> Dec f a
toDec :: Dec1 f a -> Dec f a
toDec (Dec1 f :: a -> Either b c
f x :: f b
x xs :: Dec f c
xs) = (a -> Either b c) -> f b -> Dec f c -> Dec f a
forall a b c (f :: * -> *).
(a -> Either b c) -> f b -> Dec f c -> Dec f a
Choose a -> Either b c
f f b
x Dec f c
xs
instance Contravariant (Dec1 f) where
contramap :: (a -> b) -> Dec1 f b -> Dec1 f a
contramap f :: a -> b
f (Dec1 g :: b -> Either b c
g x :: f b
x xs :: Dec f c
xs) = (a -> Either b c) -> f b -> Dec f c -> Dec1 f a
forall a b c (f :: * -> *).
(a -> Either b c) -> f b -> Dec f c -> Dec1 f a
Dec1 (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) f b
x Dec f c
xs
instance Invariant (Dec1 f) where
invmap :: (a -> b) -> (b -> a) -> Dec1 f a -> Dec1 f b
invmap _ = (b -> a) -> Dec1 f a -> Dec1 f b
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap
instance Decide (Dec1 f) where
decide :: (a -> Either b c) -> Dec1 f b -> Dec1 f c -> Dec1 f a
decide f :: a -> Either b c
f (Dec1 g :: b -> Either b c
g x :: f b
x xs :: Dec f c
xs) = (a -> Either b (Either c c))
-> f b -> Dec f (Either c c) -> Dec1 f a
forall a b c (f :: * -> *).
(a -> Either b c) -> f b -> Dec f c -> Dec1 f a
Dec1 (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)
assoc (Either (Either b c) c -> Either b (Either c c))
-> (a -> Either (Either b c) c) -> a -> 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
g (Either b c -> Either (Either b c) c)
-> (a -> Either b c) -> a -> Either (Either b c) c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Either b c
f) f b
x
(Dec f (Either c c) -> Dec1 f a)
-> (Dec1 f c -> Dec f (Either c c)) -> Dec1 f c -> Dec1 f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Either c c -> Either c c)
-> Dec f c -> Dec f c -> Dec f (Either c c)
forall (f :: * -> *) a b c.
Decide f =>
(a -> Either b c) -> f b -> f c -> f a
decide Either c c -> Either c c
forall a. a -> a
id Dec f c
xs
(Dec f c -> Dec f (Either c c))
-> (Dec1 f c -> Dec f c) -> Dec1 f c -> Dec f (Either c c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dec1 f c -> Dec f c
forall (f :: * -> *) a. Dec1 f a -> Dec f a
toDec
instance HFunctor Dec1 where
hmap :: (f ~> g) -> Dec1 f ~> Dec1 g
hmap = (f ~> g) -> Dec1 f x -> Dec1 g x
forall (f :: * -> *) (g :: * -> *). (f ~> g) -> Dec1 f ~> Dec1 g
hoistDec1
instance Inject Dec1 where
inject :: f x -> Dec1 f x
inject = f x -> Dec1 f x
forall (f :: * -> *). f ~> Dec1 f
liftDec1
instance Decide f => Interpret Dec1 f where
interpret :: (g ~> f) -> Dec1 g ~> f
interpret = (g ~> f) -> Dec1 g x -> f x
forall (g :: * -> *) (f :: * -> *).
Decide g =>
(f ~> g) -> Dec1 f ~> g
runDec1
hoistDec1 :: forall f g. (f ~> g) -> Dec1 f ~> Dec1 g
hoistDec1 :: (f ~> g) -> Dec1 f ~> Dec1 g
hoistDec1 f :: f ~> g
f (Dec1 g :: x -> Either b c
g x :: f b
x xs :: Dec f c
xs) = (x -> Either b c) -> g b -> Dec g c -> Dec1 g x
forall a b c (f :: * -> *).
(a -> Either b c) -> f b -> Dec f c -> Dec1 f a
Dec1 x -> Either b c
g (f b -> g b
f ~> g
f f b
x) ((f ~> g) -> Dec f c -> Dec g c
forall (f :: * -> *) (g :: * -> *). (f ~> g) -> Dec f ~> Dec g
hoistDec f ~> g
f Dec f c
xs)
liftDec1 :: f ~> Dec1 f
liftDec1 :: f x -> Dec1 f x
liftDec1 x :: f x
x = (x -> Either x Void) -> f x -> Dec f Void -> Dec1 f x
forall a b c (f :: * -> *).
(a -> Either b c) -> f b -> Dec f c -> Dec1 f a
Dec1 x -> Either x Void
forall a b. a -> Either a b
Left f x
x ((Void -> Void) -> Dec f Void
forall a (f :: * -> *). (a -> Void) -> Dec f a
Lose Void -> Void
forall a. a -> a
id)
runDec1 :: Decide g => (f ~> g) -> Dec1 f ~> g
runDec1 :: (f ~> g) -> Dec1 f ~> g
runDec1 f :: f ~> g
f (Dec1 g :: x -> Either b c
g x :: f b
x xs :: Dec f c
xs) = (f ~> g) -> (x -> Either b c) -> f b -> Dec f c -> g x
forall (f :: * -> *) (g :: * -> *) a b c.
Decide g =>
(f ~> g) -> (a -> Either b c) -> f b -> Dec f c -> g a
runDec1_ f ~> g
f x -> Either b c
g f b
x Dec f c
xs
runDec1_
:: forall f g a b c. Decide g
=> (f ~> g)
-> (a -> Either b c)
-> f b
-> Dec f c
-> g a
runDec1_ :: (f ~> g) -> (a -> Either b c) -> f b -> Dec f c -> g a
runDec1_ f :: f ~> g
f = (a -> Either b c) -> f b -> Dec f c -> g a
forall x y z. (x -> Either y z) -> f y -> Dec f z -> g x
go
where
go :: (x -> Either y z) -> f y -> Dec f z -> g x
go :: (x -> Either y z) -> f y -> Dec f z -> g x
go g :: x -> Either y z
g x :: f y
x = \case
Lose h :: z -> Void
h -> (x -> y) -> g y -> g x
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap ((y -> y) -> (z -> y) -> Either y z -> y
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either y -> y
forall a. a -> a
id (Void -> y
forall a. Void -> a
absurd (Void -> y) -> (z -> Void) -> z -> y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. z -> Void
h) (Either y z -> y) -> (x -> Either y z) -> x -> y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> Either y z
g) (f y -> g y
f ~> g
f f y
x)
Choose h :: z -> Either b c
h y :: f b
y ys :: Dec f c
ys -> (x -> Either y z) -> g y -> g z -> g x
forall (f :: * -> *) a b c.
Decide f =>
(a -> Either b c) -> f b -> f c -> f a
decide x -> Either y z
g (f y -> g y
f ~> g
f f y
x) ((z -> Either b c) -> f b -> Dec f c -> g z
forall x y z. (x -> Either y z) -> f y -> Dec f z -> g x
go z -> Either b c
h f b
y Dec f c
ys)