Higher effects

{-# OPTIONS --type-in-type #-}

-- This post is also available at https://github.com/effectfully/blog/blob/master/HEff.agda
-- in the case it renders incorrectly.
-- This post is a sequel of the previous post [1]. There we've seen how simple algebraic effects
-- can be modeled in a dependently typed language. This time we'll see how Idris-like
-- resource-dependent effects [2] can be defined such that the non-termination and
-- "Codensity" effects are expressible too. The reader is assumed to be familiar with Idris effects.

module HEff where

-- Some prelude first.

open import Function
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Data.Empty
open import Data.Unit.Base
open import Data.Nat.Base
open import Data.Sum
open import Data.Product as Product
open import Data.List.Base hiding ([_])

module Prelude where
  infix 3 _∈_ _∈₁_ _∈²_
  infix 4 [_]_≅_

  instance
    inj₁-instance : ∀ {A B} {{x : A}} -> A ⊎ B
    inj₁-instance {{x}} = inj₁ x

    inj₂-instance : ∀ {A B} {{y : B}} -> A ⊎ B
    inj₂-instance {{y}} = inj₂ y

  -- See https://lists.chalmers.se/pipermail/agda/2016/009069.html
  [_]_≅_ : ∀ {A x₁ x₂} -> (B : A -> Set) -> B x₁ -> B x₂ -> Set
  [ B ] y₁ ≅ y₂ = _≡_ {A = ∃ B} (, y₁) (, y₂)

  _<×>_ : ∀ {A} -> (A -> Set) -> (A -> Set) -> A -> Set
  (B <×> C) x = B x × C x

  _∈_ : ∀ {A} -> A -> List A -> Set
  y ∈ []     = ⊥
  y ∈ x ∷ xs = y ≡ x ⊎ y ∈ xs

  -- `List₁` is defined as a function rather than a data, because this way we get
  -- eta-expansion for free. I'm not sure if this is needed in the code below,
  -- but it was needed when I was writing a library some time ago.
  List₁ : ∀ {A} -> (A -> Set) -> List A -> Set
  List₁ B  []      = ⊤
  List₁ B (x ∷ xs) = B x × List₁ B xs

  head₁ : ∀ {A} {B : A -> Set} {x xs} -> List₁ B (x ∷ xs) -> B x
  head₁ (y , ys) = y

  tail₁ : ∀ {A} {B : A -> Set} {x xs} -> List₁ B (x ∷ xs) -> List₁ B xs
  tail₁ (y , ys) = ys

  _∈₁_ : ∀ {A x xs} {B : A -> Set} -> B x -> List₁ B xs -> Set
  _∈₁_ {xs = []   }     z  tt      = ⊥
  _∈₁_ {xs = _ ∷ _} {B} z (y , ys) = [ B ] y ≅ z ⊎ z ∈₁ ys

  replace₁ : ∀ {A} {B : A -> Set} {x} {xs : List A} {y : B x} {ys : List₁ B xs}
           -> B x -> y ∈₁ ys -> List₁ B xs
  replace₁ {xs = []   } {ys = tt    } z  ()
  replace₁ {xs = _ ∷ _} {ys = y , ys} z (inj₁ refl) = z , ys
  replace₁ {xs = _ ∷ _} {ys = y , ys} z (inj₂ p)    = y , replace₁ z p

  -- `x , y ∈² xs , ys` is a proof that `x` occurs at the same index in `xs` as `y` in `ys`.
  _∈²_ : ∀ {A x xs} {B C : A -> Set} -> B x × C x -> List₁ B xs × List₁ C xs -> Set
  _∈²_ {xs = []   }         (y₁ , z₁) (tt        , tt       ) = ⊥
  _∈²_ {xs = _ ∷ _} {B} {C} (y₁ , z₁) ((y₂ , ys) , (z₂ , zs)) =
    [ B <×> C ] (y₁ , z₁) ≅ (y₂ , z₂) ⊎ y₁ , z₁ ∈² ys , zs

  to∈₁ : ∀ {A x xs} {B C : A -> Set} {y : B x} {z : C x} {ys : List₁ B xs} {zs : List₁ C xs}
       -> y , z ∈² ys , zs -> z ∈₁ zs
  to∈₁ {xs = []   }  ()
  to∈₁ {xs = _ ∷ _} (inj₁ refl) = inj₁ refl
  to∈₁ {xs = _ ∷ _} (inj₂ p)    = inj₂ (to∈₁ p)

  Sets : Set
  Sets = List Set

  HList : Sets -> Set
  HList = List₁ id
open Prelude

module EffectModule where
  -- The type of effects in Idris is defined like this:

  -- Effect : Type
  -- Effect = (result : Type) ->
  --          (input_resource : Type) ->
  --          (output_resource : result -> Type) -> Type

  -- We'll use a similar definition. There are two differences:
  -- 1) Since resources are not necessary types,
  -- `Effect` is parametrized by the type of its resources.
  -- 2) `input_resource` is the first argument, because it's often a parameter of some particular
  -- effect and Agda explicitly distinguishes between parameters and indices unlike Idris
  -- (and hence it's often convenient to define an effect without an `input_resource`,
  -- and bound `input_resource` in parameters telescope instead).

  -- So the definition could be

  -- Effect : Set -> Set
  -- Effect R = R -> (A : Set) -> (A -> R) -> Set

  -- where `R` is the type of resources of an effect, but we split the definition due to
  -- the parameters-indices distinction mentioned above:

  -- `Effectful` is `Effect` without `input_resource`.
  Effectful : ∀ {R} -> Set
  Effectful {R} = (A : Set) -> (A -> R) -> Set
 
  Effect : Set -> Set
  Effect R = R -> Effectful {R}

  ResourcesTypes : Set
  ResourcesTypes = Sets

  -- `Ψs : Effects Rs` is a list of effects typed over a list of resources types `Rs`.
  Effects : ResourcesTypes -> Set
  Effects = List₁ Effect

  -- `rs : Resources Rs` is a heterogeneous list of resources of types from `Rs`.
  Resources : ResourcesTypes -> Set
  Resources = HList

  -- A higher effect is an effect that is defined over a list of simple effects and
  -- transforms resources of those effects. This notion will be motivated later.
  HigherEffect : Set
  HigherEffect = ∀ {Rs} -> Effects Rs -> Effect (Resources Rs)

  HigherEffects : Set
  HigherEffects = List HigherEffect

  record HApply {Rs} (Φ : HigherEffect) (Ψs : Effects Rs) rs A rs′ : Set where
    constructor happlied
    field getHApplied : Φ Ψs rs A rs′

  -- At first I defined this as a data type, but Agda doesn't keep track of polarity of indices
  -- and thus doesn't see that `Codensity` below is strictly positive when `Unionʰᵉ` is a data.
  -- The `HApply` wrapper allows to infer `Φ` from `Unionʰᵉ (Φ ∷ Φs) Ψs Rs A rs′` just like
  -- with the data version.
  Unionʰᵉ : HigherEffects -> HigherEffect
  Unionʰᵉ  []      Ψs rs A rs′ = ⊥
  Unionʰᵉ (Φ ∷ Φs) Ψs rs A rs′ = HApply Φ Ψs rs A rs′ ⊎ Unionʰᵉ Φs Ψs rs A rs′

  -- "Constructors" of `Unionʰᵉ`.
  pattern hereʰᵉ  a = inj₁ (happlied a)
  pattern thereʰᵉ a = inj₂  a

  -- The union of simple effects is a higher effect.
  -- This is a direct counterpart of `Unionᵉ` defined in the previous post.
  data Unionᵉ : HigherEffect where
    -- Injecting an effect into some union of effects
    -- changes the resource at the position where the effect occurs (1).
    hereᵉ  : ∀ {R Rs r A r′ rs} {Ψ : Effect R} {Ψs : Effects Rs}
           -> Ψ r A r′ -> Unionᵉ (Ψ , Ψs) (r , rs) A (λ x -> r′ x , rs)
    -- Injecting an effect into some union of effects
    -- doesn't change the resources of all other effects.
    thereᵉ : ∀ {R Rs r A rs rs′} {Ψ : Effect R} {Ψs : Effects Rs}
           -> Unionᵉ Ψs rs A rs′ -> Unionᵉ (Ψ , Ψs) (r , rs) A (λ x -> r , rs′ x)

  hinj : ∀ {Φ Φs Rs rs A rs′} {Ψs : Effects Rs}
       -> Φ ∈ Φs -> Φ Ψs rs A rs′ -> Unionʰᵉ Φs Ψs rs A rs′
  hinj {Φs = []}     ()
  hinj {Φs = _ ∷ _} (inj₁ refl) = hereʰᵉ
  hinj {Φs = _ ∷ _} (inj₂ p)    = thereʰᵉ ∘ hinj p

  -- This is another way to express (1).
  inj′ : ∀ {R Rs r A r′ rs} {Ψ : Effect R} {Ψs : Effects Rs}
       -> (p : Ψ , r ∈² Ψs , rs) -> Ψ r A r′ -> Unionᵉ Ψs rs A (λ x -> replace₁ (r′ x) (to∈₁ p))
  inj′ {Rs = []}     ()
  inj′ {Rs = _ ∷ _} (inj₁ refl) = hereᵉ
  inj′ {Rs = _ ∷ _} (inj₂ p)    = thereᵉ ∘ inj′ p

  -- If an effect doesn't change its resource, then the resources of the union of effects
  -- don't change as well.
  inj : ∀ {R Rs r A rs} {Ψ : Effect R} {Ψs : Effects Rs}
      -> Ψ , r ∈² Ψs , rs -> Ψ r A (const r) -> Unionᵉ Ψs rs A (const rs)
  inj {Rs = []}     ()
  inj {Rs = _ ∷ _} (inj₁ refl) = hereᵉ
  inj {Rs = _ ∷ _} (inj₂ p)    = thereᵉ ∘ inj p
