(* The SC monad (a hybrid of continuation and selection monads), monad laws, and a monad morphism from S (the selection monad) *)

Set Implicit Arguments.
Set Maximal Implicit Insertion.
Set Strict Implicit.

Record SC (s a : Type) := MkSC {
  runS : (a -> s) -> a;
  runC : (a -> s) -> s }.

Definition retSC {s a} (x : a) : SC s a :=
  MkSC (fun _ => x) (fun k => k x).

Definition bindSC {s a b} (f : SC s a) (g : a -> SC s b)
  : SC s b :=
  MkSC
    (fun k =>
      let x := runS f (fun x => runC (g x) k) in
      runS (g x) k)
    (fun k => runC f (fun x => runC (g x) k)).

(* Equivalence on SC *)
Definition eq_SC {s a} (f g : SC s a) :=
  forall k, runS f k = runS g k /\ runC f k = runC g k.

Infix "==" := eq_SC (at level 60).

Lemma bindSC_retSC {s a b} (x : a) (f : a -> SC s b) :
  bindSC (retSC x) f == f x.
Proof.
  split; reflexivity.
Qed.

Lemma bindSC_bindSC {s a b c} (f : SC s a) (g : a -> SC s b) (h : b -> SC s c) :
  bindSC (bindSC f g) h == bindSC f (fun x => bindSC (g x) h).
Proof.
  split; reflexivity.
Qed.

(* Selection monad *)
Record S (s a : Type) := MkS { unS : (a -> s) -> a }.

Definition retS {s a} (x : a) : S s a :=
  MkS (fun _ => x).

Definition bindS {s a b} (f : S s a) (g : a -> S s b)
  : S s b :=
  MkS
    (fun k =>
      let x := unS f (fun x => k (unS (g x) k)) in
      unS (g x) k).

(* Monad morphism and its laws *)
Definition morph {s a} (f : S s a) : SC s a :=
  MkSC (unS f) (fun k => k (unS f k)).

Lemma morph_retS {s a} (x : a) :
  morph (s := s) (retS x) == retSC x.
Proof.
  split; reflexivity.
Qed.

Lemma morph_bindS {s a b} (f : S s a) (g : a -> S s b) :
  morph (bindS f g) == bindSC (morph f) (fun x => morph (g x)).
Proof.
  split; reflexivity.
Qed.