module Data.Functor.Contravariant.Divisible.Free (
Div(..)
, hoistDiv, liftDiv, runDiv
, divListF, listFDiv
, 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.Functor.Contravariant
import Data.Functor.Contravariant.Conclude
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
import Data.List.NonEmpty (NonEmpty(..))
import Data.Void
data Div :: (Type -> Type) -> Type -> Type where
Conquer :: Div f a
Divide :: (a -> (b, c)) -> f b -> Div f c -> Div f a
instance Contravariant (Div f) where
contramap :: forall a b. (a -> b) -> Div f b -> Div f a
contramap :: (a -> b) -> Div f b -> Div f a
contramap f :: a -> b
f = \case
Conquer -> Div f a
forall (f :: * -> *) a. Div f a
Conquer
Divide g :: b -> (b, c)
g x :: f b
x xs :: Div f c
xs -> (a -> (b, c)) -> f b -> Div f c -> Div f a
forall a b c (f :: * -> *).
(a -> (b, c)) -> f b -> Div f c -> Div f a
Divide (b -> (b, c)
g (b -> (b, c)) -> (a -> b) -> a -> (b, c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) f b
x Div f c
xs
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
instance Divise (Div f) where
divise :: (a -> (b, c)) -> Div f b -> Div f c -> Div f a
divise f :: a -> (b, c)
f = \case
Conquer -> (a -> c) -> Div f c -> Div 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)
Divide g :: b -> (b, c)
g x :: f b
x xs :: Div f c
xs -> (a -> (b, (c, c))) -> f b -> Div f (c, c) -> Div f a
forall a b c (f :: * -> *).
(a -> (b, c)) -> f b -> Div f c -> Div f a
Divide (((b, c), c) -> (b, (c, c))
forall (p :: * -> * -> *) a b c.
Assoc p =>
p (p a b) c -> p a (p b c)
assoc (((b, c), c) -> (b, (c, c)))
-> (a -> ((b, c), c)) -> a -> (b, (c, c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> (b, c)) -> (b, c) -> ((b, c), c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first b -> (b, c)
g ((b, c) -> ((b, c), c)) -> (a -> (b, c)) -> a -> ((b, c), c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
f) f b
x
(Div f (c, c) -> Div f a)
-> (Div f c -> Div f (c, c)) -> Div f c -> Div f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((c, c) -> (c, c)) -> Div f c -> Div f c -> Div f (c, c)
forall (f :: * -> *) a b c.
Divise f =>
(a -> (b, c)) -> f b -> f c -> f a
divise (c, c) -> (c, c)
forall a. a -> a
id Div f c
xs
instance Divisible (Div f) where
conquer :: Div f a
conquer = Div f a
forall (f :: * -> *) a. Div f a
Conquer
divide :: (a -> (b, c)) -> Div f b -> Div f c -> Div f a
divide = (a -> (b, c)) -> Div f b -> Div f c -> Div f a
forall (f :: * -> *) a b c.
Divise f =>
(a -> (b, c)) -> f b -> f c -> f a
divise
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
. (Div f x -> Maybe (f x, Div f x)) -> Div f x -> [f x]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr Div f x -> Maybe (f x, Div f x)
forall b. Div f b -> Maybe (f b, Div f b)
go
where
go :: Div f b -> Maybe (f b, Div f b)
go = \case
Conquer -> Maybe (f b, Div f b)
forall a. Maybe a
Nothing
Divide f :: b -> (b, c)
f x :: f b
x xs :: Div f c
xs -> (f b, Div f b) -> Maybe (f b, Div f b)
forall a. a -> Maybe a
Just ( (b -> b) -> f b -> f b
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap ((b, c) -> b
forall a b. (a, b) -> a
fst ((b, c) -> b) -> (b -> (b, c)) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> (b, c)
f) f b
x
, (b -> c) -> Div f c -> Div f b
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) -> (b -> (b, c)) -> b -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b -> (b, c)
f) Div f c
xs
)
listFDiv :: ListF f ~> Div f
listFDiv :: ListF f x -> Div f x
listFDiv = (f x -> Div f x -> Div f x) -> Div f x -> [f x] -> Div f x
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((x -> (x, x)) -> f x -> Div f x -> Div f x
forall a b c (f :: * -> *).
(a -> (b, c)) -> f b -> Div f c -> Div f a
Divide (\y :: x
y -> (x
y,x
y))) Div f x
forall (f :: * -> *) a. Div f a
Conquer ([f x] -> Div f x) -> (ListF f x -> [f x]) -> ListF f x -> Div 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 :: f ~> g
f = Div f x -> Div g x
Div f ~> Div g
go
where
go :: Div f ~> Div g
go :: Div f x -> Div g x
go = \case
Conquer -> Div g x
forall (f :: * -> *) a. Div f a
Conquer
Divide g :: x -> (b, c)
g x :: f b
x xs :: Div f c
xs -> (x -> (b, c)) -> g b -> Div g c -> Div g x
forall a b c (f :: * -> *).
(a -> (b, c)) -> f b -> Div f c -> Div f a
Divide x -> (b, c)
g (f b -> g b
f ~> g
f f b
x) (Div f c -> Div g c
Div f ~> Div g
go Div f c
xs)
liftDiv :: f ~> Div f
liftDiv :: f x -> Div f x
liftDiv x :: f x
x = (x -> (x, ())) -> f x -> Div f () -> Div f x
forall a b c (f :: * -> *).
(a -> (b, c)) -> f b -> Div f c -> Div f a
Divide (,()) f x
x Div f ()
forall (f :: * -> *) a. Div f a
Conquer
runDiv :: forall f g. Divisible g => (f ~> g) -> Div f ~> g
runDiv :: (f ~> g) -> Div f ~> g
runDiv f :: f ~> g
f = Div f x -> g x
Div f ~> g
go
where
go :: Div f ~> g
go :: Div f x -> g x
go = \case
Conquer -> g x
forall (f :: * -> *) a. Divisible f => f a
conquer
Divide g :: x -> (b, c)
g x :: f b
x xs :: Div f c
xs -> (x -> (b, c)) -> g b -> g c -> g x
forall (f :: * -> *) a b c.
Divisible f =>
(a -> (b, c)) -> f b -> f c -> f a
divide x -> (b, c)
g (f b -> g b
f ~> g
f f b
x) (Div f c -> g c
Div f ~> g
go Div f c
xs)
instance HFunctor Div where
hmap :: (f ~> g) -> Div f ~> Div g
hmap = (f ~> g) -> Div f x -> Div g x
forall (f :: * -> *) (g :: * -> *). (f ~> g) -> Div f ~> Div g
hoistDiv
instance Inject Div where
inject :: f x -> Div f x
inject = f x -> Div f x
forall (f :: * -> *). f ~> Div f
liftDiv
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
data Div1 :: (Type -> Type) -> Type -> Type where
Div1 :: (a -> (b, c)) -> f b -> Div f c -> Div1 f a
instance Contravariant (Div1 f) where
contramap :: (a -> b) -> Div1 f b -> Div1 f a
contramap f :: a -> b
f (Div1 g :: b -> (b, c)
g x :: f b
x xs :: Div f c
xs) = (a -> (b, c)) -> f b -> Div f c -> Div1 f a
forall a b c (f :: * -> *).
(a -> (b, c)) -> f b -> Div f c -> Div1 f a
Div1 (b -> (b, c)
g (b -> (b, c)) -> (a -> b) -> a -> (b, c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f) f b
x Div f c
xs
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 (Div1 f) where
divise :: (a -> (b, c)) -> Div1 f b -> Div1 f c -> Div1 f a
divise f :: a -> (b, c)
f (Div1 g :: b -> (b, c)
g x :: f b
x xs :: Div f c
xs) = (a -> (b, (c, c))) -> f b -> Div f (c, c) -> Div1 f a
forall a b c (f :: * -> *).
(a -> (b, c)) -> f b -> Div f c -> Div1 f a
Div1 (((b, c), c) -> (b, (c, c))
forall (p :: * -> * -> *) a b c.
Assoc p =>
p (p a b) c -> p a (p b c)
assoc (((b, c), c) -> (b, (c, c)))
-> (a -> ((b, c), c)) -> a -> (b, (c, c))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> (b, c)) -> (b, c) -> ((b, c), c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first b -> (b, c)
g ((b, c) -> ((b, c), c)) -> (a -> (b, c)) -> a -> ((b, c), c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> (b, c)
f) f b
x
(Div f (c, c) -> Div1 f a)
-> (Div1 f c -> Div f (c, c)) -> Div1 f c -> Div1 f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((c, c) -> (c, c)) -> Div f c -> Div f c -> Div f (c, c)
forall (f :: * -> *) a b c.
Divise f =>
(a -> (b, c)) -> f b -> f c -> f a
divise (c, c) -> (c, c)
forall a. a -> a
id Div f c
xs
(Div f c -> Div f (c, c))
-> (Div1 f c -> Div f c) -> Div1 f c -> Div f (c, c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Div1 f c -> Div f c
forall (f :: * -> *) a. Div1 f a -> Div f a
toDiv
instance HFunctor Div1 where
hmap :: (f ~> g) -> Div1 f ~> Div1 g
hmap = (f ~> g) -> Div1 f x -> Div1 g x
forall (f :: * -> *) (g :: * -> *). (f ~> g) -> Div1 f ~> Div1 g
hoistDiv1
instance Inject Div1 where
inject :: f x -> Div1 f x
inject = f x -> Div1 f x
forall (f :: * -> *). f ~> Div1 f
liftDiv1
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
toDiv :: Div1 f a -> Div f a
toDiv :: Div1 f a -> Div f a
toDiv (Div1 f :: a -> (b, c)
f x :: f b
x xs :: Div f c
xs) = (a -> (b, c)) -> f b -> Div f c -> Div f a
forall a b c (f :: * -> *).
(a -> (b, c)) -> f b -> Div f c -> Div f a
Divide a -> (b, c)
f f b
x Div f c
xs
hoistDiv1 :: (f ~> g) -> Div1 f ~> Div1 g
hoistDiv1 :: (f ~> g) -> Div1 f ~> Div1 g
hoistDiv1 f :: f ~> g
f (Div1 g :: x -> (b, c)
g x :: f b
x xs :: Div f c
xs) = (x -> (b, c)) -> g b -> Div g c -> Div1 g x
forall a b c (f :: * -> *).
(a -> (b, c)) -> f b -> Div f c -> Div1 f a
Div1 x -> (b, c)
g (f b -> g b
f ~> g
f f b
x) ((f ~> g) -> Div f c -> Div g c
forall (f :: * -> *) (g :: * -> *). (f ~> g) -> Div f ~> Div g
hoistDiv f ~> g
f Div f c
xs)
liftDiv1 :: f ~> Div1 f
liftDiv1 :: f x -> Div1 f x
liftDiv1 f :: f x
f = (x -> (x, ())) -> f x -> Div f () -> Div1 f x
forall a b c (f :: * -> *).
(a -> (b, c)) -> f b -> Div f c -> Div1 f a
Div1 (,()) f x
f Div f ()
forall (f :: * -> *) a. Div f a
Conquer
runDiv1 :: Divise g => (f ~> g) -> Div1 f ~> g
runDiv1 :: (f ~> g) -> Div1 f ~> g
runDiv1 f :: f ~> g
f (Div1 g :: x -> (b, c)
g x :: f b
x xs :: Div f c
xs) = (f ~> g) -> (x -> (b, c)) -> f b -> Div f c -> g x
forall (f :: * -> *) (g :: * -> *) a b c.
Divise g =>
(f ~> g) -> (a -> (b, c)) -> f b -> Div f c -> g a
runDiv1_ f ~> g
f x -> (b, c)
g f b
x Div f c
xs
runDiv1_
:: forall f g a b c. Divise g
=> (f ~> g)
-> (a -> (b, c))
-> f b
-> Div f c
-> g a
runDiv1_ :: (f ~> g) -> (a -> (b, c)) -> f b -> Div f c -> g a
runDiv1_ f :: f ~> g
f = (a -> (b, c)) -> f b -> Div f c -> g a
forall x y z. (x -> (y, z)) -> f y -> Div f z -> g x
go
where
go :: (x -> (y, z)) -> f y -> Div f z -> g x
go :: (x -> (y, z)) -> f y -> Div f z -> g x
go g :: x -> (y, z)
g x :: f y
x = \case
Conquer -> (x -> y) -> g y -> g x
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap ((y, z) -> y
forall a b. (a, b) -> a
fst ((y, z) -> y) -> (x -> (y, z)) -> x -> y
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (y, z)
g) (f y -> g y
f ~> g
f f y
x)
Divide h :: z -> (b, c)
h y :: f b
y ys :: Div f c
ys -> (x -> (y, z)) -> g y -> g z -> g x
forall (f :: * -> *) a b c.
Divise f =>
(a -> (b, c)) -> f b -> f c -> f a
divise x -> (y, z)
g (f y -> g y
f ~> g
f f y
x) ((z -> (b, c)) -> f b -> Div f c -> g z
forall x y z. (x -> (y, z)) -> f y -> Div f z -> g x
go z -> (b, c)
h f b
y Div f c
ys)
div1NonEmptyF :: Contravariant f => Div1 f ~> NonEmptyF f
div1NonEmptyF :: Div1 f ~> NonEmptyF f
div1NonEmptyF (Div1 f :: x -> (b, c)
f x :: f b
x xs :: Div f c
xs) = 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)
-> NonEmpty (f x) -> NonEmptyF f x
forall a b. (a -> b) -> a -> b
$
(x -> b) -> f b -> f x
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap ((b, c) -> b
forall a b. (a, b) -> a
fst ((b, c) -> b) -> (x -> (b, c)) -> x -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
f) f b
x
f x -> [f x] -> NonEmpty (f x)
forall a. a -> [a] -> NonEmpty a
:| ListF f x -> [f x]
forall k (f :: k -> *) (a :: k). ListF f a -> [f a]
runListF (Div f x -> ListF f x
forall (f :: * -> *). Contravariant f => Div f ~> ListF f
divListF ((x -> c) -> Div f c -> Div f x
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) -> (x -> (b, c)) -> x -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. x -> (b, c)
f) Div f c
xs))
nonEmptyFDiv1 :: NonEmptyF f ~> Div1 f
nonEmptyFDiv1 :: NonEmptyF f x -> Div1 f x
nonEmptyFDiv1 (NonEmptyF (x :: f x
x :| xs :: [f x]
xs)) =
(x -> (x, x)) -> f x -> Div f x -> Div1 f x
forall a b c (f :: * -> *).
(a -> (b, c)) -> f b -> Div f c -> Div1 f a
Div1 (\y :: x
y -> (x
y,x
y)) f x
x (ListF f x -> Div f x
forall (f :: * -> *). ListF f ~> Div f
listFDiv ([f x] -> ListF f x
forall k (f :: k -> *) (a :: k). [f a] -> ListF f a
ListF [f x]
xs))
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)