open EffectModule

module IFreerModule where
  infixl 2 _>>=_ _>=>_
  infixr 1 _>>_
  infixl 6 _<$>_ _<*>_

  -- `IFreer` is the indexed counterpart of `Freer` and it's an effect transformer too.
  -- `IFreer` is a Hoare state monad (in the sense of [3]; [4] is relevant here too).
  data IFreer {R} (Ψ : Effect R) : Effect R where
    return : ∀ {B r′} y -> IFreer Ψ (r′ y) B r′
    call   : ∀ {r A r′ B r′′} -> Ψ r A r′ -> (∀ x -> IFreer Ψ (r′ x) B r′′) -> IFreer Ψ r B r′′

  liftᶠ : ∀ {R r A r′} {Ψ : Effect R} -> Ψ r A r′ -> IFreer Ψ r A r′
  liftᶠ a = call a return

  _>>=_ : ∀ {R r B r′ C r′′} {Ψ : Effect R}
        -> IFreer Ψ r B r′ -> (∀ y -> IFreer Ψ (r′ y) C r′′) -> IFreer Ψ r C r′′
  return y >>= g = g y
  call a f >>= g = call a λ x -> f x >>= g

  _>=>_ : ∀ {R A B r₂ C r₃} {Ψ : Effect R} {r₁ : A -> R}
        -> (∀ x -> IFreer Ψ (r₁ x) B r₂)
        -> (∀ y -> IFreer Ψ (r₂ y) C r₃)
        -> (∀ x -> IFreer Ψ (r₁ x) C r₃)
  (f >=> g) x = f x >>= g

  _>>_ : ∀ {R r₁ B r₂ C r′′} {Ψ : Effect R}
       -> IFreer Ψ r₁ B (const r₂) -> IFreer Ψ r₂ C r′′ -> IFreer Ψ r₁ C r′′
  b >> c = b >>= const c

  _<$>_ : ∀ {R r₁ B r₂ C} {Ψ : Effect R}
        -> (B -> C) -> IFreer Ψ r₁ B (const r₂) -> IFreer Ψ r₁ C (const r₂)
  g <$> b = b >>= return ∘ g

  _<*>_ : ∀ {R r₁ B r₂ C r₃} {Ψ : Effect R}
        -> IFreer Ψ r₁ (B -> C) (const r₂)
        -> IFreer Ψ r₂  B       (const r₃)
        -> IFreer Ψ r₁  C       (const r₃)
  h <*> b = h >>= _<$> b

  hoistIFreer : ∀ {R r B r′} {Ψ Φ : Effect R}
              -> (∀ {r A r′} -> Ψ r A r′ -> Φ r A r′) -> IFreer Ψ r B r′ -> IFreer Φ r B r′
  hoistIFreer h (return y) = return y
  hoistIFreer h (call a f) = call (h a) λ x -> hoistIFreer h (f x)
