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 
  }