open import Effect.Monad
open import Relation.Nullary using (¬_)
open import Data.Empty
open import Function

record ¬¬_ {ℓ} (A : Set ℓ) : Set ℓ where
  constructor ⟨_⟩
  field
    run : ¬ ¬ A
open ¬¬_

¬¬¬⊥ : ¬ (¬¬ ⊥)
¬¬¬⊥ x = run x id

distribute : ∀ {ℓ} {A B : Set ℓ} → ¬¬ (A → B) → ¬¬ A → ¬¬ B
distribute ¬¬A→B ¬¬A = ⟨ (λ ¬B → run ¬¬A→B (λ f → run ¬¬A (λ a → ¬B (f a)))) ⟩

dn-monad : ∀ {ℓ} → RawMonad {ℓ} ¬¬_
dn-monad = mkRawMonad ¬¬_
  (λ a → ⟨ (λ ¬a → ¬a a) ⟩)
  λ ¬¬a f → ⟨ (λ ¬b → run ¬¬a (λ a → run (f a) ¬b)) ⟩

module _ {ℓ} where
  open RawMonad {ℓ} dn-monad

  distribute-m : ∀ {A B : Set ℓ} → ¬¬ (A → B) → ¬¬ A → ¬¬ B
  distribute-m ¬¬A→B ¬¬A = ¬¬A→B >>= λ f → ¬¬A >>= λ a → pure (f a)

  distribute-do : ∀ {A B : Set ℓ} → ¬¬ (A → B) → ¬¬ A → ¬¬ B
  distribute-do ¬¬A→B ¬¬A =
    do
      f ← ¬¬A→B
      a ← ¬¬A
      pure (f a)