open IFreerModule

module EffModule where
  -- Some convenience.
  pattern simple a k = call (hereʰᵉ  a) k
  pattern higher a k = call (thereʰᵉ a) k

  -- The main definition. `HEff` describes a computation over a list of simple effects
  -- and a list of higher effects that contains the `Unionᵉ` higher effect.
  -- The idea is that besides performing some local effectful calls like getting
  -- the state in a stateful computation, we can also perform some "big" effectful calls that
  -- can change resources of several simple effects. This is why `Unionᵉ` is a higher effect --
  -- it's aware of resources of simple effects and changes the row of resources
  -- (by transforming one particular resource) when a simple effectful call is performed.
  -- Unlike `Eff` in Idris `HEff` doesn't allow to change effects -- only their resources.
  HEff : HigherEffects -> HigherEffect
  HEff Φs Ψs = IFreer (Unionʰᵉ (Unionᵉ ∷ Φs) Ψs)

  hinvoke : ∀ {Φ Φs Rs rs A rs′} {Ψs : Effects Rs} {{p : Φ ∈ Φs}}
          -> Φ Ψs rs A rs′ -> HEff Φs Ψs rs A rs′
  hinvoke {{p}} = liftᶠ ∘ thereʰᵉ ∘ hinj p

  invoke′ : ∀ {Φs R Rs r A r′ rs} {Ψ : Effect R} {Ψs : Effects Rs} {{p : Ψ , r ∈² Ψs , rs}}
          -> Ψ r A r′ -> HEff Φs Ψs rs A (λ x -> replace₁ (r′ x) (to∈₁ p))
  invoke′ {{p}} = liftᶠ ∘ hereʰᵉ ∘ inj′ p

  invoke : ∀ {Φs R Rs r A rs} {Ψ : Effect R} {Ψs : Effects Rs} {{p : Ψ , r ∈² Ψs , rs}}
         -> Ψ r A (const r) -> HEff Φs Ψs rs A (const rs)
  invoke {{p}} = liftᶠ ∘ hereʰᵉ ∘ inj p

  -- An equivalent of `execEff` from the previous post, only for higher effects.
  hexecEff : ∀ {Φs Rs rs B rs′ rs′′} {Φ : HigherEffect} {Ψs : Effects Rs}
           -> (∀ y -> HEff Φs Ψs (rs′ y) B rs′′)
           -> (∀ {rs A rs′}
               -> Φ Ψs rs A rs′
               -> (∀ x -> HEff Φs Ψs (rs′ x) B rs′′)
               -> HEff Φs Ψs rs B rs′′)
           -> HEff (Φ ∷ Φs) Ψs rs B rs′
           -> HEff  Φs      Ψs rs B rs′′
  hexecEff eta phi (return y)             = eta y
  hexecEff eta phi (simple  a          k) = simple a λ x -> hexecEff eta phi (k x)
  hexecEff eta phi (higher (hereʰᵉ  a) k) = phi    a λ x -> hexecEff eta phi (k x)
  hexecEff eta phi (higher (thereʰᵉ a) k) = higher a λ x -> hexecEff eta phi (k x)

  hshift : ∀ {Φs Rs rs B rs′} {Φ : HigherEffect} {Ψs : Effects Rs}
         -> HEff Φs Ψs rs B rs′ -> HEff (Φ ∷ Φs) Ψs rs B rs′
  hshift = hoistIFreer λ
    { (hereʰᵉ  a) -> hereʰᵉ   a
    ; (thereʰᵉ a) -> thereʰᵉ (thereʰᵉ a)
    }

  -- `Eff` describes a computation with no higher effects except for `Unionᵉ`.
  -- I.e. it's the usual `Eff`.
  Eff : HigherEffect
  Eff = HEff []

  runEff : ∀ {A} -> Eff tt tt A (const tt) -> A
  runEff (return x)    = x
  runEff (simple () _)
  runEff (higher () _)
