{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE DeriveDataTypeable   #-}
{-# LANGUAGE DeriveGeneric        #-}
{-# LANGUAGE LambdaCase           #-}
{-# LANGUAGE PolyKinds            #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE ScopedTypeVariables  #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

{-# OPTIONS_GHC -Wall -Wno-name-shadowing #-}

module Data.IFunctor.Foldable
    (
    -- * Fixpoint for indexed types
      IFix (..)
    -- * Morphisms
    -- * Constructive morphisms
    , cata
    , prepro
    , para
    , zygo
    , histo
    -- * Destructive morphisms
    , ana
    , postpro
    , apo
    , gapo
    , futu
    -- * Combined morphisms
    , hylo
    , dyna
    , chrono
    , meta
    , elgot
    , coelgot
    -- * Monadic morphisms
    , cataM
    , paraM
    , anaM
    , apoM
    , hyloM
    , dynaM
    -- * Distribution Laws
    , DistLaw
    -- * Constructive distribution laws
    , distCata
    , distPara
    , distZygo
    , distHisto
    -- * Destructive distribution laws
    , distAna
    , distApo
    , distGApo
    , distFutu
    -- * Generalized morphisms
    , gfold
    , gunfold
    , ghylo
    , gprepro
    , gpostpro
    -- * Generalized monadic morphisms
    , gfoldM
    , gunfoldM
    , ghyloM
    -- * Re-exports
    , module Data.Functor.Const
    , module Data.Functor.Product
    , module Data.Functor.Sum
    , module Data.IComonad
    , module Data.IFunction
    , module Data.IFunctor
    , module Data.IFunctor.Classes
    , module Data.IFunctor.ICofree
    , module Data.IFunctor.IFree
    , module Data.IFunctor.IIdentity
    , module Data.IMonad
    , module Data.ITraversable
    , module Singlethongs
    ) where

import           Control.Monad           ((<=<))
import           Data.Functor.Const      (Const (..))
import           Data.Functor.Product    (Product (..))
import           Data.Functor.Sum        (Sum (..))
import           Data.IComonad           (IComonad (..))
import           Data.IFunction          (type (~~>))
import           Data.IFunctor           (IFunctor (..))
import           Data.IFunctor.Classes
import           Data.IFunctor.ICofree   (ICofree (..))
import           Data.IFunctor.IFree     (IFree (..))
import           Data.IFunctor.IIdentity (IIdentity (..))
import           Data.IMonad             (IMonad (..))
import           Data.ITraversable       (ITraversable (..), imapDefault)
import           Data.Typeable           (Typeable)
import           GHC.Generics            (Generic, Generic1)
import           Singlethongs            (SingI (sing))
import           Text.Read

-- | Fixpoint type
newtype IFix f ix = IFix { IFix f ix -> f (IFix f) ix
unIFix :: f (IFix f) ix }
    deriving (Typeable, (forall x. IFix f ix -> Rep (IFix f ix) x)
-> (forall x. Rep (IFix f ix) x -> IFix f ix)
-> Generic (IFix f ix)
forall x. Rep (IFix f ix) x -> IFix f ix
forall x. IFix f ix -> Rep (IFix f ix) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (f :: (k -> *) -> k -> *) (ix :: k) x.
Rep (IFix f ix) x -> IFix f ix
forall k (f :: (k -> *) -> k -> *) (ix :: k) x.
IFix f ix -> Rep (IFix f ix) x
$cto :: forall k (f :: (k -> *) -> k -> *) (ix :: k) x.
Rep (IFix f ix) x -> IFix f ix
$cfrom :: forall k (f :: (k -> *) -> k -> *) (ix :: k) x.
IFix f ix -> Rep (IFix f ix) x
Generic, (forall (a :: k). IFix f a -> Rep1 (IFix f) a)
-> (forall (a :: k). Rep1 (IFix f) a -> IFix f a)
-> Generic1 (IFix f)
forall (a :: k). Rep1 (IFix f) a -> IFix f a
forall (a :: k). IFix f a -> Rep1 (IFix f) a
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
forall k (f :: (k -> *) -> k -> *) (a :: k).
Rep1 (IFix f) a -> IFix f a
forall k (f :: (k -> *) -> k -> *) (a :: k).
IFix f a -> Rep1 (IFix f) a
$cto1 :: forall k (f :: (k -> *) -> k -> *) (a :: k).
Rep1 (IFix f) a -> IFix f a
$cfrom1 :: forall k (f :: (k -> *) -> k -> *) (a :: k).
IFix f a -> Rep1 (IFix f) a
Generic1)

instance (IShow f, SingI ix) => Show (IFix f ix) where
    showsPrec :: Int -> IFix f ix -> ShowS
showsPrec p :: Int
p (IFix x :: f (IFix f) ix
x) = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$
        String -> ShowS
showString "IFix " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
.  (forall (ix :: k). SingI ix => Int -> IFix f ix -> ShowS)
-> Int -> f (IFix f) ix -> ShowS
forall k k (f :: (k -> *) -> k -> *) (ix :: k) (a :: k -> *).
(IShow f, SingI ix) =>
(forall (ix :: k). SingI ix => Int -> a ix -> ShowS)
-> Int -> f a ix -> ShowS
ishowsPrec forall (ix :: k). SingI ix => Int -> IFix f ix -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec 11 f (IFix f) ix
x

instance (IRead f, SingI ix) => Read (IFix f ix) where
    readPrec :: ReadPrec (IFix f ix)
readPrec = ReadPrec (IFix f ix) -> ReadPrec (IFix f ix)
forall a. ReadPrec a -> ReadPrec a
parens (ReadPrec (IFix f ix) -> ReadPrec (IFix f ix))
-> ReadPrec (IFix f ix) -> ReadPrec (IFix f ix)
forall a b. (a -> b) -> a -> b
$ Int -> ReadPrec (IFix f ix) -> ReadPrec (IFix f ix)
forall a. Int -> ReadPrec a -> ReadPrec a
prec 10 (ReadPrec (IFix f ix) -> ReadPrec (IFix f ix))
-> ReadPrec (IFix f ix) -> ReadPrec (IFix f ix)
forall a b. (a -> b) -> a -> b
$ do
        Ident "IFix" <- ReadPrec Lexeme
lexP
        f (IFix f) ix
x <- ReadPrec (f (IFix f) ix) -> ReadPrec (f (IFix f) ix)
forall a. ReadPrec a -> ReadPrec a
step (ReadPrec (f (IFix f) ix) -> ReadPrec (f (IFix f) ix))
-> ReadPrec (f (IFix f) ix) -> ReadPrec (f (IFix f) ix)
forall a b. (a -> b) -> a -> b
$ (forall (ix :: k). SingI ix => ReadPrec (IFix f ix))
-> ReadPrec (f (IFix f) ix)
forall k k (f :: (k -> *) -> k -> *) (ix :: k) (a :: k -> *).
(IRead f, SingI ix) =>
(forall (ix :: k). SingI ix => ReadPrec (a ix))
-> ReadPrec (f a ix)
ireadPrec forall (ix :: k). SingI ix => ReadPrec (IFix f ix)
forall a. Read a => ReadPrec a
readPrec
        IFix f ix -> ReadPrec (IFix f ix)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IFix f ix -> ReadPrec (IFix f ix))
-> IFix f ix -> ReadPrec (IFix f ix)
forall a b. (a -> b) -> a -> b
$ f (IFix f) ix -> IFix f ix
forall k (f :: (k -> *) -> k -> *) (ix :: k).
f (IFix f) ix -> IFix f ix
IFix f (IFix f) ix
x

instance (IEq f, SingI ix) => Eq (IFix f ix) where
    IFix x :: f (IFix f) ix
x == :: IFix f ix -> IFix f ix -> Bool
== IFix y :: f (IFix f) ix
y = (forall (ix :: k). SingI ix => IFix f ix -> IFix f ix -> Bool)
-> f (IFix f) ix -> f (IFix f) ix -> Bool
forall k k (f :: (k -> *) -> k -> *) (ix :: k) (a :: k -> *).
(IEq f, SingI ix) =>
(forall (ix :: k). SingI ix => a ix -> a ix -> Bool)
-> f a ix -> f a ix -> Bool
ieq forall (ix :: k). SingI ix => IFix f ix -> IFix f ix -> Bool
forall a. Eq a => a -> a -> Bool
(==) f (IFix f) ix
x f (IFix f) ix
y

instance (IOrd f, SingI ix) => Ord (IFix f ix) where
    IFix x :: f (IFix f) ix
x compare :: IFix f ix -> IFix f ix -> Ordering
`compare` IFix y :: f (IFix f) ix
y = (forall (ix :: k). SingI ix => IFix f ix -> IFix f ix -> Ordering)
-> f (IFix f) ix -> f (IFix f) ix -> Ordering
forall k k (f :: (k -> *) -> k -> *) (ix :: k) (a :: k -> *).
(IOrd f, SingI ix) =>
(forall (ix :: k). SingI ix => a ix -> a ix -> Ordering)
-> f a ix -> f a ix -> Ordering
icompare forall (ix :: k). SingI ix => IFix f ix -> IFix f ix -> Ordering
forall a. Ord a => a -> a -> Ordering
compare f (IFix f) ix
x f (IFix f) ix
y

-- * Morphisms

-- | Catamorphism, ie. fold
cata :: IFunctor f
     => (f a ~~> a)
     -> (IFix f ~~> a)
cata :: (f a ~~> a) -> IFix f ~~> a
cata f :: f a ~~> a
f = DistLaw f IIdentity -> (f (IIdentity a) ~~> a) -> IFix f ~~> a
forall k (f :: (k -> *) -> k -> *) (w :: (k -> *) -> k -> *)
       (a :: k -> *).
(IFunctor f, IComonad w) =>
DistLaw f w -> (f (w a) ~~> a) -> IFix f ~~> a
gfold forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw f IIdentity
DistLaw f IIdentity
distCata (f a ix -> a ix
f a ~~> a
f (f a ix -> a ix)
-> (f (IIdentity a) ix -> f a ix) -> f (IIdentity a) ix -> a ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IIdentity a ~~> a) -> f (IIdentity a) ~~> f a
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap IIdentity a ~~> a
forall k (f :: k -> *) (ix :: k). IIdentity f ix -> f ix
runIIdentity)

-- | Fokkinga's prepromorphism
prepro :: IFunctor f
       => (forall b. f b ~~> f b)
       -> (f a ~~> a)
       -> (IFix f ~~> a)
prepro :: (forall (b :: k -> *). f b ~~> f b) -> (f a ~~> a) -> IFix f ~~> a
prepro e :: forall (b :: k -> *). f b ~~> f b
e f :: f a ~~> a
f = DistLaw f IIdentity
-> (forall (b :: k -> *). f b ~~> f b)
-> (f (IIdentity a) ~~> a)
-> IFix f ~~> a
forall k (f :: (k -> *) -> k -> *) (w :: (k -> *) -> k -> *)
       (a :: k -> *).
(IFunctor f, IComonad w) =>
DistLaw f w
-> (forall (c :: k -> *). f c ~~> f c)
-> (f (w a) ~~> a)
-> IFix f ~~> a
gprepro forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw f IIdentity
DistLaw f IIdentity
distCata forall (b :: k -> *). f b ~~> f b
e (f a ix -> a ix
f a ~~> a
f (f a ix -> a ix)
-> (f (IIdentity a) ix -> f a ix) -> f (IIdentity a) ix -> a ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IIdentity a ~~> a) -> f (IIdentity a) ~~> f a
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap IIdentity a ~~> a
forall k (f :: k -> *) (ix :: k). IIdentity f ix -> f ix
runIIdentity)

-- | Paramorphism
para :: IFunctor f
     => (f (Product (IFix f) a) ~~> a)
     -> (IFix f ~~> a)
para :: (f (Product (IFix f) a) ~~> a) -> IFix f ~~> a
para = DistLaw f (Product (IFix f))
-> (f (Product (IFix f) a) ~~> a) -> IFix f ~~> a
forall k (f :: (k -> *) -> k -> *) (w :: (k -> *) -> k -> *)
       (a :: k -> *).
(IFunctor f, IComonad w) =>
DistLaw f w -> (f (w a) ~~> a) -> IFix f ~~> a
gfold forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw f (Product (IFix f))
DistLaw f (Product (IFix f))
distPara

-- | Zygomorphism
zygo :: IFunctor f
     => (f b ~~> b)
     -> (f (Product b a) ~~> a)
     -> (IFix f ~~> a)
zygo :: (f b ~~> b) -> (f (Product b a) ~~> a) -> IFix f ~~> a
zygo f :: f b ~~> b
f = DistLaw f (Product b) -> (f (Product b a) ~~> a) -> IFix f ~~> a
forall k (f :: (k -> *) -> k -> *) (w :: (k -> *) -> k -> *)
       (a :: k -> *).
(IFunctor f, IComonad w) =>
DistLaw f w -> (f (w a) ~~> a) -> IFix f ~~> a
gfold ((f b ~~> b) -> DistLaw f (Product b)
forall k (f :: (k -> *) -> k -> *) (b :: k -> *).
IFunctor f =>
(f b ~~> b) -> DistLaw f (Product b)
distZygo f b ~~> b
f)

-- | Histomorphism
histo :: IFunctor f
      => (f (ICofree f a) ~~> a)
      -> (IFix f ~~> a)
histo :: (f (ICofree f a) ~~> a) -> IFix f ~~> a
histo = DistLaw f (ICofree f) -> (f (ICofree f a) ~~> a) -> IFix f ~~> a
forall k (f :: (k -> *) -> k -> *) (w :: (k -> *) -> k -> *)
       (a :: k -> *).
(IFunctor f, IComonad w) =>
DistLaw f w -> (f (w a) ~~> a) -> IFix f ~~> a
gfold forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw f (ICofree f)
DistLaw f (ICofree f)
distHisto

-- | Anamorphism, ie. unfold
ana :: IFunctor f
    => (a ~~> f a)
    -> (a ~~> IFix f)
ana :: (a ~~> f a) -> a ~~> IFix f
ana g :: a ~~> f a
g = DistLaw IIdentity f -> (a ~~> f (IIdentity a)) -> a ~~> IFix f
forall k (f :: (k -> *) -> k -> *) (m :: (k -> *) -> k -> *)
       (a :: k -> *).
(IFunctor f, IMonad m) =>
DistLaw m f -> (a ~~> f (m a)) -> a ~~> IFix f
gunfold forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw IIdentity f
DistLaw IIdentity f
distAna ((a ~~> IIdentity a) -> f a ~~> f (IIdentity a)
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap a ~~> IIdentity a
forall k (f :: k -> *) (ix :: k). f ix -> IIdentity f ix
IIdentity (f a ix -> f (IIdentity a) ix)
-> (a ix -> f a ix) -> a ix -> f (IIdentity a) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a ix -> f a ix
a ~~> f a
g)

-- | Fokkinga's postpromorphism
postpro :: IFunctor f
        => (forall b. f b ~~> f b)
        -> (a ~~> f a)
        -> (a ~~> IFix f)
postpro :: (forall (b :: k -> *). f b ~~> f b) -> (a ~~> f a) -> a ~~> IFix f
postpro e :: forall (b :: k -> *). f b ~~> f b
e g :: a ~~> f a
g = DistLaw IIdentity f
-> (forall (b :: k -> *). f b ~~> f b)
-> (a ~~> f (IIdentity a))
-> a ~~> IFix f
forall k (f :: (k -> *) -> k -> *) (m :: (k -> *) -> k -> *)
       (a :: k -> *).
(IFunctor f, IMonad m) =>
DistLaw m f
-> (forall (c :: k -> *). f c ~~> f c)
-> (a ~~> f (m a))
-> a ~~> IFix f
gpostpro forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw IIdentity f
DistLaw IIdentity f
distAna forall (b :: k -> *). f b ~~> f b
e ((a ~~> IIdentity a) -> f a ~~> f (IIdentity a)
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap a ~~> IIdentity a
forall k (f :: k -> *) (ix :: k). f ix -> IIdentity f ix
IIdentity (f a ix -> f (IIdentity a) ix)
-> (a ix -> f a ix) -> a ix -> f (IIdentity a) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a ix -> f a ix
a ~~> f a
g)

-- | Apomorphism
apo :: IFunctor f
    => (a ~~> f (Sum (IFix f) a))
    -> (a ~~> IFix f)
apo :: (a ~~> f (Sum (IFix f) a)) -> a ~~> IFix f
apo = DistLaw (Sum (IFix f)) f
-> (a ~~> f (Sum (IFix f) a)) -> a ~~> IFix f
forall k (f :: (k -> *) -> k -> *) (m :: (k -> *) -> k -> *)
       (a :: k -> *).
(IFunctor f, IMonad m) =>
DistLaw m f -> (a ~~> f (m a)) -> a ~~> IFix f
gunfold forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw (Sum (IFix f)) f
DistLaw (Sum (IFix f)) f
distApo

-- | GApomorphism
gapo :: IFunctor f
     => (b ~~> f b)
     -> (a ~~> f (Sum b a))
     -> (a ~~> IFix f)
gapo :: (b ~~> f b) -> (a ~~> f (Sum b a)) -> a ~~> IFix f
gapo f :: b ~~> f b
f = DistLaw (Sum b) f -> (a ~~> f (Sum b a)) -> a ~~> IFix f
forall k (f :: (k -> *) -> k -> *) (m :: (k -> *) -> k -> *)
       (a :: k -> *).
(IFunctor f, IMonad m) =>
DistLaw m f -> (a ~~> f (m a)) -> a ~~> IFix f
gunfold ((b ~~> f b) -> DistLaw (Sum b) f
forall k (f :: (k -> *) -> k -> *) (b :: k -> *).
IFunctor f =>
(b ~~> f b) -> DistLaw (Sum b) f
distGApo b ~~> f b
f)

-- | Futumorphism
futu :: IFunctor f
     => (a ~~> f (IFree f a))
     -> (a ~~> IFix f)
futu :: (a ~~> f (IFree f a)) -> a ~~> IFix f
futu = DistLaw (IFree f) f -> (a ~~> f (IFree f a)) -> a ~~> IFix f
forall k (f :: (k -> *) -> k -> *) (m :: (k -> *) -> k -> *)
       (a :: k -> *).
(IFunctor f, IMonad m) =>
DistLaw m f -> (a ~~> f (m a)) -> a ~~> IFix f
gunfold forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw (IFree f) f
DistLaw (IFree f) f
distFutu

-- | Hylomorphism, fold then unfold
hylo :: IFunctor f
     => (f b ~~> b)
     -> (a ~~> f a)
     -> (a ~~> b)
hylo :: (f b ~~> b) -> (a ~~> f a) -> a ~~> b
hylo f :: f b ~~> b
f g :: a ~~> f a
g = DistLaw f IIdentity
-> DistLaw IIdentity f
-> (f (IIdentity b) ~~> b)
-> (a ~~> f (IIdentity a))
-> a ~~> b
forall k (f :: (k -> *) -> k -> *) (w :: (k -> *) -> k -> *)
       (m :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
(IFunctor f, IComonad w, IMonad m) =>
DistLaw f w
-> DistLaw m f -> (f (w b) ~~> b) -> (a ~~> f (m a)) -> a ~~> b
ghylo forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw f IIdentity
DistLaw f IIdentity
distCata forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw IIdentity f
DistLaw IIdentity f
distAna (f b ix -> b ix
f b ~~> b
f (f b ix -> b ix)
-> (f (IIdentity b) ix -> f b ix) -> f (IIdentity b) ix -> b ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IIdentity b ~~> b) -> f (IIdentity b) ~~> f b
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap IIdentity b ~~> b
forall k (f :: k -> *) (ix :: k). IIdentity f ix -> f ix
runIIdentity) ((a ~~> IIdentity a) -> f a ~~> f (IIdentity a)
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap a ~~> IIdentity a
forall k (f :: k -> *) (ix :: k). f ix -> IIdentity f ix
IIdentity (f a ix -> f (IIdentity a) ix)
-> (a ix -> f a ix) -> a ix -> f (IIdentity a) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a ix -> f a ix
a ~~> f a
g)

-- | Dynamorphism
dyna :: IFunctor f
     => (f (ICofree f b) ~~> b)
     -> (a ~~> f a)
     -> (a ~~> b)
dyna :: (f (ICofree f b) ~~> b) -> (a ~~> f a) -> a ~~> b
dyna f :: f (ICofree f b) ~~> b
f g :: a ~~> f a
g = DistLaw f (ICofree f)
-> DistLaw IIdentity f
-> (f (ICofree f b) ~~> b)
-> (a ~~> f (IIdentity a))
-> a ~~> b
forall k (f :: (k -> *) -> k -> *) (w :: (k -> *) -> k -> *)
       (m :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
(IFunctor f, IComonad w, IMonad m) =>
DistLaw f w
-> DistLaw m f -> (f (w b) ~~> b) -> (a ~~> f (m a)) -> a ~~> b
ghylo forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw f (ICofree f)
DistLaw f (ICofree f)
distHisto forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw IIdentity f
DistLaw IIdentity f
distAna f (ICofree f b) ~~> b
f ((a ~~> IIdentity a) -> f a ~~> f (IIdentity a)
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap a ~~> IIdentity a
forall k (f :: k -> *) (ix :: k). f ix -> IIdentity f ix
IIdentity (f a ix -> f (IIdentity a) ix)
-> (a ix -> f a ix) -> a ix -> f (IIdentity a) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a ix -> f a ix
a ~~> f a
g)

-- | Chronomorphism
chrono :: IFunctor f
       => (f (ICofree f b) ~~> b)
       -> (a ~~> f (IFree f a))
       -> (a ~~> b)
chrono :: (f (ICofree f b) ~~> b) -> (a ~~> f (IFree f a)) -> a ~~> b
chrono = DistLaw f (ICofree f)
-> DistLaw (IFree f) f
-> (f (ICofree f b) ~~> b)
-> (a ~~> f (IFree f a))
-> a ~~> b
forall k (f :: (k -> *) -> k -> *) (w :: (k -> *) -> k -> *)
       (m :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
(IFunctor f, IComonad w, IMonad m) =>
DistLaw f w
-> DistLaw m f -> (f (w b) ~~> b) -> (a ~~> f (m a)) -> a ~~> b
ghylo forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw f (ICofree f)
DistLaw f (ICofree f)
distHisto forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw (IFree f) f
DistLaw (IFree f) f
distFutu

-- | Metamorphism
-- TODO: ensure only 1 pass over structure
meta :: (IFunctor f, IFunctor g)
     => (f a ~~> a)
     -> (a ~~> b)
     -> (b ~~> g b)
     -> (IFix f ~~> IFix g)
meta :: (f a ~~> a) -> (a ~~> b) -> (b ~~> g b) -> IFix f ~~> IFix g
meta f :: f a ~~> a
f e :: a ~~> b
e g :: b ~~> g b
g = (b ~~> g b) -> b ~~> IFix g
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IFunctor f =>
(a ~~> f a) -> a ~~> IFix f
ana b ~~> g b
g (b ix -> IFix g ix)
-> (IFix f ix -> b ix) -> IFix f ix -> IFix g ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a ix -> b ix
a ~~> b
e (a ix -> b ix) -> (IFix f ix -> a ix) -> IFix f ix -> b ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f a ~~> a) -> IFix f ~~> a
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IFunctor f =>
(f a ~~> a) -> IFix f ~~> a
cata f a ~~> a
f

-- * Elgot algebras

elgot :: forall f a b. IFunctor f
      => (f a ~~> a)
      -> (b ~~> Sum a (f b))
      -> (b ~~> a)
elgot :: (f a ~~> a) -> (b ~~> Sum a (f b)) -> b ~~> a
elgot phi :: f a ~~> a
phi psi :: b ~~> Sum a (f b)
psi = b ix -> a ix
b ~~> a
h
    where
        h :: b ~~> a
        h :: b ix -> a ix
h = (forall (ix :: k). SingI ix => a ix -> a ix
forall a. a -> a
id (forall (ix :: k). SingI ix => a ix -> a ix)
-> (f b ~~> a) -> Sum a (f b) ~~> a
forall k (a :: k -> *) (b :: k -> *) (c :: k -> *).
(a ~~> c) -> (b ~~> c) -> Sum a b ~~> c
`sum` (f a ix -> a ix
f a ~~> a
phi (f a ix -> a ix) -> (f b ix -> f a ix) -> f b ix -> a ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b ~~> a) -> f b ~~> f a
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap b ~~> a
h)) (Sum a (f b) ix -> a ix)
-> (b ix -> Sum a (f b) ix) -> b ix -> a ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. b ix -> Sum a (f b) ix
b ~~> Sum a (f b)
psi
        sum :: forall a b c. (a ~~> c) -> (b ~~> c) -> (Sum a b ~~> c)
        sum :: (a ~~> c) -> (b ~~> c) -> Sum a b ~~> c
sum f :: a ~~> c
f _ (InL x :: a ix
x) = a ix -> c ix
a ~~> c
f a ix
x
        sum _ g :: b ~~> c
g (InR x :: b ix
x) = b ix -> c ix
b ~~> c
g b ix
x

coelgot :: forall f a b. IFunctor f
        => (Product a (f b) ~~> b)
        -> (a ~~> f a)
        -> (a ~~> b)
coelgot :: (Product a (f b) ~~> b) -> (a ~~> f a) -> a ~~> b
coelgot phi :: Product a (f b) ~~> b
phi psi :: a ~~> f a
psi = a ix -> b ix
a ~~> b
h
    where
        h :: a ~~> b
        h :: a ix -> b ix
h = Product a (f b) ix -> b ix
Product a (f b) ~~> b
phi (Product a (f b) ix -> b ix)
-> (a ix -> Product a (f b) ix) -> a ix -> b ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (ix :: k). SingI ix => a ix -> a ix
forall a. a -> a
id (forall (ix :: k). SingI ix => a ix -> a ix)
-> (a ~~> f b) -> a ~~> Product a (f b)
forall k (a :: k -> *) (b :: k -> *) (c :: k -> *).
(a ~~> b) -> (a ~~> c) -> a ~~> Product b c
`product` ((a ~~> b) -> f a ~~> f b
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap a ~~> b
h (f a ix -> f b ix) -> (a ix -> f a ix) -> a ix -> f b ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a ix -> f a ix
a ~~> f a
psi))
        product :: forall a b c. (a ~~> b) -> (a ~~> c) -> (a ~~> Product b c)
        product :: (a ~~> b) -> (a ~~> c) -> a ~~> Product b c
product f :: a ~~> b
f g :: a ~~> c
g x :: a ix
x = b ix -> c ix -> Product b c ix
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (a ix -> b ix
a ~~> b
f a ix
x) (a ix -> c ix
a ~~> c
g a ix
x)


-- * Monadic morphisms

-- | Monadic catamorphism
cataM :: (ITraversable f, Monad m)
      => (forall ix. SingI ix => f a ix -> m (a ix))
      -> (forall ix. SingI ix => IFix f ix -> m (a ix))
cataM :: (forall (ix :: k). SingI ix => f a ix -> m (a ix))
-> forall (ix :: k). SingI ix => IFix f ix -> m (a ix)
cataM f :: forall (ix :: k). SingI ix => f a ix -> m (a ix)
f = DistLaw f IIdentity
-> (forall (ix :: k). SingI ix => f (IIdentity a) ix -> m (a ix))
-> forall (ix :: k). SingI ix => IFix f ix -> m (a ix)
forall k (f :: (k -> *) -> k -> *) (w :: (k -> *) -> k -> *)
       (m :: * -> *) (a :: k -> *).
(ITraversable f, ITraversable w, IComonad w, Monad m) =>
DistLaw f w
-> (forall (ix :: k). SingI ix => f (w a) ix -> m (a ix))
-> forall (ix :: k). SingI ix => IFix f ix -> m (a ix)
gfoldM forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw f IIdentity
DistLaw f IIdentity
distCata (f a ix -> m (a ix)
forall (ix :: k). SingI ix => f a ix -> m (a ix)
f (f a ix -> m (a ix))
-> (f (IIdentity a) ix -> f a ix) -> f (IIdentity a) ix -> m (a ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IIdentity a ~~> a) -> f (IIdentity a) ~~> f a
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap IIdentity a ~~> a
forall k (f :: k -> *) (ix :: k). IIdentity f ix -> f ix
runIIdentity)

-- | Monadic Paramorphism
paraM :: (ITraversable f, Monad m)
      => (forall ix. SingI ix => f (Product (IFix f) a) ix -> m (a ix))
      -> (forall ix. SingI ix => IFix f ix -> m (a ix))
paraM :: (forall (ix :: k).
 SingI ix =>
 f (Product (IFix f) a) ix -> m (a ix))
-> forall (ix :: k). SingI ix => IFix f ix -> m (a ix)
paraM = DistLaw f (Product (IFix f))
-> (forall (ix :: k).
    SingI ix =>
    f (Product (IFix f) a) ix -> m (a ix))
-> forall (ix :: k). SingI ix => IFix f ix -> m (a ix)
forall k (f :: (k -> *) -> k -> *) (w :: (k -> *) -> k -> *)
       (m :: * -> *) (a :: k -> *).
(ITraversable f, ITraversable w, IComonad w, Monad m) =>
DistLaw f w
-> (forall (ix :: k). SingI ix => f (w a) ix -> m (a ix))
-> forall (ix :: k). SingI ix => IFix f ix -> m (a ix)
gfoldM forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw f (Product (IFix f))
DistLaw f (Product (IFix f))
distPara

-- | Monadic anamorphism
anaM :: (ITraversable f, Monad m)
     => (forall ix. SingI ix => a ix -> m (f a ix))
     -> (forall ix. SingI ix => a ix -> m (IFix f ix))
anaM :: (forall (ix :: k). SingI ix => a ix -> m (f a ix))
-> forall (ix :: k). SingI ix => a ix -> m (IFix f ix)
anaM g :: forall (ix :: k). SingI ix => a ix -> m (f a ix)
g = DistLaw IIdentity f
-> (forall (ix :: k). SingI ix => a ix -> m (f (IIdentity a) ix))
-> forall (ix :: k). SingI ix => a ix -> m (IFix f ix)
forall k (f :: (k -> *) -> k -> *) (m :: (k -> *) -> k -> *)
       (a :: k -> *) (x :: * -> *).
(ITraversable f, ITraversable m, IMonad m, Monad x) =>
DistLaw m f
-> (forall (ix :: k). SingI ix => a ix -> x (f (m a) ix))
-> forall (ix :: k). SingI ix => a ix -> x (IFix f ix)
gunfoldM forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw IIdentity f
DistLaw IIdentity f
distAna ((f a ix -> f (IIdentity a) ix)
-> m (f a ix) -> m (f (IIdentity a) ix)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a ~~> IIdentity a) -> f a ~~> f (IIdentity a)
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap a ~~> IIdentity a
forall k (f :: k -> *) (ix :: k). f ix -> IIdentity f ix
IIdentity) (m (f a ix) -> m (f (IIdentity a) ix))
-> (a ix -> m (f a ix)) -> a ix -> m (f (IIdentity a) ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a ix -> m (f a ix)
forall (ix :: k). SingI ix => a ix -> m (f a ix)
g)

