open import Level hiding (zero ; suc) open import Chapter4.Desc open import Chapter4.Desc.Tagged open import Chapter4.Desc.Fixpoint open import Chapter4.Desc.InitialAlgebra module Chapter6.Desc.FreeMonad.Monad {ℓ : Level} (D : tagDesc ℓ) where open import Level hiding (zero ; suc) open import Data.Unit open import Data.Nat hiding (_*_ ; fold) open import Data.Fin hiding (fold ; lift) open import Data.Vec open import Data.Product open import Category.Monad open import Chapter6.Desc.FreeMonad apply : ∀{ℓ X Y} → (D : tagDesc ℓ) → (X → D * Y) → ⟦ toDesc (D *D X) ⟧ (D * Y) → D * Y apply (cs , ds) σ (lift zero , xs , lift tt) = σ xs apply (cs , ds) σ (lift (suc k) , xs) = `comp (lift k , xs) subst : ∀{X Y} → D * X → (X → D * Y) → D * Y subst {X} dx σ = fold (toDesc (D *D X)) (apply D σ) dx monad : RawMonad (_*_ D) monad = record { return = `v ; _>>=_ = subst }