------------------------------------------------------------------------
-- The Agda standard library
--
-- The free monad construction on containers
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Container.FreeMonad where

open import Level using (Level; _⊔_)
open import Data.Sum.Base using (inj₁; inj₂ ; [_,_]′)
open import Data.Product.Base using (_,_; -,_)
open import Data.Container using (Container; ⟦_⟧; μ)
open import Data.Container.Relation.Unary.All using (□; all)
open import Data.Container.Combinator using (const; _⊎_)
open import Data.W as W using (sup)
open import Effect.Functor using (RawFunctor)
open import Effect.Applicative using (RawApplicative)
open import Effect.Monad using (RawMonad)
open import Function.Base as Function using (_$_; _∘_)

private
  variable
    x y s p ℓ : Level
    C : Container s p
    X : Set x
    Y : Set y

infixl  _⋆C_
infix   _⋆_

------------------------------------------------------------------------
-- The free monad construction over a container and a set is, in
-- universal algebra terminology, also known as the term algebra over a
-- signature (a container) and a set (of variable symbols). The return
-- of the free monad corresponds to variables and the bind operator
-- corresponds to (parallel) substitution.

-- A useful intuition is to think of containers describing single
-- operations and the free monad construction over a container and a set
-- describing a tree of operations as nodes and elements of the set as
-- leaves. If one starts at the root, then any path will pass finitely
-- many nodes (operations described by the container) and eventually end
-- up in a leaf (element of the set) -- hence the Kleene star notation
-- (the type can be read as a regular expression).

------------------------------------------------------------------------
-- Type definition

-- The free monad can be defined as the least fixpoint `μ (C ⋆C X)`

_⋆C_ : ∀ {x s p} → Container s p → Set x → Container (s ⊔ x) p
C ⋆C X = const X ⊎ C

-- However Agda's positivity checker is currently too weak to observe
-- that `X` is used in a strictly positive manner in `μ (C ⋆C X)` as
-- demonstrated in #693.
-- So we provide instead an inductive definition that we prove to be
-- equivalent to the μ-based one.

data _⋆_ (C : Container s p) (X : Set x) : Set (x ⊔ s ⊔ p) where
  pure : X → C ⋆ X
  impure : ⟦ C ⟧ (C ⋆ X) → C ⋆ X

------------------------------------------------------------------------
-- Equivalent types

-- We can prove that `C ⋆ X` is equivalent to one layer of `C ⋆C X` with
-- subterms of tyep `C ⋆ X`.

inj : {X : Set x} → ⟦ C ⋆C X ⟧ (C ⋆ X) → C ⋆ X
inj (inj₁ x , _) = pure x
inj (inj₂ c , r) = impure (c , r)

out : {X : Set x} → C ⋆ X → ⟦ C ⋆C X ⟧ (C ⋆ X)
out (pure x) = inj₁ x , λ ()
out (impure (c , r)) = inj₂ c , r

-- We can fully convert back and forth between `C ⋆ X` and `μ (C ⋆C X)`.

toμ : C ⋆ X → μ (C ⋆C X)
toμ (pure x) = sup (inj₁ x , λ ())
toμ (impure (c , r)) = sup (inj₂ c , toμ ∘ r)

fromμ : μ (C ⋆C X) → C ⋆ X
fromμ = W.foldr inj

-- We can recover an induction principle similar to the one given in `Data.W`.
-- We curry these ones by distinguishing the pure vs. impure case

module _ (P : C ⋆ X → Set ℓ)
         (algP : ∀ x → P (pure x))
         (algI : ∀ {t} → □ C P t → P (impure t)) where

 induction : (t : C ⋆ X) → P t
 induction (pure x) = algP x
 induction (impure (c , r)) = algI $ all (induction ∘ r)

module _ {P : Set ℓ}
         (algP : X → P)
         (algI : ⟦ C ⟧ P → P) where

 foldr : C ⋆ X → P
 foldr = induction (Function.const P) algP (algI ∘ -,_ ∘ □.proof)

infixr -1 _<$>_ _<*>_
infixl  _>>=_

_<$>_ : (X → Y) → C ⋆ X → C ⋆ Y
f <$> t = foldr (pure ∘ f) impure t

_<*>_ : C ⋆ (X → Y) → C ⋆ X → C ⋆ Y
pure f <*> t = f <$> t
impure (c , r) <*> t = impure (c , λ v → r v <*> t)

_>>=_ : C ⋆ X → (X → C ⋆ Y) → C ⋆ Y
pure x >>= f = f x
impure (c , r) >>= f = impure (c , λ v → r v >>= f)

------------------------------------------------------------------------
-- Structure

functor : RawFunctor (_⋆_ {x = x} C)
functor = record { _<$>_ = _<$>_ }

applicative : {C : Container s p} → RawApplicative (_⋆_ {x = x ⊔ s ⊔ p} C)
applicative = record
  { rawFunctor = functor
  ; pure = pure
  ; _<*>_ = _<*>_ }

monad : {C : Container s p} → RawMonad (_⋆_ {x = x ⊔ s ⊔ p} C)
monad {x = x} = record
  { rawApplicative = applicative {x = x}
  ; _>>=_ = _>>=_
  }

------------------------------------------------------------------------
-- DEPRECATIONS

rawFunctor = functor
{-# WARNING_ON_USAGE rawFunctor
"Warning: all rawFunctor deprecated in v2.0.
Please use functor instead."
#-}

rawApplicative = applicative
{-# WARNING_ON_USAGE rawApplicative
"Warning: rawApplicative was deprecated in v2.0.
Please use applicative instead."
#-}

rawMonad = monad
{-# WARNING_ON_USAGE rawMonad
"Warning: rawMonad was deprecated in v2.0.
Please use monad instead."
#-}