-- | Monadic apomorphism
apoM :: (ITraversable f, Monad m)
     => (forall ix. SingI ix => a ix -> m (f (Sum (IFix f) a) ix))
     -> (forall ix. SingI ix => a ix -> m (IFix f ix))
apoM :: (forall (ix :: k). SingI ix => a ix -> m (f (Sum (IFix f) a) ix))
-> forall (ix :: k). SingI ix => a ix -> m (IFix f ix)
apoM = DistLaw (Sum (IFix f)) f
-> (forall (ix :: k).
    SingI ix =>
    a ix -> m (f (Sum (IFix f) a) ix))
-> forall (ix :: k). SingI ix => a ix -> m (IFix f ix)
forall k (f :: (k -> *) -> k -> *) (m :: (k -> *) -> k -> *)
       (a :: k -> *) (x :: * -> *).
(ITraversable f, ITraversable m, IMonad m, Monad x) =>
DistLaw m f
-> (forall (ix :: k). SingI ix => a ix -> x (f (m a) ix))
-> forall (ix :: k). SingI ix => a ix -> x (IFix f ix)
gunfoldM forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw (Sum (IFix f)) f
DistLaw (Sum (IFix f)) f
distApo

-- | Monadic hylomorphism
hyloM :: (ITraversable f, Monad m)
     => (forall ix. SingI ix => f b ix -> m (b ix))
     -> (forall ix. SingI ix => a ix -> m (f a ix))
     -> (forall ix. SingI ix => a ix -> m (b ix))
