{-
(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.

The question is - can ALL manner of things one would like to be
erasable be done in this monad, such as proofs and type construction
when given erasable input?  Consider a predicate/type constructor P :
A -> Set, and the monadic value ma : M A.  What is one to do with
this?  Just fmap-ing P on ma yields M Set, which seems to be very
useless - one can't use it to declare things, for example.  Also,
there seem to be other problems (or at least major inconveniences)
when working with monadic values that are types...

-- Jonathan Leivent
-- 13-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

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

  -- 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, 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 ())

  private -- not sure of the following:
    -- 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
    -- This is scary because uniqueness doesn't necessarily imply
    -- statelessness, thus erasability.  Consider the dependent
    -- product: Σ[ n ∶ ℕ ](n ≡ f x).  Its inhabitant is unique, but
    -- seems stateful - or maybe it's stateless, since all of the
    -- "info" is tied up in the type's identity - but, is the type's
    -- identity then stateless - thinking about it hurts my brain!
    -- Otherwise, is there a general way to allow only extraction of
    -- stateless inhabitants?  How?  Or, is extract≡ sufficient?
    -- Certainly, extract! subsumes extract≡.

    -- How else to deal with types constructed in the monad?:
    setout : ∀ {i} → M (Set i) → Set i
    setout (ctor S) = S -- or, should this be M S?  
    -- As with extract!, setout is scary because I can't tell if it
    -- opens a back door to extraction of stateful information from
    -- the monad, piggy-backed on the output type somehow.  But, types
    -- are not present at runtime, so maybe this is safe.
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