open EffModule

module StateModule where
  -- The heterogeneous state effect. Its resource is of type `Set`.
  -- `Get` doesn't changes the resource. `Put` changes the resource
  -- from `S` (the current state) to `T` (the state after `Put` is called).
  data State S : Effectful where
    Get : State S S (const S)
    Put : ∀ {T} -> T -> State S ⊤ (const T)

  get : ∀ {Φs Rs S rs} {Ψs : Effects Rs} {{p : State , S ∈² Ψs , rs}}
      -> HEff Φs Ψs rs S _
  get {{p}} = invoke {{p}} Get

  zap : ∀ {Φs Rs rs T} {Ψs : Effects Rs} S {{p : State , S ∈² Ψs , rs}}
      -> T -> HEff Φs Ψs rs ⊤ _
  zap S {{p}} = invoke′ {{p}} ∘ Put

  put : ∀ {Φs Rs S rs} {Ψs : Effects Rs} {{p : State , S ∈² Ψs , rs}}
      -> S -> HEff Φs Ψs rs ⊤ (const rs)
  put {{p}} = invoke {{p}} ∘ Put

  modify′ : ∀ {Φs Rs S rs T} {Ψs : Effects Rs} {{p : State , S ∈² Ψs , rs}}
          -> (S -> T) -> HEff Φs Ψs rs ⊤ _
  modify′ {{p}} f = get >>= zap _ {{p}} ∘ f

  modify : ∀ {Φs Rs S rs} {Ψs : Effects Rs} {{p : State , S ∈² Ψs , rs}}
         -> (S -> S) -> HEff Φs Ψs rs ⊤ _
  modify f = get >>= put ∘ f

  -- `rs′` returns a final resource of `State` and final resources of other effects, hence
  -- when the `State` effect is handled resulting computation returns a value of the same type
  -- as the original computations returns plus a final resource of `State`.
  -- I.e. this is like the usual `S -> B × S`, but, since the state is heterogeneous and
  -- can depend on the value returned, it's more like `S -> Σ B T`.
  -- Resources of all other effects remain untouched.
  execState : ∀ {Rs S rs B rs′} {Ψs : Effects Rs}
            -> S
            -> Eff (State , Ψs) (S , rs)  B                   rs′
            -> Eff  Ψs           rs      (Σ B (head₁ ∘ rs′)) (tail₁ ∘ rs′ ∘ proj₁)
  execState s (return y)            = return (y , s)
  execState s (simple (hereᵉ  a) k) with a
  ... | Get    = execState s  (k s)
  ... | Put s' = execState s' (k tt)
  execState s (simple (thereᵉ a) k) = simple a λ x -> execState s (k x)
  execState s (higher ()         k)
open StateModule

