{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTSyntax #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE DerivingVia #-}

-- | Free alternative (with /left zero/ + /left catch/).
--
-- 'Alternative' laws were not set to one, clear definition,
-- but there are two major ones.
--
-- For an instance of @(Alternative f)@, both laws have these in common.
--
-- - Inherited laws from 'Applicative'
-- - @(f a, 'empty', '<|>')@ forms monoid for any type @a@.
-- - /Left zero/ law: @'empty' '<*>' x === 'empty'@.
--
-- Candidate #1 of the Alternative law have /Left distribution/ law.
--
-- @
-- -- Left distribution
-- (x '<|>' y) '<*>' z === (x \<*\> z) \<|\> (y \<*\> z)
-- @
--
-- Another candidate #2 have /Left catch/ law instead.
--
-- @
-- -- Left catch
-- 'pure' x '<|>' y === pure x
-- @
--
-- Reference Typeclassopedia <https://wiki.haskell.org/Typeclassopedia#Laws_6>
-- for more about these laws.
--
-- The \"free alternative\" construction for the alternative #1
-- (with /Left distribution/) is known and implemented.
--
-- - https://people.cs.kuleuven.be/~tom.schrijvers/Research/talks/ppdp2015.pdf
-- - <https://hackage.haskell.org/package/free-5.2/docs/Control-Alternative-Free.html>
--
-- This module provides the free alternative #2.
module Control.Alternative.Free.LZLC(
  -- * Type definitions
  Free(.., SumZOf, ApZOf),

  Summand(..), viewSummand,
  Factor(..), viewFactor,

  viewSumZ, reviewSumZ,
  viewApZ, reviewApZ,

  -- * Universal properties
  hoistFree, liftFree, foldFree,

  -- * Auxiliary definitions
  Trivial(..),
  SumZ,
  NontrivialSumZ(..),
  NontrivialApZ(..)
) where

import Control.Applicative (Alternative (..))
import Control.Applicative.Free.Zero

import Data.List.Zero
import Data.Bifunctor (Bifunctor(bimap))
import FFunctor
import FFunctor.Lift1
import FFunctor.FCompose
import FMonad

-- * Type definitions

-- | The Free (left zero + left catch) 'Alternative'.
-- 
-- The constructors of @Free@ is named intentionally verbose.
-- 
-- To construct a value of @Free f a@, a convenient and recommended
-- way is to use 'liftFree' and methods of @Alternative (Free f)@ instances.
--
-- To pattern match a value of @Free f a@, a convenient and recommended
-- way is to use 'ApZOf' and 'SumZOf' pattern synonyms, along with
-- 'viewFactor' and 'viewSummand' to pattern match on @Factor@ and @Summand@
-- further.
data Free f a where
  FreeTrivial :: Trivial f a -> Free f a
  FreeSumZOf' :: NontrivialSumZ (Summand f) a -> Free f a
  FreeApZOf' :: NontrivialApZ (Factor f) a -> Free f a
  deriving (forall a b. (a -> b) -> Free f a -> Free f b)
-> (forall a b. a -> Free f b -> Free f a) -> Functor (Free f)
forall a b. a -> Free f b -> Free f a
forall a b. (a -> b) -> Free f a -> Free f b
forall (f :: * -> *) a b. Functor f => a -> Free f b -> Free f a
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Free f a -> Free f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Free f a -> Free f b
fmap :: forall a b. (a -> b) -> Free f a -> Free f b
$c<$ :: forall (f :: * -> *) a b. Functor f => a -> Free f b -> Free f a
<$ :: forall a b. a -> Free f b -> Free f a
Functor

instance (Functor f) => Applicative (Free f) where
  pure :: forall a. a -> Free f a
pure = Trivial f a -> Free f a
forall (f :: * -> *) a. Trivial f a -> Free f a
FreeTrivial (Trivial f a -> Free f a) -> (a -> Trivial f a) -> a -> Free f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Trivial f a
forall (f :: * -> *) a. a -> Trivial f a
TrivialPure
  Free f (a -> b)
x <*> :: forall a b. Free f (a -> b) -> Free f a -> Free f b
<*> Free f a
y = ApZ (Factor f) b -> Free f b
forall (f :: * -> *) a. Functor f => ApZ (Factor f) a -> Free f a
reviewApZ (Free f (a -> b) -> ApZ (Factor f) (a -> b)
forall (f :: * -> *) a. Free f a -> ApZ (Factor f) a
viewApZ Free f (a -> b)
x ApZ (Factor f) (a -> b) -> ApZ (Factor f) a -> ApZ (Factor f) b
forall a b.
ApZ (Factor f) (a -> b) -> ApZ (Factor f) a -> ApZ (Factor f) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Free f a -> ApZ (Factor f) a
forall (f :: * -> *) a. Free f a -> ApZ (Factor f) a
viewApZ Free f a
y)

instance (Functor f) => Alternative (Free f) where
  empty :: forall a. Free f a
empty = Trivial f a -> Free f a
forall (f :: * -> *) a. Trivial f a -> Free f a
FreeTrivial Trivial f a
forall (f :: * -> *) a. Trivial f a
TrivialZero
  Free f a
x <|> :: forall a. Free f a -> Free f a -> Free f a
<|> Free f a
y = SumZ (Summand f) a -> Free f a
forall (f :: * -> *) a. SumZ (Summand f) a -> Free f a
reviewSumZ (Free f a -> SumZ (Summand f) a
forall (f :: * -> *) a. Free f a -> SumZ (Summand f) a
viewSumZ Free f a
x SumZ (Summand f) a -> SumZ (Summand f) a -> SumZ (Summand f) a
forall a. Semigroup a => a -> a -> a
<> Free f a -> SumZ (Summand f) a
forall (f :: * -> *) a. Free f a -> SumZ (Summand f) a
viewSumZ Free f a
y)

instance FFunctor Free where
  ffmap :: forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> Free g x -> Free h x
ffmap = (forall x. g x -> h x) -> Free g x -> Free h x
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> Free f a -> Free g a
hoistFree

instance FMonad Free where
  fpure :: forall (g :: * -> *). Functor g => g ~> Free g
fpure = g x -> Free g x
forall (f :: * -> *) a. f a -> Free f a
liftFree
  fbind :: forall (g :: * -> *) (h :: * -> *) a.
(Functor g, Functor h) =>
(g ~> Free h) -> Free g a -> Free h a
fbind = (forall x. g x -> Free h x) -> Free g a -> Free h a
forall (f :: * -> *) (g :: * -> *) a.
Alternative g =>
(forall x. f x -> g x) -> Free f a -> g a
foldFree

-- | Subexpressions of @'Free' f a@ which can't be written as any one of
--
-- * @empty@
-- * @pure a@
-- * Nontrivial sum @x <|> y@
newtype Summand f a = Summand {
    forall (f :: * -> *) a.
Summand f a -> Either (f a) (NontrivialApZ (Factor f) a)
runSummand :: Either (f a) (NontrivialApZ (Factor f) a) }
  deriving ((forall a b. (a -> b) -> Summand f a -> Summand f b)
-> (forall a b. a -> Summand f b -> Summand f a)
-> Functor (Summand f)
forall a b. a -> Summand f b -> Summand f a
forall a b. (a -> b) -> Summand f a -> Summand f b
forall (f :: * -> *) a b.
Functor f =>
a -> Summand f b -> Summand f a
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Summand f a -> Summand f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Summand f a -> Summand f b
fmap :: forall a b. (a -> b) -> Summand f a -> Summand f b
$c<$ :: forall (f :: * -> *) a b.
Functor f =>
a -> Summand f b -> Summand f a
<$ :: forall a b. a -> Summand f b -> Summand f a
Functor) via Lift1 (FCompose NontrivialApZ Factor) f
  deriving ((forall (f :: * -> *). Functor f => Functor (Summand f)) =>
(forall (g :: * -> *) (h :: * -> *) x.
 (Functor g, Functor h) =>
 (g ~> h) -> Summand g x -> Summand h x)
-> FFunctor Summand
forall (f :: * -> *). Functor f => Functor (Summand f)
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> Summand g x -> Summand h x
forall (ff :: FF).
(forall (g :: * -> *). Functor g => Functor (ff g)) =>
(forall (g :: * -> *) (h :: * -> *) x.
 (Functor g, Functor h) =>
 (g ~> h) -> ff g x -> ff h x)
-> FFunctor ff
$cffmap :: forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> Summand g x -> Summand h x
ffmap :: forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> Summand g x -> Summand h x
FFunctor) via Lift1 (FCompose NontrivialApZ Factor)

-- | Subexpressions of @'Free' f a@ which can't be written as any one of
--
-- * @empty@
-- * @pure a@
-- * Nontrivial product @x <*> y@
newtype Factor f a = Factor {
    forall (f :: * -> *) a.
Factor f a -> Either (f a) (NontrivialSumZ (Summand f) a)
runFactor :: Either (f a) (NontrivialSumZ (Summand f) a) }
  deriving ((forall a b. (a -> b) -> Factor f a -> Factor f b)
-> (forall a b. a -> Factor f b -> Factor f a)
-> Functor (Factor f)
forall a b. a -> Factor f b -> Factor f a
forall a b. (a -> b) -> Factor f a -> Factor f b
forall (f :: * -> *) a b.
Functor f =>
a -> Factor f b -> Factor f a
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Factor f a -> Factor f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Factor f a -> Factor f b
fmap :: forall a b. (a -> b) -> Factor f a -> Factor f b
$c<$ :: forall (f :: * -> *) a b.
Functor f =>
a -> Factor f b -> Factor f a
<$ :: forall a b. a -> Factor f b -> Factor f a
Functor) via Lift1 (FCompose NontrivialSumZ Summand) f
  deriving ((forall (f :: * -> *). Functor f => Functor (Factor f)) =>
(forall (g :: * -> *) (h :: * -> *) x.
 (Functor g, Functor h) =>
 (g ~> h) -> Factor g x -> Factor h x)
-> FFunctor Factor
forall (f :: * -> *). Functor f => Functor (Factor f)
forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> Factor g x -> Factor h x
forall (ff :: FF).
(forall (g :: * -> *). Functor g => Functor (ff g)) =>
(forall (g :: * -> *) (h :: * -> *) x.
 (Functor g, Functor h) =>
 (g ~> h) -> ff g x -> ff h x)
-> FFunctor ff
$cffmap :: forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> Factor g x -> Factor h x
ffmap :: forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> Factor g x -> Factor h x
FFunctor) via Lift1 (FCompose NontrivialSumZ Summand)

viewSumZ :: Free f a -> SumZ (Summand f) a
viewSumZ :: forall (f :: * -> *) a. Free f a -> SumZ (Summand f) a
viewSumZ Free f a
e = case Free f a
e of
  FreeTrivial Trivial f a
tfa -> Trivial (Summand f) a -> SumZ (Summand f) a
forall (f :: * -> *) a. Trivial f a -> SumZ f a
trivialSumZ (Trivial (Summand f) a -> SumZ (Summand f) a)
-> Trivial (Summand f) a -> SumZ (Summand f) a
forall a b. (a -> b) -> a -> b
$ (forall x. f x -> Summand f x)
-> Trivial f a -> Trivial (Summand f) a
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> Trivial f a -> Trivial g a
hoistTrivial (Either (f x) (NontrivialApZ (Factor f) x) -> Summand f x
forall (f :: * -> *) a.
Either (f a) (NontrivialApZ (Factor f) a) -> Summand f a
Summand (Either (f x) (NontrivialApZ (Factor f) x) -> Summand f x)
-> (f x -> Either (f x) (NontrivialApZ (Factor f) x))
-> f x
-> Summand f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> Either (f x) (NontrivialApZ (Factor f) x)
forall a b. a -> Either a b
Left) Trivial f a
tfa
  FreeSumZOf' NontrivialSumZ (Summand f) a
fas -> NontrivialSumZ (Summand f) a -> SumZ (Summand f) a
forall (f :: * -> *) a. NontrivialSumZ f a -> SumZ f a
toSumZ NontrivialSumZ (Summand f) a
fas
  FreeApZOf' NontrivialApZ (Factor f) a
fas -> Summand f a -> SumZ (Summand f) a
forall a. a -> ListZ a a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Summand f a -> SumZ (Summand f) a)
-> (NontrivialApZ (Factor f) a -> Summand f a)
-> NontrivialApZ (Factor f) a
-> SumZ (Summand f) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either (f a) (NontrivialApZ (Factor f) a) -> Summand f a
forall (f :: * -> *) a.
Either (f a) (NontrivialApZ (Factor f) a) -> Summand f a
Summand (Either (f a) (NontrivialApZ (Factor f) a) -> Summand f a)
-> (NontrivialApZ (Factor f) a
    -> Either (f a) (NontrivialApZ (Factor f) a))
