{-# OPTIONS --no-positivity-check --allow-unsolved-metas #-}

open import Prelude
open import Algebra

module Control.Comonad.Cofree
  where

module Comonadic
  {ℓ₁ β„“β‚‚} {𝑆 : Type ℓ₁} {π‘Š : 𝑆 β†’ Type β„“β‚‚ β†’ Type β„“β‚‚}
  (mon : Monoid 𝑆)
  (comon : GradedComonad mon π‘Š)
  {𝐹 : Type (ℓ₁ β„“βŠ” β„“β‚‚) β†’ Type β„“β‚‚}
  (functor : Functor 𝐹) where

  open Monoid mon
  open GradedComonad comon renaming (map to cmap)
  open Functor functor renaming (map to fmap)

  record CofreeF (A : Type β„“β‚‚) : Type β„“β‚‚ where
    constructor _β—ƒ_
    coinductive
    field
      head : A
      step : 𝐹 (βˆƒ y Γ— π‘Š y (CofreeF A))
  open CofreeF public

  Cofree : Type β„“β‚‚ β†’ Type β„“β‚‚
  Cofree A = π‘Š Ξ΅ (CofreeF A)

  extractβ€² : Cofree A β†’ A
  extractβ€² = head ∘ extract

  {-# TERMINATING #-}
  extendβ€² : βˆ€ {x} β†’ (Cofree A β†’ B) β†’ π‘Š x (CofreeF A) β†’ π‘Š x (CofreeF B)
  extendβ€² k xs = xs =>>[ βˆ™Ξ΅ _ ] (Ξ» x β†’ k x β—ƒ fmap (mapβ‚‚ (extendβ€² k)) (step (extract x)))

module Monadic
  {ℓ₁ β„“β‚‚} {𝑆 : Type ℓ₁} {𝑀 : 𝑆 β†’ Type β„“β‚‚ β†’ Type β„“β‚‚}
  (mon : Monoid 𝑆)
  (monad : GradedMonad mon 𝑀)
  {𝐹 : Type (ℓ₁ β„“βŠ” β„“β‚‚) β†’ Type β„“β‚‚}
  (alternative : Alternative 𝐹) where

  open Monoid mon
  open GradedMonad monad renaming ( map to mmap)
  open Alternative alternative renaming (map to fmap)

  record CofreeF (A : Type β„“β‚‚) : Type β„“β‚‚ where
    pattern
    constructor _β—ƒ_
    inductive
    field
      head : A
      step : 𝐹 (βˆƒ y Γ— 𝑀 y (CofreeF A))
  open CofreeF public

  Cofree : Type β„“β‚‚ β†’ Type β„“β‚‚
  Cofree A = 𝑀 Ξ΅ (CofreeF A)

  returnβ€² : A β†’ Cofree A
  returnβ€² x = return (x β—ƒ 0#)

  {-# TERMINATING #-}
  bindβ€² : βˆ€ {x} β†’ (A β†’ Cofree B) β†’ 𝑀 x (CofreeF A) β†’ 𝑀 x (CofreeF B)
  bindβ€² k xs = xs >>=[ βˆ™Ξ΅ _ ]
    Ξ» { (x β—ƒ xs) β†’ mmap (Ξ» { (y β—ƒ ys) β†’  y β—ƒ (ys <|> fmap (mapβ‚‚ (bindβ€² k)) xs) }) (k x) }