module Polynomial.Monad where

open import Prelude.Basic
open import Prelude.Equality
open import Prelude.Fam
open import Prelude.Equivalences

open import Polynomial.IR

-- unit

IR-η : {D E : Set₁} -> E -> IR D E
IR-η e = con ⊤ , (λ _ → e)

η-equal : {D E : Set₁} -> {Z : Fam D}{e : E} -> ⟦ IR-η e ⟧ Z ≡ Fam-η e
η-equal = refl

-- multiplication

Poly-μ : {D E : Set1} -> (c : Poly D) -> (α : Info c -> IR D E) ->
          Poly D
Poly-μ c α = sigma c (proj₁ ∘ α)

Info-μ : {D E : Set1} -> (c : Poly D) -> (α : Info c -> IR D E) ->
         Info (Poly-μ c α) -> E
Info-μ c α (x , y) = proj₂ (α x) y

IR-μ : {D E : Set1} -> IR D (IR D E) -> IR D E
IR-μ (c , α) = (Poly-μ c α , Info-μ c α)

μ-equal : {D E : Set₁} -> {Z : Fam D}{c : IR D (IR D E)} ->
          ⟦ IR-μ c ⟧ Z ≡ Fam-μ (Fam-map (λ x → ⟦ x ⟧ Z) (⟦ c ⟧ Z))
μ-equal = refl

-- bind

_Polynomial->>=_ : {D E E' : Set₁} → IR D E → (E → IR D E') → IR D E'
c Polynomial->>= h = IR-μ (IR-map h c)

_Polynomial->>=d_ : {C D : Set₁}{E : D -> Set₁} ->
               IR C D → ((d : D) → IR C (E d)) → IR C (Σ D E)
c Polynomial->>=d h = IR-μ (IR-map (λ d → IR-map (λ e → d , e) (h d)) c)

-- c Polynomial->>=d h = c Polynomial->>= (λ x → IR-map (λ e → (x , e)) (h x))