-> NontrivialApZ (Factor f) a
-> Summand f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NontrivialApZ (Factor f) a
-> Either (f a) (NontrivialApZ (Factor f) a)
forall a b. b -> Either a b
Right (NontrivialApZ (Factor f) a -> SumZ (Summand f) a)
-> NontrivialApZ (Factor f) a -> SumZ (Summand f) a
forall a b. (a -> b) -> a -> b
$ NontrivialApZ (Factor f) a
fas

reviewSumZ :: SumZ (Summand f) a -> Free f a
reviewSumZ :: forall (f :: * -> *) a. SumZ (Summand f) a -> Free f a
reviewSumZ SumZ (Summand f) a
e = case SumZ (Summand f) a
-> Either (Trivial (Summand f) a) (NontrivialSumZ (Summand f) a)
forall (f :: * -> *) a.
SumZ f a -> Either (Trivial f a) (NontrivialSumZ f a)
nontrivialSumZ SumZ (Summand f) a
e of
  Left Trivial (Summand f) a
tfa  -> (forall x. Summand f x -> Free f x)
-> Trivial (Summand f) a -> Free f a
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> Free g x) -> Trivial f a -> Free g a
trivialFree Summand f x -> Free f x
forall x. Summand f x -> Free f x
forall (f :: * -> *) a. Summand f a -> Free f a
injectSummand Trivial (Summand f) a
tfa
  Right NontrivialSumZ (Summand f) a