module ErrorModule where
  -- The error effect is almost the same as before, since its resource is trivial.
  data Error E : Effect ⊤ where
    Throw : E -> Error E _ ⊥ _

  -- Note that `throw` transforms initial resources into whatever other resources.
  -- Indeed, we need to be able to throws errors via the `Error` effect in any part of
  -- a computation: it's not required that initial and final resources must match --
  -- `throw` is not `return`.
  throw : ∀ {Φs Rs E rs B rs′} {Ψs : Effects Rs} {{p : Error E , tt ∈² Ψs , rs}}
        -> E -> HEff Φs Ψs rs B rs′
  throw {{p}} e = invoke {{p}} (Throw e) >>= ⊥-elim

  -- But this means that if a computation threw an error, it's not known in what state
  -- resources were. I.e. resources became existential. Therefore in order to handle `Error`,
  -- we must "deexistentialize" resources. Hence `execError` returns a computation that
  -- returns `E ⊎ B` like before, but also attaches `Resources Rs` to `E`. I.e. if a computation
  -- threw an error, then return also resources so we can make them final via `[ proj₂ , _ ]`
  execError : ∀ {Rs E rs B rs′} {Ψs : Effects Rs}
            -> Eff (Error E , Ψs) (tt , rs) B rs′
            -> Eff Ψs rs (E × Resources Rs ⊎ B) [ proj₂ , tail₁ ∘ rs′ ]′
  execError (return y)                   = return (inj₂  y)
  execError (simple (hereᵉ (Throw e)) k) = return (inj₁ (e , _))
  execError (simple (thereᵉ a       ) k) = simple a λ x -> execError (k x)
  execError (higher  ()               k)

  -- But having exisentials means there is some CPS lying around.
  -- Instead of returning resources on failing we can just handle errors such that
  -- no matter what resources are, they are always transformed to what is required.
  catchError : ∀ {Rs E rs B rs′} {Ψs : Effects Rs}
             -> Eff (Error E , Ψs) (tt , rs) B rs′
             -> (∀ {rs} -> E -> Eff Ψs rs B (tail₁ ∘ rs′))
             -> Eff Ψs rs B (tail₁ ∘ rs′)
  catchError (return y)                   h = return y
  catchError (simple (hereᵉ (Throw e)) k) h = h e
  catchError (simple (thereᵉ a       ) k) h = simple a λ x -> catchError (k x) h
  catchError (higher  ()               k) h
open ErrorModule

module StateTest where
  open import Data.Fin

  -- Here's an example.

  -- final resources producer ----------------------------|
  -- result is of type ----------------------------|      |
  -- initial resources ------------------|         |      |
  -- effects ----------|                 |         |      |
  fpred : Eff (Error ⊤ , State , tt) (tt , ℕ , tt) ℕ (λ n -> tt , Fin n , tt)
  fpred = get >>= λ
    {  0      -> throw tt
    ; (suc n) -> zap ℕ (fromℕ n) >> return (suc n)
    }

  -- `fpred` gets the current state, if it's `0`, then it throws an error,
  -- if it's `suc n`, then puts `fromℕ n` in the state and returns `suc n`.
  -- Note that the type signature of `fpred` guarantees that the value in a final state
  -- is always of type `Fin n` where `n` is what the computation returned.
  -- And indeed `fromℕ n` has type `Fin (suc n)`.
  -- If we try to return `n` instead of `suc n` we'll get the following very useful error:

  -- No instance of type
  -- ((Set , State , ℕ) ≡ (⊤ , Error ⊤ , tt) ⊎
  --  (Set , State , ℕ) ≡ (Set , State , ℕ) ⊎ ⊥)
  -- was found in scope.

  -- But if we explicitly fill the instance argument to `zap` the error becomes

  -- suc x != x of type ℕ

  -- A more general type signature for `fpred`:

  -- fpred : ∀ {Rs rs} {Ψs : Effects Rs}
  --           {{err : Error ⊤ , tt ∈² Ψs , rs}} {{st : State , ℕ ∈² Ψs , rs}}
  --       -> Eff Ψs rs ℕ (λ n -> replace₁ (Fin n) (to∈₁ st))

  -- (Having to deal with `replace₁` is slightly annoying. Since resources are independent
  -- on each other, we perhaps can do better).

  -- A couple of tests:

  -- state ----------------------------------------------------------------|
  -- resources ----------------------------------------------------|       |
  -- error -------------------------------------------------|      |       |
  test₀ : (runEff ∘ execState 0 $ execError fpred) ≡ (inj₁ (tt , ℕ , tt) , 0)
  test₀ = refl

  -- state ----------------------------------------------------|
  -- result -----------------------------------------------|   |
  test₂ : (runEff ∘ execState 2 $ execError fpred) ≡ (inj₂ 2 , Fin.suc zero)
  test₂ = refl

