-- |
-- Module      : Data.Functor.Contravariant.Divisible.Free
-- Copyright   : (c) Justin Le 2019
-- License     : BSD3
--
-- Maintainer  : justin@jle.im
-- Stability   : experimental
-- Portability : non-portable
--
-- Provides free structures for the various typeclasses of the 'Divisible'
-- hierarchy.
--
-- @since 0.3.0.0
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

-- | The free 'Divisible'.  Used to sequence multiple contravariant
-- consumers, splitting out the input across all consumers.
--
-- Note that @'Div' f@ is essentially @'ListF'
-- ('Data.Functor.Contravariant.Coyoneda' f)@, or just @'ListF' f@ in the
-- case that @f@ is already contravariant.  However, this is left in here
-- because it can be more convenient to use if you are working with an
-- intermediate @f@ that isn't 'Contravariant'.
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

-- | 'Div' is isomorphic to 'ListF' for contravariant @f@.  This witnesses
-- one way of that isomorphism.
--
-- Be aware that this is essentially O(n^2).
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
                            )

-- | 'Div' is isomorphic to 'ListF' for contravariant @f@.  This witnesses
-- one way of that isomorphism.
--
-- This direction is O(n), unlike 'divListF'.
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

-- | Map over the undering context in a 'Div'.
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)

-- | Inject a single action in @f@ into a @'Div' f@.
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

-- | Interpret a 'Div' into a context @g@, provided @g@ is 'Divisible'.
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

-- | The free 'Divise': a non-empty version of 'Div'.
--
-- Note that @'Div1' f@ is essentially @'NonEmptyF'
-- ('Data.Functor.Contravariant.Coyoneda' f)@, or just @'NonEmptyF' f@ in the
-- case that @f@ is already contravariant.  However, it can be more
-- convenient to use if you are working with an intermediate @f@ that isn't
-- 'Contravariant'.
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

-- | A 'Div1' is a "non-empty" 'Div'; this function "forgets" the non-empty
-- property and turns it back into a normal 'Div'.
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

-- | Map over the undering context in a 'Div1'.
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)

-- | Inject a single action in @f@ into a @'Div' f@.
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

-- | Interpret a 'Div1' into a context @g@, provided @g@ is 'Divise'.
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)

-- | 'Div1' is isomorphic to 'NonEmptyF' for contravariant @f@.  This
-- witnesses one way of that isomorphism.
--
-- Be aware that this is essentially O(n^2).
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))

-- | 'Div1' is isomorphic to 'NonEmptyF' for contravariant @f@.  This
-- witnesses one way of that isomorphism.
--
-- This direction is O(n), unlike 'div1NonEmptyF'.
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))

-- | The free 'Decide'.  Used to aggregate multiple possible consumers,
-- directing the input into an appropriate consumer.
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

-- | Map over the undering context in a 'Dec'.
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)

-- | Inject a single action in @f@ into a @'Dec' f@.
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)

-- | Interpret a 'Dec' into a context @g@, provided @g@ is 'Conclude'.
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)


-- | The free 'Decide': a non-empty version of 'Dec'.
data Dec1 :: (Type -> Type) -> Type -> Type where
    Dec1 :: (a -> Either b c) -> f b -> Dec f c -> Dec1 f a

-- | A 'Dec1' is a "non-empty" 'Dec'; this function "forgets" the non-empty
-- property and turns it back into a normal 'Dec'.
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

-- | Map over the undering context in a 'Dec1'.
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)

-- | Inject a single action in @f@ into a @'Dec1' f@.
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)

-- | Interpret a 'Dec1' into a context @g@, provided @g@ is 'Decide'.
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)