hyloM :: (forall (ix :: k). SingI ix => f b ix -> m (b ix))
-> (forall (ix :: k). SingI ix => a ix -> m (f a ix))
-> forall (ix :: k). SingI ix => a ix -> m (b ix)
hyloM f :: forall (ix :: k). SingI ix => f b ix -> m (b ix)
f g :: forall (ix :: k). SingI ix => a ix -> m (f a ix)
g = DistLaw f IIdentity
-> DistLaw IIdentity f
-> (forall (ix :: k). SingI ix => f (IIdentity b) ix -> m (b ix))
-> (forall (ix :: k). SingI ix => a ix -> m (f (IIdentity a) ix))
-> forall (ix :: k). SingI ix => a ix -> m (b ix)
forall k (f :: (k -> *) -> k -> *) (w :: (k -> *) -> k -> *)
       (m :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *)
       (x :: * -> *).
(ITraversable f, ITraversable w, ITraversable m, IComonad w,
 IMonad m, Monad x) =>
DistLaw f w
-> DistLaw m f
-> (forall (ix :: k). SingI ix => f (w b) ix -> x (b ix))
-> (forall (ix :: k). SingI ix => a ix -> x (f (m a) ix))
-> forall (ix :: k). SingI ix => a ix -> x (b ix)
ghyloM forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw f IIdentity
DistLaw f IIdentity
distCata forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw IIdentity f
DistLaw IIdentity f
distAna (f b ix -> m (b ix)
forall (ix :: k). SingI ix => f b ix -> m (b ix)
f (f b ix -> m (b ix))
-> (f (IIdentity b) ix -> f b ix) -> f (IIdentity b) ix -> m (b ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IIdentity b ~~> b) -> f (IIdentity b) ~~> f b
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap IIdentity b ~~> b
forall k (f :: k -> *) (ix :: k). IIdentity f ix -> f ix
runIIdentity) ((f a ix -> f (IIdentity a) ix)
-> m (f a ix) -> m (f (IIdentity a) ix)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a ~~> IIdentity a) -> f a ~~> f (IIdentity a)
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap a ~~> IIdentity a
forall k (f :: k -> *) (ix :: k). f ix -> IIdentity f ix
IIdentity) (m (f a ix) -> m (f (IIdentity a) ix))
-> (a ix -> m (f a ix)) -> a ix -> m (f (IIdentity a) ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a ix -> m (f a ix)
forall (ix :: k). SingI ix => a ix -> m (f a ix)
g)

