{-# LANGUAGE CPP                 #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE InstanceSigs        #-}
{-# LANGUAGE PolyKinds           #-}
{-# LANGUAGE RankNTypes          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies        #-}

{-# OPTIONS_HADDOCK show-extensions #-}

module Control.Arrow.Free
  ( -- * Free arrow
    Arr (Id, Arr, Prod)
  , arrArr
  , liftArr
  , mapArr
  , foldArr

    -- * Free arrow (CPS style)
  , A (..)
  , fromA
  , toA
    -- * Free interface re-exports
  , FreeAlgebra2 (..)
  , wrapFree2
  , foldFree2
  , hoistFree2
  , joinFree2
  , bindFree2
    -- * Free 'ArrowChoice'
  , Choice (..)
  , liftArrChoice
  , foldArrChoice
  ) where

import           Prelude hiding (id, (.))
import           Control.Arrow (Arrow (..), ArrowChoice (..), (>>>))
import           Control.Category (Category (..))

import           Control.Algebra.Free2
  ( AlgebraType0
  , AlgebraType
  , FreeAlgebra2 (..)
  , Proof (..)
  , wrapFree2
  , foldFree2
  , hoistFree2
  , hoistFreeH2
  , joinFree2
  , bindFree2
  )
import           Control.Category.Free.Internal

data Arr f a b where
  Id    :: Arr f a a
  Cons  :: f b c     -> Queue (Arr f) a b -> Arr f a c
  Arr   :: (b -> c)  -> Arr f a b -> Arr f a c
  Prod  :: Arr f a b -> Arr f a c -> Arr f a (b, c)

arrArr :: (b -> c) -> Arr f b c
arrArr :: forall b c (f :: * -> * -> *). (b -> c) -> Arr f b c
arrArr b -> c
bc = forall a c (f :: * -> * -> *) a. (a -> c) -> Arr f a a -> Arr f a c
Arr b -> c
bc forall (f :: * -> * -> *) a. Arr f a a
Id

liftArr :: f a b
        -> Arr f a b
liftArr :: forall (f :: * -> * -> *) a b. f a b -> Arr f a b
liftArr f a b
f = forall (f :: * -> * -> *) a c a.
f a c -> Queue (Arr f) a a -> Arr f a c
Cons f a b
f forall k (f :: k -> k -> *) (a :: k). Queue f a a
nilQ

mapArr :: f b c
       -> Arr f a b
       -> Arr f a c
mapArr :: forall (f :: * -> * -> *) b c a. f b c -> Arr f a b -> Arr f a c
mapArr f b c
bc Arr f a b
ac = forall (f :: * -> * -> *) a c a.
f a c -> Queue (Arr f) a a -> Arr f a c
Cons f b c
bc forall k (f :: k -> k -> *) (a :: k). Queue f a a
nilQ forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Arr f a b
ac

foldArr :: forall f arr a b.
           Arrow arr
        => (forall x y. f x y -> arr x y)
        -> Arr f a b
        -> arr a b
foldArr :: forall (f :: * -> * -> *) (arr :: * -> * -> *) a b.
Arrow arr =>
(forall x y. f x y -> arr x y) -> Arr f a b -> arr a b
foldArr forall x y. f x y -> arr x y
_   Arr f a b
Id = forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id
foldArr forall x y. f x y -> arr x y
fun (Cons f b b
bc Queue (Arr f) a b
ab) = forall x y. f x y -> arr x y
fun f b b
bc forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall k (f :: k -> k -> *) (c :: k -> k -> *) (a :: k) (b :: k).
Category c =>
(forall (x :: k) (y :: k). f x y -> c x y) -> Queue f a b -> c a b
foldNatQ (forall k (m :: (k -> k -> *) -> k -> k -> *) (d :: k -> k -> *)
       (f :: k -> k -> *) (a :: k) (b :: k).
(FreeAlgebra2 m, AlgebraType m d, AlgebraType0 m f) =>
(forall (x :: k) (y :: k). f x y -> d x y) -> m f a b -> d a b
foldNatFree2 forall x y. f x y -> arr x y
fun) Queue (Arr f) a b
ab
foldArr forall x y. f x y -> arr x y
fun (Arr b -> b
f Arr f a b
g)    = forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr b -> b
f  forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall k (m :: (k -> k -> *) -> k -> k -> *) (d :: k -> k -> *)
       (f :: k -> k -> *) (a :: k) (b :: k).
(FreeAlgebra2 m, AlgebraType m d, AlgebraType0 m f) =>
(forall (x :: k) (y :: k). f x y -> d x y) -> m f a b -> d a b
foldNatFree2 forall x y. f x y -> arr x y
fun Arr f a b
g
foldArr forall x y. f x y -> arr x y
fun (Prod Arr f a b
f Arr f a c
g)   = forall k (m :: (k -> k -> *) -> k -> k -> *) (d :: k -> k -> *)
       (f :: k -> k -> *) (a :: k) (b :: k).
(FreeAlgebra2 m, AlgebraType m d, AlgebraType0 m f) =>
(forall (x :: k) (y :: k). f x y -> d x y) -> m f a b -> d a b
foldNatFree2 forall x y. f x y -> arr x y
fun Arr f a b
f forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& forall k (m :: (k -> k -> *) -> k -> k -> *) (d :: k -> k -> *)
       (f :: k -> k -> *) (a :: k) (b :: k).
(FreeAlgebra2 m, AlgebraType m d, AlgebraType0 m f) =>
(forall (x :: k) (y :: k). f x y -> d x y) -> m f a b -> d a b
foldNatFree2 forall x y. f x y -> arr x y
fun Arr f a c
g

instance Category (Arr f) where
  id :: forall a. Arr f a a
id = forall (f :: * -> * -> *) a. Arr f a a
Id
  Arr f b c
Id         . :: forall b c a. Arr f b c -> Arr f a b -> Arr f a c
. Arr f a b
f  = Arr f a b
f
  Arr f b c
f          . Arr f a b
Id = Arr f b c
f
  (Cons f b c
f Queue (Arr f) b b
g) . Arr f a b
h  = forall (f :: * -> * -> *) a c a.
f a c -> Queue (Arr f) a a -> Arr f a c
Cons f b c
f (Queue (Arr f) b b
g forall k (f :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Queue f b c -> f a b -> Queue f a c
`snocQ` Arr f a b
h)
  (Arr b -> c
f Arr f b b
g)  . Arr f a b
h  = forall a c (f :: * -> * -> *) a. (a -> c) -> Arr f a a -> Arr f a c
Arr b -> c
f (Arr f b b
g forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Arr f a b
h)
  (Prod Arr f b b
f Arr f b c
g) . Arr f a b
h  = forall (f :: * -> * -> *) a a b.
Arr f a a -> Arr f a b -> Arr f a (a, b)
Prod (Arr f b b
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Arr f a b
h) (Arr f b c
g forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Arr f a b
h)

instance Semigroup (Arr f o o) where
    Arr f o o
f <> :: Arr f o o -> Arr f o o -> Arr f o o
<> Arr f o o
g = Arr f o o
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. Arr f o o
g

instance Monoid (Arr f o o) where
    mempty :: Arr f o o
mempty = forall (f :: * -> * -> *) a. Arr f a a
Id

instance Arrow (Arr f) where
  arr :: forall b c. (b -> c) -> Arr f b c
arr       = forall b c (f :: * -> * -> *). (b -> c) -> Arr f b c
arrArr
  first :: forall b c d. Arr f b c -> Arr f (b, d) (c, d)
first Arr f b c
bc  = forall (f :: * -> * -> *) a a b.
Arr f a a -> Arr f a b -> Arr f a (a, b)
Prod (Arr f b c
bc forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a b. (a, b) -> a
fst) (forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a b. (a, b) -> b
snd)
  second :: forall b c d. Arr f b c -> Arr f (d, b) (d, c)
second Arr f b c
bc = forall (f :: * -> * -> *) a a b.
Arr f a a -> Arr f a b -> Arr f a (a, b)
Prod (forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a b. (a, b) -> a
fst) (Arr f b c
bc forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a b. (a, b) -> b
snd)
  Arr f b c
ab *** :: forall b c b' c'. Arr f b c -> Arr f b' c' -> Arr f (b, b') (c, c')
*** Arr f b' c'
xy = forall (f :: * -> * -> *) a a b.
Arr f a a -> Arr f a b -> Arr f a (a, b)
Prod (Arr f b c
ab forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a b. (a, b) -> a
fst) (Arr f b' c'
xy forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a b. (a, b) -> b
snd)
  &&& :: forall b c c'. Arr f b c -> Arr f b c' -> Arr f b (c, c')
(&&&)     = forall (f :: * -> * -> *) a a b.
Arr f a a -> Arr f a b -> Arr f a (a, b)
Prod

type instance AlgebraType0 Arr f = ()
type instance AlgebraType  Arr c = Arrow c

instance FreeAlgebra2 Arr where
  liftFree2 :: forall (f :: * -> * -> *) a b.
AlgebraType0 Arr f =>
f a b -> Arr f a b
liftFree2 = \f a b
fab -> forall (f :: * -> * -> *) a c a.
f a c -> Queue (Arr f) a a -> Arr f a c
Cons f a b
fab forall k (f :: k -> k -> *) (a :: k). Queue f a a
nilQ
  {-# INLINE liftFree2 #-}

  foldNatFree2 :: forall (d :: * -> * -> *) (f :: * -> * -> *) a b.
(AlgebraType Arr d, AlgebraType0 Arr f) =>
(forall x y. f x y -> d x y) -> Arr f a b -> d a b
foldNatFree2 = forall (f :: * -> * -> *) (arr :: * -> * -> *) a b.
Arrow arr =>
(forall x y. f x y -> arr x y) -> Arr f a b -> arr a b
foldArr
  {-# INLINE foldNatFree2 #-}

  codom2 :: forall (f :: * -> * -> *).
AlgebraType0 Arr f =>
Proof (AlgebraType Arr (Arr f)) (Arr f)
codom2  = forall {l} (c :: Constraint) (a :: l). c => Proof c a
Proof
  forget2 :: forall (f :: * -> * -> *).
AlgebraType Arr f =>
Proof (AlgebraType0 Arr f) (Arr f)
forget2 = forall {l} (c :: Constraint) (a :: l). c => Proof c a
Proof

--
-- Free arrows using CSP style
--

-- | Free arrow using CPS style.
--
newtype A f a b
  = A { forall (f :: * -> * -> *) a b.
A f a b
-> forall (r :: * -> * -> *).
   Arrow r =>
   (forall x y. f x y -> r x y) -> r a b
runA :: forall r. Arrow r
             => (forall x y. f x y -> r x y)
             -> r a b
      }

-- | Isomorphism from @'Arr'@ to @'A'@, which is a specialisation of
-- @'hoistFreeH2'@.
--
toA :: Arr f a b -> A f a b
toA :: forall (f :: * -> * -> *) a b. Arr f a b -> A f a b
toA = forall {k} (m :: (k -> k -> *) -> k -> k -> *)
       (n :: (k -> k -> *) -> k -> k -> *) (f :: k -> k -> *) (a :: k)
       (b :: k).
(FreeAlgebra2 m, FreeAlgebra2 n, AlgebraType0 m f,
 AlgebraType0 n f, AlgebraType m (n f)) =>
m f a b -> n f a b
hoistFreeH2
{-# INLINE toA #-}

-- | Inverse of @'fromA'@, which also is a specialisation of @'hoistFreeH2'@.
--
fromA :: A f a b -> Arr f a b
fromA :: forall (f :: * -> * -> *) a b. A f a b -> Arr f a b
fromA = forall {k} (m :: (k -> k -> *) -> k -> k -> *)
       (n :: (k -> k -> *) -> k -> k -> *) (f :: k -> k -> *) (a :: k)
       (b :: k).
(FreeAlgebra2 m, FreeAlgebra2 n, AlgebraType0 m f,
 AlgebraType0 n f, AlgebraType m (n f)) =>
m f a b -> n f a b
hoistFreeH2
{-# INLINE fromA #-}

instance Category (A f) where
  id :: forall a. A f a a
id = forall (f :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r a b)
-> A f a b
A (\forall x y. f x y -> r x y
_ -> forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id)
  A forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b c
f . :: forall b c a. A f b c -> A f a b -> A f a c
. A forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r a b
g = forall (f :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r a b)
-> A f a b
A forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b c
f forall x y. f x y -> r x y
k forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r a b
g forall x y. f x y -> r x y
k

instance Semigroup (A f o o) where
    A f o o
f <> :: A f o o -> A f o o -> A f o o
<> A f o o
g = A f o o
f forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. A f o o
g

instance Monoid (A f o o) where
    mempty :: A f o o
mempty = forall {k} (cat :: k -> k -> *) (a :: k). Category cat => cat a a
id

instance Arrow (A f) where
  arr :: forall b c. (b -> c) -> A f b c
arr b -> c
f = forall (f :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r a b)
-> A f a b
A (\forall x y. f x y -> r x y
_ -> (forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr b -> c
f))
  A forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b c
f *** :: forall b c b' c'. A f b c -> A f b' c' -> A f (b, b') (c, c')
*** A forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b' c'
g  = forall (f :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r a b)
-> A f a b
A forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b c
f forall x y. f x y -> r x y
k forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b' c'
g forall x y. f x y -> r x y
k
  first :: forall b c d. A f b c -> A f (b, d) (c, d)
first  (A forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b c
f) = forall (f :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r a b)
-> A f a b
A forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first (forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b c
f forall x y. f x y -> r x y
k)
  second :: forall b c d. A f b c -> A f (d, b) (d, c)
second (A forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b c
f) = forall (f :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r a b)
-> A f a b
A forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r b c
f forall x y. f x y -> r x y
k)

type instance AlgebraType0 A f = ()
type instance AlgebraType  A c = Arrow c

instance FreeAlgebra2 A where
  liftFree2 :: forall (f :: * -> * -> *) a b. AlgebraType0 A f => f a b -> A f a b
liftFree2 = \f a b
fab -> forall (f :: * -> * -> *) a b.
(forall (r :: * -> * -> *).
 Arrow r =>
 (forall x y. f x y -> r x y) -> r a b)
-> A f a b
A forall a b. (a -> b) -> a -> b
$ \forall x y. f x y -> r x y
k -> forall x y. f x y -> r x y
k f a b
fab
  {-# INLINE liftFree2 #-}

  foldNatFree2 :: forall (d :: * -> * -> *) (f :: * -> * -> *) a b.
(AlgebraType A d, AlgebraType0 A f) =>
(forall x y. f x y -> d x y) -> A f a b -> d a b
foldNatFree2 forall x y. f x y -> d x y
fun (A forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r a b
f) = forall (r :: * -> * -> *).
Arrow r =>
(forall x y. f x y -> r x y) -> r a b
f forall x y. f x y -> d x y
fun
  {-# INLINE foldNatFree2 #-}

  codom2 :: forall (f :: * -> * -> *).
AlgebraType0 A f =>
Proof (AlgebraType A (A f)) (A f)
codom2  = forall {l} (c :: Constraint) (a :: l). c => Proof c a
Proof
  forget2 :: forall (f :: * -> * -> *).
AlgebraType A f =>
Proof (AlgebraType0 A f) (A f)
forget2 = forall {l} (c :: Constraint) (a :: l). c => Proof c a
Proof

data Choice f a b where
  NoChoice :: f a b
           -> Choice f a b

  Choose   :: ArrChoice f a c
           -> ArrChoice f b c
           -> Choice f (Either a b) c

type ArrChoice f a b = Arr (Choice f) a b

instance ArrowChoice (Arr (Choice f)) where
  Arr (Choice f) b c
f +++ :: forall b c b' c'.
Arr (Choice f) b c
-> Arr (Choice f) b' c'
-> Arr (Choice f) (Either b b') (Either c c')
+++ Arr (Choice f) b' c'
g = forall (f :: * -> * -> *) a b. f a b -> Arr f a b
liftArr forall a b. (a -> b) -> a -> b
$ forall (f :: * -> * -> *) a c b.
ArrChoice f a c -> ArrChoice f b c -> Choice f (Either a b) c
Choose (Arr (Choice f) b c
f forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a b. a -> Either a b
Left) (Arr (Choice f) b' c'
g forall {k} (cat :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Category cat =>
cat a b -> cat b c -> cat a c
>>> forall (a :: * -> * -> *) b c. Arrow a => (b -> c) -> a b c
arr forall a b. b -> Either a b
Right)

liftArrChoice :: f a b
              -> ArrChoice f a b
liftArrChoice :: forall (f :: * -> * -> *) a b. f a b -> ArrChoice f a b
liftArrChoice = forall (f :: * -> * -> *) a b. f a b -> Arr f a b
liftArr forall {k} (cat :: k -> k -> *) (b :: k) (c :: k) (a :: k).
Category cat =>
cat b c -> cat a b -> cat a c
. forall (f :: * -> * -> *) a b. f a b -> Choice f a b
NoChoice

foldArrChoice :: forall f arr a b.
                 ArrowChoice arr
              => (forall x y. f x y -> arr x y)
              -> ArrChoice f a b
              -> arr a b
foldArrChoice :: forall (f :: * -> * -> *) (arr :: * -> * -> *) a b.
ArrowChoice arr =>
(forall x y. f x y -> arr x y) -> ArrChoice f a b -> arr a b
foldArrChoice forall x y. f x y -> arr x y
fun = forall (f :: * -> * -> *) (arr :: * -> * -> *) a b.
Arrow arr =>
(forall x y. f x y -> arr x y) -> Arr f a b -> arr a b
foldArr forall x y. Choice f x y -> arr x y
fun'
  where
    fun' :: Choice f x y -> arr x y
    fun' :: forall x y. Choice f x y -> arr x y
fun' (NoChoice f x y
f) = forall x y. f x y -> arr x y
fun f x y
f
    fun' (Choose ArrChoice f a y
f ArrChoice f b y
g) = forall (f :: * -> * -> *) (arr :: * -> * -> *) a b.
ArrowChoice arr =>
(forall x y. f x y -> arr x y) -> ArrChoice f a b -> arr a b
foldArrChoice forall x y. f x y -> arr x y
fun ArrChoice f a y
f forall (a :: * -> * -> *) b d c.
ArrowChoice a =>
a b d -> a c d -> a (Either b c) d
||| forall (f :: * -> * -> *) (arr :: * -> * -> *) a b.
ArrowChoice arr =>
(forall x y. f x y -> arr x y) -> ArrChoice f a b -> arr a b
foldArrChoice forall x y. f x y -> arr x y
fun ArrChoice f b y
g