Reader_Equivalence.v

(** We aim to show that the classic Reader monad is equivalent
    to an ADT (more precisely a GADT (Generalized Algebraic Data Types).
 *)

Section ForStephane.

(** The reader config type (what's read)
  *
  * trait Config
  *)
Variable Config : Type.

(** The classic definition of the reader monad
  *
  * type ReaderFun[+A] = Config => A
  *)
Definition ReaderFun (A: Type): Type := Config -> A.


(** How to run the reader monad given a configuration
  *
  * def runFun[A](reader: ReaderFun[A], config: Config): A = reader(config)
  *)
Definition runFun {A : Type} (reader: ReaderFun A) (c: Config): A :=
  reader c
.

(** A candidate for reader monad as GADT
  * 
  * sealed abstract class ReaderADT[+A]
  * final case object Get                                                      extends ReaderADT[Config]
  * final case class  Pure[+A](value: A)                                       extends ReaderADT[A]
  * final case class  FlatMap[X,+A](arg: ReaderADT[X], fun: X => ReaderADT[A]) extends ReaderADT[A]
  *)
Inductive ReaderADT : Type -> Type :=
  | Get : ReaderADT Config
  | Pure: forall {A : Type}, A -> ReaderADT A
  | FlatMap : forall {A B: Type}, ReaderADT A -> (A -> ReaderADT B) -> ReaderADT B
.

(** How to run this GADT reader monad
  *
  * def runADT[A](reader: ReaderADT[A], config: Config): A =
  *   reader match {
  *     case Get => config
  *     case Pure(a) => a
  *     case FlatMap(r,f) => runADT(f(runADT(reader, config)), config)
  *   }
  *)
Fixpoint runADT {A : Type} (reader: ReaderADT A) (c: Config) {struct reader} : A :=
  match reader with 
     Get => c
   | Pure a => a
   | FlatMap r f => runADT (f (runADT r c)) c
  end
.

(** Conversion from the classical definition to the GADT one
  *
  * def fun2adt[A](reader: ReaderFun[A]): ReaderADT[A] =
  *   FlatMap(Get, (c: Config) => Pure(reader(c)))
  *)
Definition fun2adt {A: Type} (reader: ReaderFun A): ReaderADT A :=
    FlatMap Get (fun (c: Config) => Pure (reader c))
.

(** Conversion from the GADT definition to the classical one
  *
  * def adt2fun[A](reader: ReaderADT[A]): ReaderFun[A] =
  *  runADT(reader, _)
  *)
Definition adt2fun {A: Type} (reader: ReaderADT A): ReaderFun A :=
  runADT reader
.

(** Now we need to prove that these two definitions are equivalent.
  * Note that there is probably no bijection between these types.
  *
  * What we want to prove runnng a reader on one side gives the
  * same result as converting it to the other side and then running
  * it there.
  *
  * More precisely runFun == runADT o fun2adt
  *            and runADT == runFun o adt2fun
  *)

(** One side of the eqvuialence *)
Theorem fun2adtEquiv: forall (A: Type) (c: Config) (reader: ReaderFun A),
                        runFun reader c = runADT (fun2adt reader) c.
Proof.
auto.
Defined.

(** The other side *)
Theorem adt2funEquiv: forall (A: Type) (c: Config) (reader: ReaderADT A),
                        runADT reader c = runFun (adt2fun reader) c.
Proof.
auto.
Defined.

(** Going from Fun to ADT and back again into Fun ... *)
Definition fun2fun {A: Type} (r: ReaderFun A): ReaderFun A := adt2fun (fun2adt r).

(** ... is the identity! *)
Theorem funEquivId {A: Type} : forall (r: ReaderFun A), fun2fun r = r.
Proof.
auto.
Defined.

(** Going from ADT to Fun and back again into ADT ... *)
Definition adt2adt {A: Type} (r: ReaderADT A): ReaderADT A := fun2adt (adt2fun r).

(** is not identity but equivalent to! *)
Theorem adtEquivId {A: Type} : forall (r: ReaderADT A) (c: Config), runADT (adt2adt r) c = runADT r c.
Proof.
auto.
Defined.

End ForStephane.