-- | Monadic dynamorphism
dynaM :: (ITraversable f, Monad m)
      => (forall ix. SingI ix => f (ICofree f b) ix -> m (b ix))
      -> (forall ix. SingI ix => a ix -> m (f a ix))
      -> (forall ix. SingI ix => a ix -> m (b ix))
dynaM :: (forall (ix :: k). SingI ix => f (ICofree f b) ix -> m (b ix))
-> (forall (ix :: k). SingI ix => a ix -> m (f a ix))
-> forall (ix :: k). SingI ix => a ix -> m (b ix)
dynaM f :: forall (ix :: k). SingI ix => f (ICofree f b) ix -> m (b ix)
f g :: forall (ix :: k). SingI ix => a ix -> m (f a ix)
g = DistLaw f (ICofree f)
-> DistLaw IIdentity f
-> (forall (ix :: k). SingI ix => f (ICofree f b) ix -> m (b ix))
-> (forall (ix :: k). SingI ix => a ix -> m (f (IIdentity a) ix))
-> forall (ix :: k). SingI ix => a ix -> m (b ix)
forall k (f :: (k -> *) -> k -> *) (w :: (k -> *) -> k -> *)
       (m :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *)
       (x :: * -> *).
(ITraversable f, ITraversable w, ITraversable m, IComonad w,
 IMonad m, Monad x) =>