module GeneralModule where
  -- Now general recursion stuff. Imagine a function that receives a value and returns some other
  -- value, but also performs various effectful calls and changes resources of effects.
  -- A delayed recursive call must change resources as well, because that's what an actual
  -- recursive call does. And hence we have a higher effect that transforms resources
  -- of simple effects.

  -- `General` is a true inductive family. See `rs′′` appears twice? The first one is what
  -- you pass to the effect and the second one is what a whole computation returns.
  -- I.e. a computation that has the `General A rs′ B rs′′` effect always returns `rs′′` as
  -- a final resources producer. If it pretends to return something else, then this something else
  -- unifies with `rs′′` once pattern matching on `Rec` is performed. This is just like with
  -- `x ≡ y`: you can write distinct `x` and `y` there, but once you pattern matched on `refl`,
  -- they're unified. Two appearances of `rs′` are treated similarly.
  data General {Rs} A (rs′ : A -> Resources Rs) (B : A -> Set)
               (rs′′ : ∀ {x} -> B x -> Resources Rs) : HigherEffect where
    Rec : ∀ {Ψs} x -> General A rs′ B rs′′ Ψs (rs′ x) (B x) rs′′

  -- The `λ {_} → ...` part is due to the notorious hidden-lambda bug (see [7]).
  rec : ∀ {Φs Rs A} {Ψs : Effects Rs} {rs′ : A -> Resources Rs}
          {B : A -> Set} {rs′′ : ∀ {x} -> B x -> Resources Rs}
          {{p : (λ {_} → General A rs′ B rs′′) ∈ Φs}}
      -> ∀ x -> HEff Φs Ψs (rs′ x) (B x) rs′′
  rec = hinvoke ∘ Rec

  -- A function of type `Π A Φs Ψs (λ x -> rs′ x , B x , rs′′)` is a function
  -- that receives a value of type `A`, can perform higher effects from `Φs` and
  -- simple effects from Ψs. Its initial resources of effects are `rs′ x` for the `x` received,
  -- it returns `B x` (for the same `x`) and the final resources producer is `rs′′`.
  Π : ∀ {Rs}
    -> (A : Set)
    -> HigherEffects
    -> Effects Rs
    -> (A -> Resources Rs × Σ Set λ B -> B -> Resources Rs)
    -> Set
  Π A Φs Ψs F = ∀ x -> let rs , B , rs′ = F x in
    HEff (General A (proj₁ ∘ F) (proj₁ ∘ proj₂ ∘ F) (proj₂ $ proj₂ (F _)) ∷ Φs) Ψs rs B rs′

  -- At the value level the next three functions are just the same as their non-dependent
  -- counterparts from the previous post.
  execGeneral : ∀ {Φs Rs A x} {Ψs : Effects Rs} {rs′ : A -> Resources Rs}
                  {B : A -> Set} {rs′′ : ∀ {x} -> B x -> Resources Rs}
              -> (∀ x -> HEff Φs Ψs (rs′ x) (B x) rs′′)
              -> HEff (General A rs′ B rs′′ ∷ Φs) Ψs (rs′ x) (B x) rs′′
              -> HEff  Φs                         Ψs (rs′ x) (B x) rs′′
  execGeneral {Φs} {Rs} {A} {x} {Ψs} {rs′} {B} {rs′′} f = hexecEff return h where
    -- This is where the aforementioned unification plays its role.
    -- Pattern matching on `Rec` reveals that universally quantified `rs` is actually `rs′ x`
    -- and the final resources producers are unified too.
    h : ∀ {rs Bx rs′′′}
      -> General A rs′ B rs′′ Ψs rs Bx rs′′′
      -> ((y : Bx) -> HEff Φs Ψs (rs′′′ y) (B x) rs′′)
      -> HEff Φs Ψs rs (B x) rs′′
    h (Rec x) k = f x >>= k

  {-# NON_TERMINATING #-}
  execApply : ∀ {Φs Rs A F} {Ψs : Effects Rs} -> Π A Φs Ψs F -> ∀ x -> HEff Φs Ψs _ _ _
  execApply f x = execGeneral (execApply f) (f x)

  execPetrol : ∀ {Φs Rs A} {Ψs : Effects Rs} {F} {{p : ∀ {x} -> Error ⊤ , tt ∈² Ψs , proj₁ (F x)}}
             -> ℕ -> Π A Φs Ψs F -> ∀ x -> HEff Φs Ψs _ _ _
  execPetrol  0      f x = throw tt
  execPetrol (suc n) f x = execGeneral (λ x -> execPetrol n f x) (f x)
open GeneralModule

module TestGeneral where
  open import Data.Fin hiding (_+_)
  open import Data.Vec as Vec hiding (_>>=_; sum)

  -- Here is a contrived example.
  -- The type level reads as follows: `ones` receives a number and returns an effectful
  -- computation that has the `State` and `General` effects; initially, a `Fin (suc n)` is
  -- in the state; the computation returns a list of numbers `xs` and puts
  -- a `Vec ℕ n × Fin (suc (sum xs))` into the state.
  -- At the value level `ones` performs delayed recursive calls until the `Fin` in the state is
  -- `zero`. An argument to delayed recursive calls grows at each call (from `n` to `suc n`).
  -- When a `Fin` becomes `zero`, we put a vector of `0`s and `zero` into the state.
  -- But since `n` was grown, the length of the vector is greater than original `n` and
  -- hence after each delayed recursive call we truncate the vector (and also grow a `Fin`):
  -- the `modify′ {{p}} (Product.map Vec.tail suc)` part. In order to be able to grow a `Fin`,
  -- we must prepend `1` to the resulting list, because `suc` transforms a `Fin n` into a
  -- `Fin (suc n)` and we can't violate the guarantees provided by type signature.
  -- So `ones` truncates the `Fin` in the state before each recursive call, performs the call
  -- and grows the `Fin` back, thus the `Fin` in a final state is always the same as in an initial.
  ones : ∀ {Rs} {Ψs : Effects Rs} {rs : Resources Rs}
       -> Π ℕ [] (State , Ψs) λ n -> (Fin (suc n) , rs)
                                   , List ℕ
                                   , λ xs -> (Vec ℕ n × Fin (suc (sum xs))) , rs
  ones n = get {{p}} >>= λ
    {  zero   -> zap _ {{p}} (Vec.replicate 0 , zero) >> return []
    ; (suc i) -> zap _ {{p}} (inject₁ (inject₁ i)) >>
                 rec {{p}} (suc n) >>= λ xs ->
                 modify′ {{p}} (Product.map Vec.tail suc) >>
                 return (1 ∷ xs)
    } where pattern p = inj₁ refl

  -- `p` is a number of steps to perform, `i` is an initial `Fin` in the state.
  run : ℕ -> Fin 4 -> ⊤ × ⊤ ⊎ ∃ λ xs -> Vec ℕ 3 × Fin (suc (sum xs))
  run p i = runEff ∘ execError ∘ execState i $ execPetrol p ones 3

  test₀ : ∀ {n} -> run (suc n) zero ≡ inj₂ ([] , 0 ∷ 0 ∷ 0 ∷ [] , zero)
  test₀ = refl

  test₁ : run 2 (suc zero) ≡ inj₂ (1 ∷ [] , 0 ∷ 0 ∷ 0 ∷ [] , suc zero)
  test₁ = refl

  test₂ : ∀ {n} -> run (3 + n) (suc (suc zero)) ≡ inj₂ (1 ∷ 1 ∷ [] , 0 ∷ 0 ∷ 0 ∷ [] , suc (suc zero))
  test₂ = refl

  test₃ : run 3 (suc (suc (suc zero))) ≡ inj₁ (tt , tt)
  test₃ = refl

module CodensityModule where
  infixl 2 _⟨>>=⟩_ _⟨>>=⟩′_
  infixr 1 _⟨>>⟩_

  -- Let's see another example of a higher effect.

  -- Free monads and their relatives are known to be inefficient wrt left-nested binds.
  -- The situation is similar to that of lists: left-nested appends result in quadratic performance,
  -- while right-nested appends have linear performance. A common way to mitigate the situation
  -- is to use difference lists: they have O(1) append and it takes O(n) time to reify a difference
  -- list into an actual one. The same trick can be used to improve performance of free monads and
  -- that's what [5] does.
  -- [6] takes a different perspective: instead of performing binds the authors chose to collect
  -- them in a data type which gives same O(1) `bind`. Their approach is much smarter than what
  -- I'm going to show and I believe it should be adopted in a practical library (there would be
  -- termination checking issues, but they probably can be solved with sized types), but
  -- nevertheless this example is nice.

  -- Here is the effect. Looks quite intimidating, right? But the idea is simple: we package
  -- an effectful computation (which has this same `Codensity` effect too) with a bind continuation
  -- instead of actually performing `_>>=_`.
  data Codensity Φs : HigherEffect where
    Bind : ∀ {Rs rs B rs′ C rs′′} {Ψs : Effects Rs}
         -> HEff (Codensity Φs ∷ Φs) Ψs rs B rs′
         -> (∀ y -> HEff Φs Ψs (rs′ y) C rs′′)
         -> Codensity Φs Ψs rs C rs′′

  -- And this is what we get on invoking `Bind`. The idea is that left-nested calls to `_⟨>>=⟩_`
  -- stack via the `Codensity` effect instead of being computed like with `_>>=_`.
  -- Right-nested calls are disallowed so far, since the bind continuation doesn't have the
  -- `Codensity` effect.
  _⟨>>=⟩_ : ∀ {Φs Rs rs B rs′ C rs′′} {Ψs : Effects Rs} 
          -> HEff (Codensity Φs ∷ Φs) Ψs rs B rs′
          -> (∀ y -> HEff Φs Ψs (rs′ y) C rs′′)
          -> HEff (Codensity Φs ∷ Φs) Ψs rs C rs′′
  b ⟨>>=⟩ g = hinvoke (Bind b g)

  _⟨>>⟩_ : ∀ {Φs Rs rs₁ B rs₂ C rs′′} {Ψs : Effects Rs} 
         -> HEff (Codensity Φs ∷ Φs) Ψs rs₁ B (const rs₂)
         -> HEff  Φs                 Ψs rs₂ C  rs′′
         -> HEff (Codensity Φs ∷ Φs) Ψs rs₁ C  rs′′
  b ⟨>>⟩ c = b ⟨>>=⟩ const c

  -- Here we reassociate binds via CPS by growing the `k₃` continuation.
  -- Just like with difference lists.
  bindCodensity : ∀ {Φs Rs rs B rs′ C rs′′} {Ψs : Effects Rs}
                -> HEff (Codensity Φs ∷ Φs) Ψs rs B rs′
                -> (∀ y -> HEff Φs Ψs (rs′ y) C rs′′)
                -> HEff Φs Ψs rs C rs′′
  bindCodensity (return y)                       k₃ = k₃ y
  bindCodensity (simple  a                   k₂) k₃ = simple a λ x -> bindCodensity (k₂ x) k₃
  bindCodensity (higher (hereʰᵉ (Bind a k₁)) k₂) k₃ =
    bindCodensity a (k₁ >=> λ x -> bindCodensity (k₂ x) k₃)
  bindCodensity (higher (thereʰᵉ a)          k₂) k₃ = higher a λ x -> bindCodensity (k₂ x) k₃

  execCodensity : ∀ {Φs Rs rs B rs′} {Ψs : Effects Rs}
                -> HEff (Codensity Φs ∷ Φs) Ψs rs B rs′ -> HEff Φs Ψs rs B rs′
  execCodensity b = bindCodensity b return

  -- We can also have right-nested computations with the `Codensity` effect.
  -- I don't know if we lose much by handling `Codenisty` so early or not, though.
  _⟨>>=⟩′_ : ∀ {Φs Rs rs B rs′ C rs′′} {Ψs : Effects Rs} 
           -> HEff (Codensity Φs ∷ Φs) Ψs rs B rs′
           -> (∀ y -> HEff (Codensity Φs ∷ Φs) Ψs (rs′ y) C rs′′)
           -> HEff (Codensity Φs ∷ Φs) Ψs rs C rs′′
  b ⟨>>=⟩′ g = b ⟨>>=⟩ execCodensity ∘ g
