{-
(Towards) A Monad for General Erasability

A pure monad from which only stateless information can be extracted.
This erasability doesn't produce or guarantee erasure directly - but
could if the compiler recognized (and acted on) it as such.  Which
seems possible.

-- Jonathan Leivent
-- 16-Feb-2012

This work is licensed under the Creative Commons
Attribution-ShareAlike 3.0 Unported License. To view a copy of this
license, visit http://creativecommons.org/licenses/by-sa/3.0/ or send
a letter to Creative Commons, 444 Castro Street, Suite 900, Mountain
View, California, 94041, USA.  

-} 

module ErasableMonad where

open import Level
open import Relation.Binary.PropositionalEquality
open import Data.Empty
open import Data.Product

module Hide where
  private -- make sure nothing outside Hide can see the state of Ḿ
    data Ḿ {i}(A : Set i) : Set i where
      ctor : A → Ḿ A

  -- expose Ḿ via M, but not ctor (to prevent extraction via
  -- projection), outside Hide:
  M : ∀ {i}(A : Set i) → Set i
  M A = Ḿ A

   -- Keep the following definitions abstract to make sure things like
   -- "return 0 ≡ return 1 → ⊥" can't be proved outside the monad:
  abstract
    -- return and bind are trivial and pure:
    return : ∀ {i}{A : Set i} → A → M A
    return a = (ctor a)
  
    bind : ∀ {i j}{A : Set i}{B : Set j} → M A →  (A → M B) → M B
    bind (ctor a) f = f a

    -- like bind, but provides useful proof of arg equivalence to input:
    bind≡ : ∀ {i j}{A : Set i}{B : Set j} → (ma : M A) → ((a : A) → (ma ≡ return a) → M B) → M B
    bind≡ (ctor a) f = f a refl

    -- Allow only very limited (stateless) extractions to maintain erasability:

    -- irrelevant extraction:
    .extract : ∀ {i}{A : Set i} → M A → A
    extract (ctor a) = a

    -- extraction of ≡ proofs is OK because their unique inhabitant (refl) is stateless:
    extract≡ : ∀ {i}{A : Set i}{a b : A} → M (a ≡ b) → a ≡ b
    extract≡ (ctor a) = a

    -- extraction of ⊥
    extract⊥ : M ⊥ → ⊥
    extract⊥ (ctor ())

    -- extraction of unique inhabitants, given a proof of their uniqueness:
    extract! : ∀ {i}{A : Set i} → .(∀ (a b : A) → a ≡ b) → M A → A
    extract! _ (ctor a) = a

    -- extraction of sets is OK because sets are erased at runtime:
    setout : ∀ {i} → M (Set i) → Set i
    setout (ctor S) = S 

    -- Axioms - which are neede because the above definitions are abstract
    -- first, the standard 3 monad axioms:
    Ax1 : ∀ {i j}{A : Set i}{B : Set j}(x : A)(f : A → M B) → bind (return x) f ≡ f x
    Ax1 x f = refl

    Ax2 : ∀ {i}{A : Set i}(mx : M A) → bind mx return ≡ mx
    Ax2 (ctor y) = refl

    Ax3 : ∀ {i j k}{A : Set i}{B : Set j}{C : Set k}(mx : M A)(f : A → M B)(g : B → M C) →
        bind (bind mx f) g ≡ bind mx (λ y → bind (f y) g)
    Ax3 (ctor y) f g = refl

    -- plus another for setout:
    Axs : ∀ {i}(A : Set i) → setout (return A) ≡ A
    Axs A = refl

open Hide public

-- The usual, defined as usual:
infixl 1 _>>=_
_>>=_ : ∀ {i j} {A : Set i} → {B : Set j} → M A → (A → M B) → M B
_>>=_ = bind

infixr 1 _=<<_
_=<<_ : ∀ {i j}{A : Set i}{B : Set j} → (A → M B) → M A → M B
f =<< ma = ma >>= f

fmap : ∀ {i j}{A : Set i}{B : Set j} → (A → B) → M A → M B
fmap f ma = ma >>= (λ x → return (f x))

join : ∀ {i}{A : Set i} → M (M A) → M A
join a = a >>= (λ x → x)

infixl 1 _>=>_
_>=>_ : ∀ {i j k}{A : Set i}{B : Set j}{C : Set k} → 
      (A → M B) → (B → M C) → (A → M C)
f >=> g = λ x → f x >>= g

-- some other useful functions

smap : ∀ {i j}{A : Set i} → (A → Set j) → M A → Set j
smap f ma = setout (fmap f ma)

infixl 1 _>>≡_
_>>≡_ : ∀ {i j} {A : Set i} → {B : Set j} → (ma : M A) → ((a : A) → (ma ≡ return a) → M B) → M B
_>>≡_ = bind≡