DistLaw f w
-> DistLaw m f
-> (forall (ix :: k). SingI ix => f (w b) ix -> x (b ix))
-> (forall (ix :: k). SingI ix => a ix -> x (f (m a) ix))
-> forall (ix :: k). SingI ix => a ix -> x (b ix)
ghyloM forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw f (ICofree f)
DistLaw f (ICofree f)
distHisto forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw IIdentity f
DistLaw IIdentity f
distAna forall (ix :: k). SingI ix => f (ICofree f b) ix -> m (b ix)
f ((f a ix -> f (IIdentity a) ix)
-> m (f a ix) -> m (f (IIdentity a) ix)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a ~~> IIdentity a) -> f a ~~> f (IIdentity a)
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap a ~~> IIdentity a
forall k (f :: k -> *) (ix :: k). f ix -> IIdentity f ix
IIdentity) (m (f a ix) -> m (f (IIdentity a) ix))
-> (a ix -> m (f a ix)) -> a ix -> m (f (IIdentity a) ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a ix -> m (f a ix)
forall (ix :: k). SingI ix => a ix -> m (f a ix)
g)

-- * Distribution laws

-- | Type of distribution laws
-- A Constructive morphism means the second part is a 'IComonad'
-- A Destructive morphism means the first part is an 'IMonad'
type DistLaw f g = forall a. f (g a) ~~> g (f a)

-- * Constructive distribution laws

distCata :: IFunctor f => DistLaw f IIdentity
distCata :: DistLaw f IIdentity
distCata = f a ix -> IIdentity (f a) ix
forall k (f :: k -> *) (ix :: k). f ix -> IIdentity f ix
IIdentity (f a ix -> IIdentity (f a) ix)
-> (f (IIdentity a) ix -> f a ix)
-> f (IIdentity a) ix
-> IIdentity (f a) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IIdentity a ~~> a) -> f (IIdentity a) ~~> f a
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap IIdentity a ~~> a
forall k (f :: k -> *) (ix :: k). IIdentity f ix -> f ix
runIIdentity

distPara :: IFunctor f => DistLaw f (Product (IFix f))
distPara :: DistLaw f (Product (IFix f))
distPara = (f (IFix f) ~~> IFix f) -> DistLaw f (Product (IFix f))
forall k (f :: (k -> *) -> k -> *) (b :: k -> *).
IFunctor f =>
(f b ~~> b) -> DistLaw f (Product b)
distZygo f (IFix f) ~~> IFix f
forall k (f :: (k -> *) -> k -> *) (ix :: k).
f (IFix f) ix -> IFix f ix
IFix

distZygo :: IFunctor f => (f b ~~> b) -> DistLaw f (Product b)
distZygo :: (f b ~~> b) -> DistLaw f (Product b)
distZygo g :: f b ~~> b
g m :: f (Product b a) ix
m = b ix -> f a ix -> Product b (f a) ix
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (f b ix -> b ix
f b ~~> b
g ((Product b a ~~> b) -> f (Product b a) ix -> f b ix
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap (\(Pair a _) -> b ix
a) f (Product b a) ix
m)) ((Product b a ~~> a) -> f (Product b a) ix -> f a ix
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap (\(Pair _ b) -> a ix
b) f (Product b a) ix
m)

distHisto :: IFunctor f => DistLaw f (ICofree f)
distHisto :: DistLaw f (ICofree f)
distHisto x :: f (ICofree f a) ix
x = (ICofree f a ~~> a) -> f (ICofree f a) ix -> f a ix
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap (\(a ::< _) -> a ix
a) f (ICofree f a) ix
x f a ix -> f (ICofree f (f a)) ix -> ICofree f (f a) ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (ix :: k).
a ix -> f (ICofree f a) ix -> ICofree f a ix
::< (ICofree f a ~~> ICofree f (f a))
-> f (ICofree f a) ix -> f (ICofree f (f a)) ix
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap (\(_ ::< x) -> f (ICofree f a) ix -> ICofree f (f a) ix
forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw f (ICofree f)
distHisto f (ICofree f a) ix
x) f (ICofree f a) ix
x

-- * Destructive distribution laws

distAna :: IFunctor f => DistLaw IIdentity f
distAna :: DistLaw IIdentity f
distAna = (a ~~> IIdentity a) -> f a ~~> f (IIdentity a)
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap a ~~> IIdentity a
forall k (f :: k -> *) (ix :: k). f ix -> IIdentity f ix
IIdentity (f a ix -> f (IIdentity a) ix)
-> (IIdentity (f a) ix -> f a ix)
-> IIdentity (f a) ix
-> f (IIdentity a) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IIdentity (f a) ix -> f a ix
forall k (f :: k -> *) (ix :: k). IIdentity f ix -> f ix
runIIdentity

distApo :: IFunctor f => DistLaw (Sum (IFix f)) f
distApo :: DistLaw (Sum (IFix f)) f
distApo = (IFix f ~~> f (IFix f)) -> DistLaw (Sum (IFix f)) f
forall k (f :: (k -> *) -> k -> *) (b :: k -> *).
IFunctor f =>
(b ~~> f b) -> DistLaw (Sum b) f
distGApo IFix f ~~> f (IFix f)
forall k (f :: (k -> *) -> k -> *) (ix :: k).
IFix f ix -> f (IFix f) ix
unIFix

distGApo :: IFunctor f => (b ~~> f b) -> DistLaw (Sum b) f
distGApo :: (b ~~> f b) -> DistLaw (Sum b) f
distGApo f :: b ~~> f b
f (InL x :: b ix
x) = (b ~~> Sum b a) -> f b ~~> f (Sum b a)
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap b ~~> Sum b a
forall k (f :: k -> *) (g :: k -> *) (a :: k). f a -> Sum f g a
InL (f b ix -> f (Sum b a) ix) -> f b ix -> f (Sum b a) ix
forall a b. (a -> b) -> a -> b
$ b ix -> f b ix
b ~~> f b
f b ix
x
distGApo _ (InR x :: f a ix
x) = (a ~~> Sum b a) -> f a ix -> f (Sum b a) ix
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap a ~~> Sum b a
forall k (f :: k -> *) (g :: k -> *) (a :: k). g a -> Sum f g a
InR f a ix
x