open CodensityModule

module TestCodensity where
  -- This is `replicateM` that generates left-nested `_>>_`s.
  replicateLeftM : ∀ {Φs Rs rs B} {Ψs : Effects Rs} 
                 -> ℕ -> HEff Φs Ψs rs B (const rs) -> HEff Φs Ψs rs ⊤ (const rs)
  replicateLeftM {Φs} {Rs} {rs} {B} {Ψs} n e = go n eₜₜ where
    eₜₜ = _ <$> e

    go : ℕ -> HEff Φs Ψs rs ⊤ (const rs) -> HEff Φs Ψs rs ⊤ (const rs)
    go  0      a = return tt
    go  1      a = a
    go (suc n) a = go n (a >> eₜₜ)

  -- This is `replicateM` that generates left-nested `_⟨>>⟩_`s.
  replicateCoLeftM : ∀ {Φs Rs rs B} {Ψs : Effects Rs} 
                   -> ℕ
                   -> HEff  Φs                 Ψs rs B (const rs)
                   -> HEff (Codensity Φs ∷ Φs) Ψs rs ⊤ (const rs)
  replicateCoLeftM {Φs} {Rs} {rs} {B} {Ψs} n e = go n (hshift eₜₜ) where
    eₜₜ = _ <$> e

    go : ℕ
       -> HEff (Codensity Φs ∷ Φs) Ψs rs ⊤ (const rs)
       -> HEff (Codensity Φs ∷ Φs) Ψs rs ⊤ (const rs)
    go  0      a = return tt
    go  1      a = a
    go (suc n) a = go n (a ⟨>>⟩ eₜₜ)

  -- Uncomment this and memory consumption will grow from 117 MB to 880 MB.
  -- test₁ : (proj₂ ∘ runEff ∘ execState 0 ∘ replicateLeftM 80 $ modify suc) ≡ 80
  -- test₁ = refl

  -- Uncomment this and memory consumption will grow from 117 MB to 160 MB.
  -- This version type checks much faster as expected.
  -- test₂ : (proj₂ ∘ runEff ∘ execState 0 ∘ execCodensity ∘ replicateCoLeftM 80 $ modify suc) ≡ 80
  -- test₂ = refl

module References where
  -- [1] "Turing-completeness totally freer"
  -- http://effectfully.blogspot.com/2016/12/turing-completeness-totally-freer.html

  -- [2] "The Effects Tutorial"
  -- http://docs.idris-lang.org/en/latest/effects/

  -- [3] "Inferring Precise Polymorphic Specifications for the Hoare State Monad",
  -- Cole Schlesinger and Nikhil Swamy
  -- http://research.microsoft.com/en-us/um/people/nswamy/paper.pdf

  -- [4] "The Hoare State Monad", Wouter Swierstra
  -- http://www.staff.science.uu.nl/~swier004/talks/2009-eindhoven.pdf

  -- [5] "Asymptotic Improvement of Computations over Free Monads"
  -- http://www.janis-voigtlaender.eu/papers/AsymptoticImprovementOfComputationsOverFreeMonads.pdf

  -- [6] "Freer Monads, More Extensible Effects", Oleg Kiselyov, Hiromi Ishii
  -- http://okmij.org/ftp/Haskell/extensible/more.pdf

  -- [7] "Eliminating the problems of hidden-lambda insertion", Marcus Johansson, Jesper Lloyd
  -- http://www2.tcs.ifi.lmu.de/~abel/MScThesisJohanssonLloyd.pdf