fas    -> NontrivialSumZ (Summand f) a -> Free f a
forall (f :: * -> *) a. NontrivialSumZ (Summand f) a -> Free f a
FreeSumZOf' NontrivialSumZ (Summand f) a
fas
  where
    injectSummand :: Summand f a -> Free f a
    injectSummand :: forall (f :: * -> *) a. Summand f a -> Free f a
injectSummand = (f a -> Free f a)
-> (NontrivialApZ (Factor f) a -> Free f a)
-> Either (f a) (NontrivialApZ (Factor f) a)
-> Free f a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either f a -> Free f a
forall (f :: * -> *) a. f a -> Free f a
liftFree NontrivialApZ (Factor f) a -> Free f a
forall (f :: * -> *) a. NontrivialApZ (Factor f) a -> Free f a
FreeApZOf' (Either (f a) (NontrivialApZ (Factor f) a) -> Free f a)
-> (Summand f a -> Either (f a) (NontrivialApZ (Factor f) a))
-> Summand f a
-> Free f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Summand f a -> Either (f a) (NontrivialApZ (Factor f) a)
forall (f :: * -> *) a.
Summand f a -> Either (f a) (NontrivialApZ (Factor f) a)
runSummand

-- | View @Free f a@ as a sum of @Summand f@, terminated by
--   either @Nil@ or @Zee a@ (corresponding @empty@ or @pure a@ respectively)
pattern SumZOf :: SumZ (Summand f) a -> Free f a
pattern $mSumZOf :: forall {r} {f :: * -> *} {a}.
Free f a -> (SumZ (Summand f) a -> r) -> ((# #) -> r) -> r
$bSumZOf :: forall (f :: * -> *) a. SumZ (Summand f) a -> Free f a
SumZOf sz <- (viewSumZ -> sz)
  where SumZOf SumZ (Summand f) a
sz = SumZ (Summand f) a -> Free f a
forall (f :: * -> *) a. SumZ (Summand f) a -> Free f a
reviewSumZ SumZ (Summand f) a
sz

{-# COMPLETE SumZOf #-}

viewApZ :: Free f a -> ApZ (Factor f) a
viewApZ :: forall (f :: * -> *) a. Free f a -> ApZ (Factor f) a
viewApZ Free f a
e = case Free f a
e of
  FreeTrivial Trivial f a
tfa -> Trivial (Factor f) a -> ApZ (Factor f) a
forall (f :: * -> *) a. Trivial f a -> ApZ f a
trivialApZ (Trivial (Factor f) a -> ApZ (Factor f) a)
-> Trivial (Factor f) a -> ApZ (Factor f) a
forall a b. (a -> b) -> a -> b
$ (forall x. f x -> Factor f x)
-> Trivial f a -> Trivial (Factor f) a
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> Trivial f a -> Trivial g a
hoistTrivial (Either (f x) (NontrivialSumZ (Summand f) x) -> Factor f x
forall (f :: * -> *) a.
Either (f a) (NontrivialSumZ (Summand f) a) -> Factor f a
Factor (Either (f x) (NontrivialSumZ (Summand f) x) -> Factor f x)
-> (f x -> Either (f x) (NontrivialSumZ (Summand f) x))
-> f x
-> Factor f x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> Either (f x) (NontrivialSumZ (Summand f) x)
forall a b. a -> Either a b
Left) Trivial f a
tfa
  FreeSumZOf' NontrivialSumZ (Summand f) a
fas -> Factor f a -> ApZ (Factor f) a
forall (f :: * -> *) a. f a -> ApZ f a
liftApZ (Factor f a -> ApZ (Factor f) a)
-> (NontrivialSumZ (Summand f) a -> Factor f a)
-> NontrivialSumZ (Summand f) a
-> ApZ (Factor f) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either (f a) (NontrivialSumZ (Summand f) a) -> Factor f a
forall (f :: * -> *) a.
Either (f a) (NontrivialSumZ (Summand f) a) -> Factor f a
Factor (Either (f a) (NontrivialSumZ (Summand f) a) -> Factor f a)
-> (NontrivialSumZ (Summand f) a
    -> Either (f a) (NontrivialSumZ (Summand f) a))
-> NontrivialSumZ (Summand f) a
-> Factor f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NontrivialSumZ (Summand f) a
-> Either (f a) (NontrivialSumZ (Summand f) a)
forall a b. b -> Either a b
Right (NontrivialSumZ (Summand f) a -> ApZ (Factor f) a)
-> NontrivialSumZ (Summand f) a -> ApZ (Factor f) a
forall a b. (a -> b) -> a -> b
$ NontrivialSumZ (Summand f) a
fas
  FreeApZOf' NontrivialApZ (Factor f) a
fas -> NontrivialApZ (Factor f) a -> ApZ (Factor f) a
forall (f :: * -> *) a. NontrivialApZ f a -> ApZ f a
toApZ NontrivialApZ (Factor f) a
fas

reviewApZ :: Functor f => ApZ (Factor f) a -> Free f a
reviewApZ :: forall (f :: * -> *) a. Functor f => ApZ (Factor f) a -> Free f a
reviewApZ ApZ (Factor f) a
e = case ApZ (Factor f) a
-> Either (Trivial (Factor f) a) (NontrivialApZ (Factor f) a)
forall (f :: * -> *) a.
Functor f =>
ApZ f a -> Either (Trivial f a) (NontrivialApZ f a)
nontrivialApZ ApZ (Factor f) a
e of
  Left Trivial (Factor f) a
tfa -> (forall x. Factor f x -> Free f x)
-> Trivial (Factor f) a -> Free f a
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> Free g x) -> Trivial f a -> Free g a
trivialFree Factor f x -> Free f x
forall x. Factor f x -> Free f x
forall (f :: * -> *) a. Factor f a -> Free f a
injectFactor Trivial (Factor f) a
tfa
  Right NontrivialApZ (Factor f) a
fas    -> NontrivialApZ (Factor f) a -> Free f a
forall (f :: * -> *) a. NontrivialApZ (Factor f) a -> Free f a
FreeApZOf' NontrivialApZ (Factor f) a
fas
  where
    injectFactor :: Factor f a -> Free f a
    injectFactor :: forall (f :: * -> *) a. Factor f a -> Free f a
injectFactor = (f a -> Free f a)
-> (NontrivialSumZ (Summand f) a -> Free f a)
-> Either (f a) (NontrivialSumZ (Summand f) a)
-> Free f a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either f a -> Free f a
forall (f :: * -> *) a. f a -> Free f a
liftFree NontrivialSumZ (Summand f) a -> Free f a
forall (f :: * -> *) a. NontrivialSumZ (Summand f) a -> Free f a
FreeSumZOf' (Either (f a) (NontrivialSumZ (Summand f) a) -> Free f a)
-> (Factor f a -> Either (f a) (NontrivialSumZ (Summand f) a))
-> Factor f a
-> Free f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Factor f a -> Either (f a) (NontrivialSumZ (Summand f) a)
forall (f :: * -> *) a.
Factor f a -> Either (f a) (NontrivialSumZ (Summand f) a)
runFactor

-- | View @Free f a@ as a product of @Factor f@, terminated by
--   either @'Zero'@ or @'Pure' a@ (corresponding @empty@ or @pure a@ respectively)
pattern ApZOf :: Functor f => () => ApZ (Factor f) a -> Free f a
pattern $mApZOf :: forall {r} {f :: * -> *} {a}.
Functor f =>
Free f a -> (ApZ (Factor f) a -> r) -> ((# #) -> r) -> r
$bApZOf :: forall (f :: * -> *) a. Functor f => ApZ (Factor f) a -> Free f a
ApZOf az <- (viewApZ -> az)
  where ApZOf ApZ (Factor f) a
az = ApZ (Factor f) a -> Free f a
forall (f :: * -> *) a. Functor f => ApZ (Factor f) a -> Free f a
reviewApZ ApZ (Factor f) a
az

{-# COMPLETE ApZOf #-}

-- | @Summand f a@ is either @f a@ or a product of multiple @Factor f@ values.
--   The @Right@ case never returns a trivial summand, which is one of
--
-- * @'Zero'@,
-- * @'Pure' a@,
-- * @'liftApZ' fac@ for one @fac :: Factor f a@
viewSummand :: Summand f a -> Either (f a) (ApZ (Factor f) a)
viewSummand :: forall (f :: * -> *) a.
Summand f a -> Either (f a) (ApZ (Factor f) a)
viewSummand = (NontrivialApZ (Factor f) a -> ApZ (Factor f) a)
-> Either (f a) (NontrivialApZ (Factor f) a)
-> Either (f a) (ApZ (Factor f) a)
forall a b. (a -> b) -> Either (f a) a -> Either (f a) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NontrivialApZ (Factor f) a -> ApZ (Factor f) a
forall (f :: * -> *) a. NontrivialApZ f a -> ApZ f a
toApZ (Either (f a) (NontrivialApZ (Factor f) a)
 -> Either (f a) (ApZ (Factor f) a))
-> (Summand f a -> Either (f a) (NontrivialApZ (Factor f) a))
-> Summand f a
-> Either (f a) (ApZ (Factor f) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Summand f a -> Either (f a) (NontrivialApZ (Factor f) a)
forall (f :: * -> *) a.
Summand f a -> Either (f a) (NontrivialApZ (Factor f) a)
runSummand

-- | @Factor f a@ is either @f a@ or a sum of multiple @Summand f@ values.
--   The @Right@ case never returns a trivial factor, which is one of
--
-- * @'Nil'@,
-- * @'Zee' a@,
-- * @'Cons' suma Nil@ for one @suma :: Summand f a@
viewFactor :: Factor f a -> Either (f a) (SumZ (Summand f) a)
viewFactor :: forall (f :: * -> *) a.
Factor f a -> Either (f a) (SumZ (Summand f) a)
viewFactor = (NontrivialSumZ (Summand f) a -> SumZ (Summand f) a)
-> Either (f a) (NontrivialSumZ (Summand f) a)
-> Either (f a) (SumZ (Summand f) a)
forall a b. (a -> b) -> Either (f a) a -> Either (f a) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NontrivialSumZ (Summand f) a -> SumZ (Summand f) a
forall (f :: * -> *) a. NontrivialSumZ f a -> SumZ f a
toSumZ (Either (f a) (NontrivialSumZ (Summand f) a)
 -> Either (f a) (SumZ (Summand f) a))
-> (Factor f a -> Either (f a) (NontrivialSumZ (Summand f) a))
-> Factor f a
-> Either (f a) (SumZ (Summand f) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Factor f a -> Either (f a) (NontrivialSumZ (Summand f) a)
forall (f :: * -> *) a.
Factor f a -> Either (f a) (NontrivialSumZ (Summand f) a)
runFactor

hoistFree :: (forall x. f x -> g x) -> Free f a -> Free g a
hoistFree :: forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> Free f a -> Free g a
hoistFree forall x. f x -> g x
fg Free f a
e = case Free f a
e of
  FreeTrivial Trivial f a
tfa -> Trivial g a -> Free g a
forall (f :: * -> *) a. Trivial f a -> Free f a
FreeTrivial ((forall x. f x -> g x) -> Trivial f a -> Trivial g a
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> Trivial f a -> Trivial g a
hoistTrivial f x -> g x
forall x. f x -> g x
fg Trivial f a
tfa)
  FreeSumZOf' NontrivialSumZ (Summand f) a
fas -> NontrivialSumZ (Summand g) a -> Free g a
forall (f :: * -> *) a. NontrivialSumZ (Summand f) a -> Free f a
FreeSumZOf' ((forall x. Summand f x -> Summand g x)
-> NontrivialSumZ (Summand f) a -> NontrivialSumZ (Summand g) a
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> NontrivialSumZ f a -> NontrivialSumZ g a
hoistNontrivialSumZ ((forall x. f x -> g x) -> Summand f x -> Summand g x
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> Summand f a -> Summand g a
hoistSummand f x -> g x
forall x. f x -> g x
fg) NontrivialSumZ (Summand f) a
fas)
  FreeApZOf' NontrivialApZ (Factor f) a
fas -> NontrivialApZ (Factor g) a -> Free g a
forall (f :: * -> *) a. NontrivialApZ (Factor f) a -> Free f a
FreeApZOf' ((forall x. Factor f x -> Factor g x)
-> NontrivialApZ (Factor f) a -> NontrivialApZ (Factor g) a
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> NontrivialApZ f a -> NontrivialApZ g a
hoistNontrivialApZ ((forall x. f x -> g x) -> Factor f x -> Factor g x
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> Factor f a -> Factor g a
hoistFactor f x -> g x
forall x. f x -> g x
fg) NontrivialApZ (Factor f) a
fas)

hoistFactor :: (forall x. f x -> g x) -> Factor f a -> Factor g a
hoistFactor :: forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> Factor f a -> Factor g a
hoistFactor forall x. f x -> g x
fg = Either (g a) (NontrivialSumZ (Summand g) a) -> Factor g a
forall (f :: * -> *) a.
Either (f a) (NontrivialSumZ (Summand f) a) -> Factor f a
Factor (Either (g a) (NontrivialSumZ (Summand g) a) -> Factor g a)
-> (Factor f a -> Either (g a) (NontrivialSumZ (Summand g) a))
-> Factor f a
-> Factor g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f a -> g a)
-> (NontrivialSumZ (Summand f) a -> NontrivialSumZ (Summand g) a)
-> Either (f a) (NontrivialSumZ (Summand f) a)
-> Either (g a) (NontrivialSumZ (Summand g) a)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap f a -> g a
forall x. f x -> g x
fg ((forall x. Summand f x -> Summand g x)
-> NontrivialSumZ (Summand f) a -> NontrivialSumZ (Summand g) a
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> NontrivialSumZ f a -> NontrivialSumZ g a
hoistNontrivialSumZ ((forall x. f x -> g x) -> Summand f x -> Summand g x
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> Summand f a -> Summand g a
hoistSummand f x -> g x
forall x. f x -> g x
fg)) (Either (f a) (NontrivialSumZ (Summand f) a)
 -> Either (g a) (NontrivialSumZ (Summand g) a))
-> (Factor f a -> Either (f a) (NontrivialSumZ (Summand f) a))
-> Factor f a
-> Either (g a) (NontrivialSumZ (Summand g) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Factor f a -> Either (f a) (NontrivialSumZ (Summand f) a)
forall (f :: * -> *) a.
Factor f a -> Either (f a) (NontrivialSumZ (Summand f) a)
runFactor

hoistSummand :: (forall x. f x -> g x) -> Summand f a -> Summand g a
hoistSummand :: forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> Summand f a -> Summand g a
hoistSummand forall x. f x -> g x
fg = Either (g a) (NontrivialApZ (Factor g) a) -> Summand g a
forall (f :: * -> *) a.
Either (f a) (NontrivialApZ (Factor f) a) -> Summand f a
Summand (Either (g a) (NontrivialApZ (Factor g) a) -> Summand g a)
-> (Summand f a -> Either (g a) (NontrivialApZ (Factor g) a))
-> Summand f a
-> Summand g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f a -> g a)
-> (NontrivialApZ (Factor f) a -> NontrivialApZ (Factor g) a)
-> Either (f a) (NontrivialApZ (Factor f) a)
-> Either (g a) (NontrivialApZ (Factor g) a)
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap f a -> g a
forall x. f x -> g x
fg ((forall x. Factor f x -> Factor g x)
-> NontrivialApZ (Factor f) a -> NontrivialApZ (Factor g) a
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> NontrivialApZ f a -> NontrivialApZ g a
hoistNontrivialApZ ((forall x. f x -> g x) -> Factor f x -> Factor g x
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> Factor f a -> Factor g a
hoistFactor f x -> g x
forall x. f x -> g x
fg)) (Either (f a) (NontrivialApZ (Factor f) a)
 -> Either (g a) (NontrivialApZ (Factor g) a))
-> (Summand f a -> Either (f a) (NontrivialApZ (Factor f) a))
-> Summand f a
-> Either (g a) (NontrivialApZ (Factor g) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Summand f a -> Either (f a) (NontrivialApZ (Factor f) a)
forall (f :: * -> *) a.
Summand f a -> Either (f a) (NontrivialApZ (Factor f) a)
runSummand

liftFree :: f a -> Free f a
liftFree :: forall (f :: * -> *) a. f a -> Free f a
liftFree = Trivial f a -> Free f a
forall (f :: * -> *) a. Trivial f a -> Free f a
FreeTrivial (Trivial f a -> Free f a)
-> (f a -> Trivial f a) -> f a -> Free f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> Trivial f a
forall (f :: * -> *) a. f a -> Trivial f a
TrivialLift

foldFree :: forall f g a. (Alternative g) => (forall x. f x -> g x) -> Free f a -> g a
foldFree :: forall (f :: * -> *) (g :: * -> *) a.
Alternative g =>
(forall x. f x -> g x) -> Free f a -> g a
foldFree forall x. f x -> g x
handle = SumZ (Summand f) a -> g a
forall b. SumZ (Summand f) b -> g b
goSumZ (SumZ (Summand f) a -> g a)
-> (Free f a -> SumZ (Summand f) a) -> Free f a -> g a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Free f a -> SumZ (Summand f) a
forall (f :: * -> *) a. Free f a -> SumZ (Summand f) a
viewSumZ
  where
    goSumZ :: forall b. SumZ (Summand f) b -> g b
    goSumZ :: forall b. SumZ (Summand f) b -> g b
goSumZ = g b
-> (b -> g b)
-> (Summand f b -> g b -> g b)
-> ListZ b (Summand f b)
-> g b
forall r e a. r -> (e -> r) -> (a -> r -> r) -> ListZ e a -> r
foldrZ g b
forall a. g a
forall (f :: * -> *) a. Alternative f => f a
empty b -> g b
forall a. a -> g a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (g b -> g b -> g b
forall a. g a -> g a -> g a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (g b -> g b -> g b)
-> (Summand f b -> g b) -> Summand f b -> g b -> g b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Summand f b -> g b
forall b. Summand f b -> g b
goSummand)

    goSummand :: forall b. Summand f b -> g b
    goSummand :: forall b. Summand f b -> g b
goSummand = (f b -> g b)
-> (ApZ (Factor f) b -> g b)
-> Either (f b) (ApZ (Factor f) b)
-> g b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either f b -> g b
forall x. f x -> g x
handle ApZ (Factor f) b -> g b
forall b. ApZ (Factor f) b -> g b
goApZ (Either (f b) (ApZ (Factor f) b) -> g b)
-> (Summand f b -> Either (f b) (ApZ (Factor f) b))
-> Summand f b
-> g b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Summand f b -> Either (f b) (ApZ (Factor f) b)
forall (f :: * -> *) a.
Summand f a -> Either (f a) (ApZ (Factor f) a)
viewSummand

    goApZ :: forall b. ApZ (Factor f) b -> g b
    goApZ :: forall b. ApZ (Factor f) b -> g b
goApZ = (forall r. Factor f r -> g r)
-> (forall a. g a) -> ApZ (Factor f) b -> g b
forall (g :: * -> *) (f :: * -> *) a.
Applicative g =>
(forall r. f r -> g r) -> (forall r. g r) -> ApZ f a -> g a
foldApZ Factor f r -> g r
forall r. Factor f r -> g r
goFactor g r
forall a. g a
forall (f :: * -> *) a. Alternative f => f a
empty

    goFactor :: forall b. Factor f b -> g b
    goFactor :: forall r. Factor f r -> g r
goFactor = (f b -> g b)
-> (SumZ (Summand f) b -> g b)
-> Either (f b) (SumZ (Summand f) b)
-> g b
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either f b -> g b
forall x. f x -> g x
handle SumZ (Summand f) b -> g b
forall b. SumZ (Summand f) b -> g b
goSumZ (Either (f b) (SumZ (Summand f) b) -> g b)
-> (Factor f b -> Either (f b) (SumZ (Summand f) b))
-> Factor f b
-> g b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Factor f b -> Either (f b) (SumZ (Summand f) b)
forall (f :: * -> *) a.
Factor f a -> Either (f a) (SumZ (Summand f) a)
viewFactor

----

-- | Trivial expressions
data Trivial f a = TrivialZero | TrivialPure a | TrivialLift (f a)
  deriving ((forall a b. (a -> b) -> Trivial f a -> Trivial f b)
-> (forall a b. a -> Trivial f b -> Trivial f a)
-> Functor (Trivial f)
forall a b. a -> Trivial f b -> Trivial f a
forall a b. (a -> b) -> Trivial f a -> Trivial f b
forall (f :: * -> *) a b.
Functor f =>
a -> Trivial f b -> Trivial f a
forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Trivial f a -> Trivial f b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (f :: * -> *) a b.
Functor f =>
(a -> b) -> Trivial f a -> Trivial f b
fmap :: forall a b. (a -> b) -> Trivial f a -> Trivial f b
$c<$ :: forall (f :: * -> *) a b.
Functor f =>
a -> Trivial f b -> Trivial f a
<$ :: forall a b. a -> Trivial f b -> Trivial f a
Functor)

hoistTrivial :: (forall x. f x -> g x) -> Trivial f a -> Trivial g a
hoistTrivial :: forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> Trivial f a -> Trivial g a
hoistTrivial forall x. f x -> g x
fg Trivial f a
e = case Trivial f a
e of
  Trivial f a
TrivialZero -> Trivial g a
forall (f :: * -> *) a. Trivial f a
TrivialZero
  TrivialPure a
a -> a -> Trivial g a
forall (f :: * -> *) a. a -> Trivial f a
TrivialPure a
a
  TrivialLift f a
fa -> g a -> Trivial g a
forall (f :: * -> *) a. f a -> Trivial f a
TrivialLift (f a -> g a
forall x. f x -> g x
fg f a
fa)

trivialFree :: (forall x. f x -> Free g x) -> Trivial f a -> Free g a
trivialFree :: forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> Free g x) -> Trivial f a -> Free g a
trivialFree forall x. f x -> Free g x
k Trivial f a
e = case Trivial f a
e of
  Trivial f a
TrivialZero -> Trivial g a -> Free g a
forall (f :: * -> *) a. Trivial f a -> Free f a
FreeTrivial Trivial g a
forall (f :: * -> *) a. Trivial f a
TrivialZero
  TrivialPure a
a -> Trivial g a -> Free g a
forall (f :: * -> *) a. Trivial f a -> Free f a
FreeTrivial (a -> Trivial g a
forall (f :: * -> *) a. a -> Trivial f a
TrivialPure a
a)
  TrivialLift f a
fa -> f a -> Free g a
forall x. f x -> Free g x
k f a
fa

-- | Formal sum of @f a@ ending in either @pure a@ (@Zee a@) or @empty@ (Nil).
type SumZ f a = ListZ a (f a)

-- | @Trivial f a + NontrivialSumZ f a ~ SumZ f a = ListZ a (f a)@
data NontrivialSumZ f a =
    ConsZee (f a) a
  | ConsMany (f a) (f a) (ListZ a (f a))

instance Functor f => Functor (NontrivialSumZ f) where
  fmap :: forall a b. (a -> b) -> NontrivialSumZ f a -> NontrivialSumZ f b
fmap a -> b
h NontrivialSumZ f a
e = case NontrivialSumZ f a
e of
    ConsZee f a
fa a
a -> f b -> b -> NontrivialSumZ f b
forall (f :: * -> *) a. f a -> a -> NontrivialSumZ f a
ConsZee ((a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
h f a
fa) (a -> b
h a
a)
    ConsMany f a
fa f a
fa' ListZ a (f a)
rest -> f b -> f b -> ListZ b (f b) -> NontrivialSumZ f b
forall (f :: * -> *) a.
f a -> f a -> ListZ a (f a) -> NontrivialSumZ f a
ConsMany ((a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
h f a
fa) ((a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
h f a
fa') ((a -> b) -> (f a -> f b) -> ListZ a (f a) -> ListZ b (f b)
forall a b c d. (a -> b) -> (c -> d) -> ListZ a c -> ListZ b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap a -> b
h ((a -> b) -> f a -> f b
forall a b. (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
h) ListZ a (f a)
rest)

instance FFunctor NontrivialSumZ where
  ffmap :: forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> NontrivialSumZ g x -> NontrivialSumZ h x
ffmap = (forall x. g x -> h x) -> NontrivialSumZ g x -> NontrivialSumZ h x
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> NontrivialSumZ f a -> NontrivialSumZ g a
hoistNontrivialSumZ

hoistNontrivialSumZ :: (forall x. f x -> g x) -> NontrivialSumZ f a -> NontrivialSumZ g a
hoistNontrivialSumZ :: forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> NontrivialSumZ f a -> NontrivialSumZ g a
hoistNontrivialSumZ forall x. f x -> g x
fg NontrivialSumZ f a
e = case NontrivialSumZ f a
e of
    ConsZee f a
fa a
a -> g a -> a -> NontrivialSumZ g a
forall (f :: * -> *) a. f a -> a -> NontrivialSumZ f a
ConsZee (f a -> g a
forall x. f x -> g x
fg f a
fa) a
a
    ConsMany f a
fa f a
fa' ListZ a (f a)
rest -> g a -> g a -> ListZ a (g a) -> NontrivialSumZ g a
forall (f :: * -> *) a.
f a -> f a -> ListZ a (f a) -> NontrivialSumZ f a
ConsMany (f a -> g a
forall x. f x -> g x
fg f a
fa) (f a -> g a
forall x. f x -> g x
fg f a
fa') ((f a -> g a) -> ListZ a (f a) -> ListZ a (g a)
forall a b. (a -> b) -> ListZ a a -> ListZ a b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f a -> g a
forall x. f x -> g x
fg ListZ a (f a)
rest)

trivialSumZ :: Trivial f a -> SumZ f a
trivialSumZ :: forall (f :: * -> *) a. Trivial f a -> SumZ f a
trivialSumZ Trivial f a
e = case Trivial f a
e of
  Trivial f a
TrivialZero -> SumZ f a
forall e a. ListZ e a
Nil
  TrivialPure a
a -> a -> SumZ f a
forall e a. e -> ListZ e a
Zee a
a
  TrivialLift f a
fa -> f a -> SumZ f a -> SumZ f a
forall e a. a -> ListZ e a -> ListZ e a
Cons f a
fa SumZ f a
forall e a. ListZ e a
Nil

toSumZ :: NontrivialSumZ f a -> SumZ f a
toSumZ :: forall (f :: * -> *) a. NontrivialSumZ f a -> SumZ f a
toSumZ (ConsZee f a
fa a
a) = f a -> ListZ a (f a) -> ListZ a (f a)
forall e a. a -> ListZ e a -> ListZ e a
Cons f a
fa (a -> ListZ a (f a)
forall e a. e -> ListZ e a
Zee a
a)
toSumZ (ConsMany f a
fa f a
fa' ListZ a (f a)
rest) = f a -> ListZ a (f a) -> ListZ a (f a)
forall e a. a -> ListZ e a -> ListZ e a
Cons f a
fa (f a -> ListZ a (f a) -> ListZ a (f a)
forall e a. a -> ListZ e a -> ListZ e a
Cons f a
fa' ListZ a (f a)
rest)

nontrivialSumZ :: SumZ f a -> Either (Trivial f a) (NontrivialSumZ f a)
nontrivialSumZ :: forall (f :: * -> *) a.
SumZ f a -> Either (Trivial f a) (NontrivialSumZ f a)
nontrivialSumZ SumZ f a
e = case SumZ f a
e of
  SumZ f a
Nil -> Trivial f a -> Either (Trivial f a) (NontrivialSumZ f a)
forall a b. a -> Either a b
Left Trivial f a
forall (f :: * -> *) a. Trivial f a
TrivialZero
  Zee a
a -> Trivial f a -> Either (Trivial f a) (NontrivialSumZ f a)
forall a b. a -> Either a b
Left (Trivial f a -> Either (Trivial f a) (NontrivialSumZ f a))
-> Trivial f a -> Either (Trivial f a) (NontrivialSumZ f a)
forall a b. (a -> b) -> a -> b
$ a -> Trivial f a
forall (f :: * -> *) a. a -> Trivial f a
TrivialPure a
a
  Cons f a
fa SumZ f a
Nil -> Trivial f a -> Either (Trivial f a) (NontrivialSumZ f a)
forall a b. a -> Either a b
Left (Trivial f a -> Either (Trivial f a) (NontrivialSumZ f a))
-> Trivial f a -> Either (Trivial f a) (NontrivialSumZ f a)
forall a b. (a -> b) -> a -> b
$ f a -> Trivial f a
forall (f :: * -> *) a. f a -> Trivial f a
TrivialLift f a
fa
  Cons f a
fa (Zee a
a) -> NontrivialSumZ f a -> Either (Trivial f a) (NontrivialSumZ f a)
forall a b. b -> Either a b
Right (NontrivialSumZ f a -> Either (Trivial f a) (NontrivialSumZ f a))
-> NontrivialSumZ f a -> Either (Trivial f a) (NontrivialSumZ f a)
forall a b. (a -> b) -> a -> b
$ f a -> a -> NontrivialSumZ f a
forall (f :: * -> *) a. f a -> a -> NontrivialSumZ f a
ConsZee f a
fa a
a
  Cons f a
fa (Cons f a
fa' SumZ f a
rest) -> NontrivialSumZ f a -> Either (Trivial f a) (NontrivialSumZ f a)
forall a b. b -> Either a b
Right (NontrivialSumZ f a -> Either (Trivial f a) (NontrivialSumZ f a))
-> NontrivialSumZ f a -> Either (Trivial f a) (NontrivialSumZ f a)
forall a b. (a -> b) -> a -> b
$ f a -> f a -> SumZ f a -> NontrivialSumZ f a
forall (f :: * -> *) a.
f a -> f a -> ListZ a (f a) -> NontrivialSumZ f a
ConsMany f a
fa f a
fa' SumZ f a
rest

-- | @Trivial f a + NontrivialApZ f a ~ ApZ f a@
data NontrivialApZ f a where
  ApZero :: f a -> NontrivialApZ f b
  ApMany :: f a -> f b -> ApZ f (b -> a -> c) -> NontrivialApZ f c

deriving instance Functor (NontrivialApZ f)

instance FFunctor NontrivialApZ where
  ffmap :: forall (g :: * -> *) (h :: * -> *) x.
(Functor g, Functor h) =>
(g ~> h) -> NontrivialApZ g x -> NontrivialApZ h x
ffmap = (forall x. g x -> h x) -> NontrivialApZ g x -> NontrivialApZ h x
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> NontrivialApZ f a -> NontrivialApZ g a
hoistNontrivialApZ

hoistNontrivialApZ :: (forall x. f x -> g x) -> NontrivialApZ f a -> NontrivialApZ g a
hoistNontrivialApZ :: forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> NontrivialApZ f a -> NontrivialApZ g a
hoistNontrivialApZ forall x. f x -> g x
fg NontrivialApZ f a
e = case NontrivialApZ f a
e of
  ApZero f a
fa -> g a -> NontrivialApZ g a
forall (f :: * -> *) a b. f a -> NontrivialApZ f b
ApZero (f a -> g a
forall x. f x -> g x
fg f a
fa)
  ApMany f a
fa f b
fb ApZ f (b -> a -> a)
rest -> g a -> g b -> ApZ g (b -> a -> a) -> NontrivialApZ g a
forall (f :: * -> *) a b c.
f a -> f b -> ApZ f (b -> a -> c) -> NontrivialApZ f c
ApMany (f a -> g a
forall x. f x -> g x
fg f a
fa) (f b -> g b
forall x. f x -> g x
fg f b
fb) ((forall x. f x -> g x)
-> ApZ f (b -> a -> a) -> ApZ g (b -> a -> a)
forall (f :: * -> *) (g :: * -> *) a.
(forall x. f x -> g x) -> ApZ f a -> ApZ g a
hoistApZ f x -> g x
forall x. f x -> g x
fg ApZ f (b -> a -> a)
rest)

trivialApZ :: Trivial f a -> ApZ f a
trivialApZ :: forall (f :: * -> *) a. Trivial f a -> ApZ f a
trivialApZ Trivial f a
e = case Trivial f a
e of
  Trivial f a
TrivialZero -> ApZ f a
forall (f :: * -> *) a. ApZ f a
Zero
  TrivialPure a
a -> a -> ApZ f a
forall a (f :: * -> *). a -> ApZ f a
Pure a
a
  TrivialLift f a
fa -> f a -> ApZ f a
forall (f :: * -> *) a. f a -> ApZ f a
liftApZ f a
fa

toApZ :: NontrivialApZ f a -> ApZ f a
toApZ :: forall (f :: * -> *) a. NontrivialApZ f a -> ApZ f a
toApZ (ApZero f a
fa) = f a -> ApZ f (a -> a) -> ApZ f a
forall (f :: * -> *) a1 a. f a1 -> ApZ f (a1 -> a) -> ApZ f a
Ap f a
fa ApZ f (a -> a)
forall (f :: * -> *) a. ApZ f a
Zero
toApZ (ApMany f a
fa f b
fb ApZ f (b -> a -> a)
rest) = f a -> ApZ f (a -> a) -> ApZ f a
forall (f :: * -> *) a1 a. f a1 -> ApZ f (a1 -> a) -> ApZ f a
Ap f a
fa (f b -> ApZ f (b -> a -> a) -> ApZ f (a -> a)
forall (f :: * -> *) a1 a. f a1 -> ApZ f (a1 -> a) -> ApZ f a
Ap f b
fb ApZ f (b -> a -> a)
rest)

nontrivialApZ :: Functor f => ApZ f a -> Either (Trivial f a) (NontrivialApZ f a)
nontrivialApZ :: forall (f :: * -> *) a.
Functor f =>
ApZ f a -> Either (Trivial f a) (NontrivialApZ f a)
nontrivialApZ ApZ f a
e = case ApZ f a
e of
  Pure a
a -> Trivial f a -> Either (Trivial f a) (NontrivialApZ f a)
forall a b. a -> Either a b
Left (Trivial f a -> Either (Trivial f a) (NontrivialApZ f a))
-> Trivial f a -> Either (Trivial f a) (NontrivialApZ f a)
forall a b. (a -> b) -> a -> b
$ a -> Trivial f a
forall (f :: * -> *) a. a -> Trivial f a
TrivialPure a
a
  ApZ f a
Zero -> Trivial f a -> Either (Trivial f a) (NontrivialApZ f a)
forall a b. a -> Either a b
Left Trivial f a
forall (f :: * -> *) a. Trivial f a
TrivialZero
  Ap f a1
fa (Pure a1 -> a
k) -> Trivial f a -> Either (Trivial f a) (NontrivialApZ f a)
forall a b. a -> Either a b
Left (Trivial f a -> Either (Trivial f a) (NontrivialApZ f a))
-> Trivial f a -> Either (Trivial f a) (NontrivialApZ f a)
forall a b. (a -> b) -> a -> b
$ f a -> Trivial f a
forall (f :: * -> *) a. f a -> Trivial f a
TrivialLift (a1 -> a
k (a1 -> a) -> f a1 -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a1
fa)
  Ap f a1
fa ApZ f (a1 -> a)
Zero -> NontrivialApZ f a -> Either (Trivial f a) (NontrivialApZ f a)
forall a b. b -> Either a b
Right (NontrivialApZ f a -> Either (Trivial f a) (NontrivialApZ f a))
-> NontrivialApZ f a -> Either (Trivial f a) (NontrivialApZ f a)
forall a b. (a -> b) -> a -> b
$ f a1 -> NontrivialApZ f a
forall (f :: * -> *) a b. f a -> NontrivialApZ f b
ApZero f a1
fa
  Ap f a1
fa (Ap f a1
fb ApZ f (a1 -> a1 -> a)
rest) -> NontrivialApZ f a -> Either (Trivial f a) (NontrivialApZ f a)
forall a b. b -> Either a b
Right (NontrivialApZ f a -> Either (Trivial f a) (NontrivialApZ f a))
-> NontrivialApZ f a -> Either (Trivial f a) (NontrivialApZ f a)
forall a b. (a -> b) -> a -> b
$ f a1 -> f a1 -> ApZ f (a1 -> a1 -> a) -> NontrivialApZ f a
forall (f :: * -> *) a b c.
f a -> f b -> ApZ f (b -> a -> c) -> NontrivialApZ f c
ApMany f a1
fa f a1
fb ApZ f (a1 -> a1 -> a)
rest