distFutu :: IFunctor f => DistLaw (IFree f) f
distFutu :: DistLaw (IFree f) f
distFutu (IPure x :: f a ix
x) = (a ~~> IFree f a) -> f a ix -> f (IFree f a) ix
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap a ~~> IFree f a
forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (ix :: k).
a ix -> IFree f a ix
IPure f a ix
x
distFutu (IFree x :: f (IFree f (f a)) ix
x) = (IFree f (f a) ~~> IFree f a)
-> f (IFree f (f a)) ix -> f (IFree f a) ix
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap (f (IFree f a) ix -> IFree f a ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *) (ix :: k).
f (IFree f a) ix -> IFree f a ix
IFree (f (IFree f a) ix -> IFree f a ix)
-> (IFree f (f a) ix -> f (IFree f a) ix)
-> IFree f (f a) ix
-> IFree f a ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IFree f (f a) ix -> f (IFree f a) ix
forall k (f :: (k -> *) -> k -> *).
IFunctor f =>
DistLaw (IFree f) f
distFutu) f (IFree f (f a)) ix
x

-- * Generalized combinators

-- | Generalized fold
gfold :: forall f w a. (IFunctor f, IComonad w)
      => DistLaw f w
      -> (f (w a) ~~> a)
      -> (IFix f ~~> a)
gfold :: DistLaw f w -> (f (w a) ~~> a) -> IFix f ~~> a
gfold k :: DistLaw f w
k g :: f (w a) ~~> a
g = f (w a) ix -> a ix
f (w a) ~~> a
g (f (w a) ix -> a ix)
-> (IFix f ix -> f (w a) ix) -> IFix f ix -> a ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. w (f (w a)) ix -> f (w a) ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IComonad f =>
f a ~~> a
iextract (w (f (w a)) ix -> f (w a) ix)
-> (IFix f ix -> w (f (w a)) ix) -> IFix f ix -> f (w a) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IFix f ix -> w (f (w a)) ix
IFix f ~~> w (f (w a))
c
    where
        c :: IFix f ~~> w (f (w a))
        c :: IFix f ix -> w (f (w a)) ix
c = f (w (w a)) ix -> w (f (w a)) ix
DistLaw f w
k (f (w (w a)) ix -> w (f (w a)) ix)
-> (IFix f ix -> f (w (w a)) ix) -> IFix f ix -> w (f (w a)) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IFix f ~~> w (w a)) -> f (IFix f) ~~> f (w (w a))
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap (w a ix -> w (w a) ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IComonad f =>
f a ~~> f (f a)
iduplicate (w a ix -> w (w a) ix)
-> (IFix f ix -> w a ix) -> IFix f ix -> w (w a) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (w a) ~~> a) -> w (f (w a)) ~~> w a
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap f (w a) ~~> a
g (w (f (w a)) ix -> w a ix)
-> (IFix f ix -> w (f (w a)) ix) -> IFix f ix -> w a ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IFix f ix -> w (f (w a)) ix
IFix f ~~> w (f (w a))
c) (f (IFix f) ix -> f (w (w a)) ix)
-> (IFix f ix -> f (IFix f) ix) -> IFix f ix -> f (w (w a)) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IFix f ix -> f (IFix f) ix
forall k (f :: (k -> *) -> k -> *) (ix :: k).
IFix f ix -> f (IFix f) ix
unIFix

-- | Generalized unfold
gunfold :: forall f m a. (IFunctor f, IMonad m)
        => DistLaw m f
        -> (a ~~> f (m a))
        -> (a ~~> IFix f)
gunfold :: DistLaw m f -> (a ~~> f (m a)) -> a ~~> IFix f
gunfold k :: DistLaw m f
k f :: a ~~> f (m a)
f = m (f (m a)) ix -> IFix f ix
m (f (m a)) ~~> IFix f
a (m (f (m a)) ix -> IFix f ix)
-> (a ix -> m (f (m a)) ix) -> a ix -> IFix f ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (m a) ix -> m (f (m a)) ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IMonad f =>
a ~~> f a
ipure (f (m a) ix -> m (f (m a)) ix)
-> (a ix -> f (m a) ix) -> a ix -> m (f (m a)) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a ix -> f (m a) ix
a ~~> f (m a)
f
    where
        a :: m (f (m a)) ~~> IFix f
        a :: m (f (m a)) ix -> IFix f ix
a = f (IFix f) ix -> IFix f ix
forall k (f :: (k -> *) -> k -> *) (ix :: k).
f (IFix f) ix -> IFix f ix
IFix (f (IFix f) ix -> IFix f ix)
-> (m (f (m a)) ix -> f (IFix f) ix) -> m (f (m a)) ix -> IFix f ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m (m a) ~~> IFix f) -> f (m (m a)) ~~> f (IFix f)
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap (m (f (m a)) ix -> IFix f ix
m (f (m a)) ~~> IFix f
a (m (f (m a)) ix -> IFix f ix)
-> (m (m a) ix -> m (f (m a)) ix) -> m (m a) ix -> IFix f ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a ~~> f (m a)) -> m a ~~> m (f (m a))
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap a ~~> f (m a)
f (m a ix -> m (f (m a)) ix)
-> (m (m a) ix -> m a ix) -> m (m a) ix -> m (f (m a)) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (m a) ix -> m a ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IMonad f =>
f (f a) ~~> f a
ijoin) (f (m (m a)) ix -> f (IFix f) ix)
-> (m (f (m a)) ix -> f (m (m a)) ix)
-> m (f (m a)) ix
-> f (IFix f) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (f (m a)) ix -> f (m (m a)) ix
DistLaw m f
k

-- | Generalized hylomorphism
ghylo :: forall f w m a b. (IFunctor f, IComonad w, IMonad m)
      => DistLaw f w
      -> DistLaw m f
      -> f (w b) ~~> b
      -> a ~~> f (m a)
      -> a ~~> b
ghylo :: DistLaw f w
-> DistLaw m f -> (f (w b) ~~> b) -> (a ~~> f (m a)) -> a ~~> b
ghylo w :: DistLaw f w
w m :: DistLaw m f
m f :: f (w b) ~~> b
f g :: a ~~> f (m a)
g = w b ix -> b ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IComonad f =>
f a ~~> a
iextract (w b ix -> b ix) -> (a ix -> w b ix) -> a ix -> b ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a ix -> w b ix
m a ~~> w b
h (m a ix -> w b ix) -> (a ix -> m a ix) -> a ix -> w b ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a ix -> m a ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IMonad f =>
a ~~> f a
ipure
    where
        h :: m a ~~> w b
        h :: m a ix -> w b ix
h = (f (w b) ~~> b) -> w (f (w b)) ~~> w b
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap f (w b) ~~> b
f (w (f (w b)) ix -> w b ix)
-> (m a ix -> w (f (w b)) ix) -> m a ix -> w b ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (w (w b)) ix -> w (f (w b)) ix
DistLaw f w
w (f (w (w b)) ix -> w (f (w b)) ix)
-> (m a ix -> f (w (w b)) ix) -> m a ix -> w (f (w b)) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m (m a) ~~> w (w b)) -> f (m (m a)) ~~> f (w (w b))
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap (w b ix -> w (w b) ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IComonad f =>
f a ~~> f (f a)
iduplicate (w b ix -> w (w b) ix)
-> (m (m a) ix -> w b ix) -> m (m a) ix -> w (w b) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a ix -> w b ix
m a ~~> w b
h (m a ix -> w b ix)
-> (m (m a) ix -> m a ix) -> m (m a) ix -> w b ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (m a) ix -> m a ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IMonad f =>
f (f a) ~~> f a
ijoin) (f (m (m a)) ix -> f (w (w b)) ix)
-> (m a ix -> f (m (m a)) ix) -> m a ix -> f (w (w b)) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (f (m a)) ix -> f (m (m a)) ix
DistLaw m f
m (m (f (m a)) ix -> f (m (m a)) ix)
-> (m a ix -> m (f (m a)) ix) -> m a ix -> f (m (m a)) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a ~~> f (m a)) -> m a ~~> m (f (m a))
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap a ~~> f (m a)
g

-- | Generalized monadic fold
gfoldM :: forall f w m a. (ITraversable f, ITraversable w, IComonad w, Monad m)
       => DistLaw f w
       -> (forall ix. SingI ix => f (w a) ix -> m (a ix))
       -> (forall ix. SingI ix => IFix f ix -> m (a ix))
