open import Level

-- some typeclasses
record Apply (M : ∀ {ℓ} → Set ℓ → Set ℓ) (ℓ₁ ℓ₂ : Level) : Set (suc ℓ₁ ⊔ suc ℓ₂) where
  field
    _<*>_ : ∀ {t₁ : Set ℓ₁} {t₂ : Set ℓ₂} → M (t₁ → t₂) → M t₁ → M t₂

record Return (M : ∀ {ℓ} → Set ℓ → Set ℓ) (ℓ : Level) : Set (suc ℓ) where
  field
    return : ∀ (t : Set ℓ) → M t

record Bind (M : ∀ {ℓ} → Set ℓ → Set ℓ) (ℓ₁ ℓ₂ : Level) : Set (suc ℓ₁ ⊔ suc ℓ₂) where
  field
    _>>=_ : ∀ {t₁ : Set ℓ₁} {t₂ : Set ℓ₂} → M t₁ → (t₁ → M t₂) → M t₂

open Apply {{...}}
open Return {{...}}
open Bind {{...}}

-- make a nice free monad

open import Data.Container
open import Data.Container.Combinator hiding (_∘_)

private
  _⋆C_ : ∀ {c} (_ : Container c) {ℓ} → Set ℓ → Container (c ⊔ ℓ)
  _⋆C_ {c} (Shape ▷ Position) {ℓ} X = const (Lift {ℓ} {c} X) ⊎ (Lift {c} {ℓ} Shape ▷ λ x → Lift {c} {ℓ} (Position (lower x)))

  PrimFree : ∀ {ℓc} (c : Container ℓc) {ℓ} (t : Set ℓ) → Set (ℓc ⊔ ℓ)
  PrimFree c t = μ (c ⋆C t)

record Free {ℓc} (c : Container ℓc) {ℓ} (t : Set ℓ) : Set (ℓc ⊔ ℓ) where
  field
    free : PrimFree c t

-- black magic (He Who Must Not Be Named)

data Interpreter {ℓc} (c : Container ℓc) {ℓ} (t : Set ℓ) : _ where
  MkInterpreter : ∀ (_ : {M : ∀ {ℓ} → Set ℓ → Set ℓ}
                        {{_ : ∀ {ℓ₁ ℓ₂} → Apply M ℓ₁ ℓ₂}}
                        {{_ : ∀ {ℓ} → Return M ℓ}}
                        {{_ : ∀ {ℓ₁ ℓ₂} → Bind M ℓ₁ ℓ₂}}
                 → ((∀ {ℓ} {t' : Set ℓ} → Free c t' → M t') → M t)) → Interpreter c t

private
  -- helper to pull the interpreter out of our Interpreter
  extract : ∀ {ℓc} {c : Container ℓc} {ℓ} {t : Set ℓ} → Interpreter c t →
                 ∀ {M : ∀ {ℓ} → Set ℓ → Set ℓ}
                        {{_ : ∀ {ℓ₁ ℓ₂} → Apply M ℓ₁ ℓ₂}}
                        {{_ : ∀ {ℓ} → Return M ℓ}}
                        {{_ : ∀ {ℓ₁ ℓ₂} → Bind M ℓ₁ ℓ₂}}
                 → ((∀ {ℓ} {t' : Set ℓ} → Free c t' → M t') → M t)
  extract (MkInterpreter x) = x

open import Data.W
open import Data.Sum
open import Data.Empty
open import Function

-- shapes from our free monad are still usable in the interpreter
insert : ∀ {ℓ₁ ℓ₂} {t : Set ℓ₁} {c : Container ℓ₂} → (x : Shape c) → Interpreter c (Position c x)
insert {_} {_} {t} {c} v =
  let
    m : Free c (Position c v)
    m = record { free = sup (inj₂ (lift v)) (λ x → sup (inj₁ (lift (Lift.lower x))) (⊥-elim ∘ lower)) }
  in
  MkInterpreter (λ r → r m)

-- and we can define our ops
pure : ∀ {ℓ} {t : Set ℓ} {ℓc} {c : Container ℓc} → t → Interpreter c t
pure x = MkInterpreter λ r → r record { free = sup (inj₁ (lift x)) (⊥-elim ∘ lower) }

_<**>_ : ∀ {ℓ₁ ℓ₂} {t₁ : Set ℓ₁} {t₂ : Set ℓ₂} {ℓc} {c : Container ℓc} →
         Interpreter c (t₁ → t₂) → Interpreter c t₁ → Interpreter c t₂
_<**>_ (MkInterpreter f) (MkInterpreter i) = MkInterpreter (λ {{w}} r → f r <*> i r)

_>>-_ : ∀ {ℓ₁ ℓ₂} {t₁ : Set ℓ₁} {t₂ : Set ℓ₂} {ℓc} {c : Container ℓc} →
         Interpreter c t₁ → (t₁ → Interpreter c t₂) → Interpreter c t₂
_>>-_ (MkInterpreter i) f = MkInterpreter (λ r → i r >>= λ x → extract (f x) r)

-- but if you try to make these instances of our typeclass... ohno!

-- instance
--   interpreterCanBind : ∀ {ℓc} {c : Container ℓc} {ℓ₁ ℓ₂} → Bind (Interpreter c) ℓ₁ ℓ₂
--   interpreterCanBind = ?