gfoldM :: DistLaw f w
-> (forall (ix :: k). SingI ix => f (w a) ix -> m (a ix))
-> forall (ix :: k). SingI ix => IFix f ix -> m (a ix)
gfoldM k :: DistLaw f w
k g :: forall (ix :: k). SingI ix => f (w a) ix -> m (a ix)
g = f (w a) ix -> m (a ix)
forall (ix :: k). SingI ix => f (w a) ix -> m (a ix)
g (f (w a) ix -> m (a ix))
-> (w (f (w a)) ix -> f (w a) ix) -> w (f (w a)) ix -> m (a ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. w (f (w a)) ix -> f (w a) ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IComonad f =>
f a ~~> a
iextract (w (f (w a)) ix -> m (a ix))
-> (IFix f ix -> m (w (f (w a)) ix)) -> IFix f ix -> m (a ix)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< IFix f ix -> m (w (f (w a)) ix)
forall (ix :: k). SingI ix => IFix f ix -> m (w (f (w a)) ix)
c
    where
        c :: forall ix. SingI ix => IFix f ix -> m (w (f (w a)) ix)
        c :: IFix f ix -> m (w (f (w a)) ix)
c = (f (w (w a)) ix -> w (f (w a)) ix)
-> m (f (w (w a)) ix) -> m (w (f (w a)) ix)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (w (w a)) ix -> w (f (w a)) ix
DistLaw f w
k (m (f (w (w a)) ix) -> m (w (f (w a)) ix))
-> (IFix f ix -> m (f (w (w a)) ix))
-> IFix f ix
-> m (w (f (w a)) ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (ix :: k). SingI ix => IFix f ix -> m (w (w a) ix))
-> f (IFix f) ix -> m (f (w (w a)) ix)
forall k k (f :: (k -> *) -> k -> *) (m :: * -> *) (ix :: k)
       (a :: k -> *) (b :: k -> *).
(ITraversable f, Applicative m, SingI ix) =>
(forall (ix :: k). SingI ix => a ix -> m (b ix))
-> f a ix -> m (f b ix)
itraverse ((w a ix -> w (w a) ix) -> m (w a ix) -> m (w (w a) ix)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap w a ix -> w (w a) ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IComonad f =>
f a ~~> f (f a)
iduplicate (m (w a ix) -> m (w (w a) ix))
-> (w (f (w a)) ix -> m (w a ix))
-> w (f (w a)) ix
-> m (w (w a) ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (ix :: k). SingI ix => f (w a) ix -> m (a ix))
-> w (f (w a)) ix -> m (w a ix)
forall k k (f :: (k -> *) -> k -> *) (m :: * -> *) (ix :: k)
       (a :: k -> *) (b :: k -> *).
(ITraversable f, Applicative m, SingI ix) =>
(forall (ix :: k). SingI ix => a ix -> m (b ix))
-> f a ix -> m (f b ix)
itraverse forall (ix :: k). SingI ix => f (w a) ix -> m (a ix)
g (w (f (w a)) ix -> m (w (w a) ix))
-> (IFix f ix -> m (w (f (w a)) ix)) -> IFix f ix -> m (w (w a) ix)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< IFix f ix -> m (w (f (w a)) ix)
forall (ix :: k). SingI ix => IFix f ix -> m (w (f (w a)) ix)
c) (f (IFix f) ix -> m (f (w (w a)) ix))
-> (IFix f ix -> f (IFix f) ix) -> IFix f ix -> m (f (w (w a)) ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IFix f ix -> f (IFix f) ix
forall k (f :: (k -> *) -> k -> *) (ix :: k).
IFix f ix -> f (IFix f) ix
unIFix

-- | Generalized monadic unfold
gunfoldM :: forall f m a x. (ITraversable f, ITraversable m, IMonad m, Monad x)
         => DistLaw m f
         -> (forall ix. SingI ix => a ix -> x (f (m a) ix))
         -> (forall ix. SingI ix => a ix -> x (IFix f ix))
gunfoldM :: DistLaw m f
-> (forall (ix :: k). SingI ix => a ix -> x (f (m a) ix))
-> forall (ix :: k). SingI ix => a ix -> x (IFix f ix)
gunfoldM k :: DistLaw m f
k f :: forall (ix :: k). SingI ix => a ix -> x (f (m a) ix)
f = m (f (m a)) ix -> x (IFix f ix)
forall (ix :: k). SingI ix => m (f (m a)) ix -> x (IFix f ix)
a (m (f (m a)) ix -> x (IFix f ix))
-> (f (m a) ix -> m (f (m a)) ix) -> f (m a) ix -> x (IFix f ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (m a) ix -> m (f (m a)) ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IMonad f =>
a ~~> f a
ipure (f (m a) ix -> x (IFix f ix))
-> (a ix -> x (f (m a) ix)) -> a ix -> x (IFix f ix)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< a ix -> x (f (m a) ix)
forall (ix :: k). SingI ix => a ix -> x (f (m a) ix)
f
    where
        a :: SingI ix => m (f (m a)) ix -> x (IFix f ix)
        a :: m (f (m a)) ix -> x (IFix f ix)
a = (f (IFix f) ix -> IFix f ix) -> x (f (IFix f) ix) -> x (IFix f ix)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (IFix f) ix -> IFix f ix
forall k (f :: (k -> *) -> k -> *) (ix :: k).
f (IFix f) ix -> IFix f ix
IFix (x (f (IFix f) ix) -> x (IFix f ix))
-> (m (f (m a)) ix -> x (f (IFix f) ix))
-> m (f (m a)) ix
-> x (IFix f ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (ix :: k). SingI ix => m (m a) ix -> x (IFix f ix))
-> f (m (m a)) ix -> x (f (IFix f) ix)
forall k k (f :: (k -> *) -> k -> *) (m :: * -> *) (ix :: k)
       (a :: k -> *) (b :: k -> *).
(ITraversable f, Applicative m, SingI ix) =>
(forall (ix :: k). SingI ix => a ix -> m (b ix))
-> f a ix -> m (f b ix)
itraverse (m (f (m a)) ix -> x (IFix f ix)
forall (ix :: k). SingI ix => m (f (m a)) ix -> x (IFix f ix)
a (m (f (m a)) ix -> x (IFix f ix))
-> (m (m a) ix -> x (m (f (m a)) ix))
-> m (m a) ix
-> x (IFix f ix)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< (forall (ix :: k). SingI ix => a ix -> x (f (m a) ix))
-> m a ix -> x (m (f (m a)) ix)
forall k k (f :: (k -> *) -> k -> *) (m :: * -> *) (ix :: k)
       (a :: k -> *) (b :: k -> *).
(ITraversable f, Applicative m, SingI ix) =>
(forall (ix :: k). SingI ix => a ix -> m (b ix))
-> f a ix -> m (f b ix)
itraverse forall (ix :: k). SingI ix => a ix -> x (f (m a) ix)
f (m a ix -> x (m (f (m a)) ix))
-> (m (m a) ix -> m a ix) -> m (m a) ix -> x (m (f (m a)) ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (m a) ix -> m a ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IMonad f =>
f (f a) ~~> f a
ijoin) (f (m (m a)) ix -> x (f (IFix f) ix))
-> (m (f (m a)) ix -> f (m (m a)) ix)
-> m (f (m a)) ix
-> x (f (IFix f) ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (f (m a)) ix -> f (m (m a)) ix
DistLaw m f
k

-- | Generalized monadic hylomorphism
ghyloM :: forall f w m a b x. (ITraversable f, ITraversable w, ITraversable m, IComonad w, IMonad m, Monad x)
       => DistLaw f w
       -> DistLaw m f
       -> (forall ix. SingI ix => f (w b) ix -> x (b ix))
       -> (forall ix. SingI ix => a ix -> x (f (m a) ix))
       -> (forall ix. SingI ix => a ix -> x (b ix))
ghyloM :: DistLaw f w
-> DistLaw m f
-> (forall (ix :: k). SingI ix => f (w b) ix -> x (b ix))
-> (forall (ix :: k). SingI ix => a ix -> x (f (m a) ix))
-> forall (ix :: k). SingI ix => a ix -> x (b ix)
ghyloM w :: DistLaw f w
w m :: DistLaw m f
m f :: forall (ix :: k). SingI ix => f (w b) ix -> x (b ix)
f g :: forall (ix :: k). SingI ix => a ix -> x (f (m a) ix)
g = (w b ix -> b ix) -> x (w b ix) -> x (b ix)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap w b ix -> b ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IComonad f =>
f a ~~> a
iextract (x (w b ix) -> x (b ix))
-> (a ix -> x (w b ix)) -> a ix -> x (b ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a ix -> x (w b ix)
forall (ix :: k). SingI ix => m a ix -> x (w b ix)
h (m a ix -> x (w b ix)) -> (a ix -> m a ix) -> a ix -> x (w b ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a ix -> m a ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IMonad f =>
a ~~> f a
ipure
    where
        h :: SingI ix => m a ix -> x (w b ix)
        h :: m a ix -> x (w b ix)
h = (forall (ix :: k). SingI ix => f (w b) ix -> x (b ix))
-> w (f (w b)) ix -> x (w b ix)
forall k k (f :: (k -> *) -> k -> *) (m :: * -> *) (ix :: k)
       (a :: k -> *) (b :: k -> *).
(ITraversable f, Applicative m, SingI ix) =>
(forall (ix :: k). SingI ix => a ix -> m (b ix))
-> f a ix -> m (f b ix)
itraverse forall (ix :: k). SingI ix => f (w b) ix -> x (b ix)
f (w (f (w b)) ix -> x (w b ix))
-> (m a ix -> x (w (f (w b)) ix)) -> m a ix -> x (w b ix)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< (f (w (w b)) ix -> w (f (w b)) ix)
-> x (f (w (w b)) ix) -> x (w (f (w b)) ix)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap f (w (w b)) ix -> w (f (w b)) ix
DistLaw f w
w (x (f (w (w b)) ix) -> x (w (f (w b)) ix))
-> (m (f (m a)) ix -> x (f (w (w b)) ix))
-> m (f (m a)) ix
-> x (w (f (w b)) ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (ix :: k). SingI ix => m (m a) ix -> x (w (w b) ix))
-> f (m (m a)) ix -> x (f (w (w b)) ix)
forall k k (f :: (k -> *) -> k -> *) (m :: * -> *) (ix :: k)
       (a :: k -> *) (b :: k -> *).
(ITraversable f, Applicative m, SingI ix) =>
(forall (ix :: k). SingI ix => a ix -> m (b ix))
-> f a ix -> m (f b ix)
itraverse ((w b ix -> w (w b) ix) -> x (w b ix) -> x (w (w b) ix)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap w b ix -> w (w b) ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IComonad f =>
f a ~~> f (f a)
iduplicate (x (w b ix) -> x (w (w b) ix))
-> (m (m a) ix -> x (w b ix)) -> m (m a) ix -> x (w (w b) ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a ix -> x (w b ix)
forall (ix :: k). SingI ix => m a ix -> x (w b ix)
h (m a ix -> x (w b ix))
-> (m (m a) ix -> m a ix) -> m (m a) ix -> x (w b ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (m a) ix -> m a ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IMonad f =>
f (f a) ~~> f a
ijoin) (f (m (m a)) ix -> x (f (w (w b)) ix))
-> (m (f (m a)) ix -> f (m (m a)) ix)
-> m (f (m a)) ix
-> x (f (w (w b)) ix)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (f (m a)) ix -> f (m (m a)) ix
DistLaw m f
m (m (f (m a)) ix -> x (w (f (w b)) ix))
-> (m a ix -> x (m (f (m a)) ix)) -> m a ix -> x (w (f (w b)) ix)
forall (m :: * -> *) b c a.
Monad m =>
(b -> m c) -> (a -> m b) -> a -> m c
<=< (forall (ix :: k). SingI ix => a ix -> x (f (m a) ix))
-> m a ix -> x (m (f (m a)) ix)
forall k k (f :: (k -> *) -> k -> *) (m :: * -> *) (ix :: k)
       (a :: k -> *) (b :: k -> *).
(ITraversable f, Applicative m, SingI ix) =>
(forall (ix :: k). SingI ix => a ix -> m (b ix))
-> f a ix -> m (f b ix)
itraverse forall (ix :: k). SingI ix => a ix -> x (f (m a) ix)
g

-- | Generalized prepromorphism
gprepro :: forall f w a. (IFunctor f, IComonad w)
        => DistLaw f w
        -> (forall c. f c ~~> f c)
        -> (f (w a) ~~> a)
        -> (IFix f ~~> a)
gprepro :: DistLaw f w
-> (forall (c :: k -> *). f c ~~> f c)
-> (f (w a) ~~> a)
-> IFix f ~~> a
gprepro k :: DistLaw f w
k e :: forall (c :: k -> *). f c ~~> f c
e f :: f (w a) ~~> a
f = w a ix -> a ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IComonad f =>
f a ~~> a
iextract (w a ix -> a ix) -> (IFix f ix -> w a ix) -> IFix f ix -> a ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IFix f ix -> w a ix
IFix f ~~> w a
c
    where
        c :: IFix f ~~> w a
        c :: IFix f ix -> w a ix
c = (f (w a) ~~> a) -> w (f (w a)) ~~> w a
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap f (w a) ~~> a
f (w (f (w a)) ix -> w a ix)
-> (IFix f ix -> w (f (w a)) ix) -> IFix f ix -> w a ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (w (w a)) ix -> w (f (w a)) ix
DistLaw f w
k (f (w (w a)) ix -> w (f (w a)) ix)
-> (IFix f ix -> f (w (w a)) ix) -> IFix f ix -> w (f (w a)) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (IFix f ~~> w (w a)) -> f (IFix f) ~~> f (w (w a))
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap (w a ix -> w (w a) ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IComonad f =>
f a ~~> f (f a)
iduplicate (w a ix -> w (w a) ix)
-> (IFix f ix -> w a ix) -> IFix f ix -> w (w a) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IFix f ix -> w a ix
IFix f ~~> w a
c (IFix f ix -> w a ix)
-> (IFix f ix -> IFix f ix) -> IFix f ix -> w a ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f (IFix f) ~~> IFix f) -> IFix f ~~> IFix f
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IFunctor f =>
(f a ~~> a) -> IFix f ~~> a
cata (f (IFix f) ix -> IFix f ix
forall k (f :: (k -> *) -> k -> *) (ix :: k).
f (IFix f) ix -> IFix f ix
IFix (f (IFix f) ix -> IFix f ix)
-> (f (IFix f) ix -> f (IFix f) ix) -> f (IFix f) ix -> IFix f ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (IFix f) ix -> f (IFix f) ix
forall (c :: k -> *). f c ~~> f c
e)) (f (IFix f) ix -> f (w (w a)) ix)
-> (IFix f ix -> f (IFix f) ix) -> IFix f ix -> f (w (w a)) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IFix f ix -> f (IFix f) ix
forall k (f :: (k -> *) -> k -> *) (ix :: k).
IFix f ix -> f (IFix f) ix
unIFix

-- | Generalized postpromorphism
gpostpro :: forall f m a. (IFunctor f, IMonad m)
         => DistLaw m f
         -> (forall c. f c ~~> f c)
         -> (a ~~> f (m a))
         -> (a ~~> IFix f)
gpostpro :: DistLaw m f
-> (forall (c :: k -> *). f c ~~> f c)
-> (a ~~> f (m a))
-> a ~~> IFix f
gpostpro k :: DistLaw m f
k e :: forall (c :: k -> *). f c ~~> f c
e g :: a ~~> f (m a)
g = m a ix -> IFix f ix
m a ~~> IFix f
a (m a ix -> IFix f ix) -> (a ix -> m a ix) -> a ix -> IFix f ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a ix -> m a ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IMonad f =>
a ~~> f a
ipure
    where
        a :: m a ~~> IFix f
        a :: m a ix -> IFix f ix
a = f (IFix f) ix -> IFix f ix
forall k (f :: (k -> *) -> k -> *) (ix :: k).
f (IFix f) ix -> IFix f ix
IFix (f (IFix f) ix -> IFix f ix)
-> (m a ix -> f (IFix f) ix) -> m a ix -> IFix f ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (m (m a) ~~> IFix f) -> f (m (m a)) ~~> f (IFix f)
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap ((f (IFix f) ~~> IFix f) -> IFix f ~~> IFix f
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IFunctor f =>
(f a ~~> a) -> IFix f ~~> a
cata (f (IFix f) ix -> IFix f ix
forall k (f :: (k -> *) -> k -> *) (ix :: k).
f (IFix f) ix -> IFix f ix
IFix (f (IFix f) ix -> IFix f ix)
-> (f (IFix f) ix -> f (IFix f) ix) -> f (IFix f) ix -> IFix f ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f (IFix f) ix -> f (IFix f) ix
forall (c :: k -> *). f c ~~> f c
e) (IFix f ix -> IFix f ix)
-> (m (m a) ix -> IFix f ix) -> m (m a) ix -> IFix f ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a ix -> IFix f ix
m a ~~> IFix f
a (m a ix -> IFix f ix)
-> (m (m a) ix -> m a ix) -> m (m a) ix -> IFix f ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (m a) ix -> m a ix
forall k (f :: (k -> *) -> k -> *) (a :: k -> *).
IMonad f =>
f (f a) ~~> f a
ijoin) (f (m (m a)) ix -> f (IFix f) ix)
-> (m a ix -> f (m (m a)) ix) -> m a ix -> f (IFix f) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m (f (m a)) ix -> f (m (m a)) ix
DistLaw m f
k (m (f (m a)) ix -> f (m (m a)) ix)
-> (m a ix -> m (f (m a)) ix) -> m a ix -> f (m (m a)) ix
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a ~~> f (m a)) -> m a ~~> m (f (m a))
forall k k (f :: (k -> *) -> k -> *) (a :: k -> *) (b :: k -> *).
IFunctor f =>
(a ~~> b) -> f a ~~> f b
imap a ~~> f (m a)
g