weirdsli.v

Parameter m w : Type -> Type.

Parameter fmap_w : forall {a b}, (a -> b) -> w a -> w b.
Parameter fmap_m : forall {a b}, (a -> b) -> m a -> m b.

Parameter pure : forall {a}, a -> m a.
Parameter subst : forall {a b}, (a -> m b) -> m a -> m b.
(* subst = flip (>>=) *)

Parameter extract : forall {a}, w a -> a.
Parameter extend : forall {a b}, (w a -> b) -> w a -> w b.

Parameter distribute : forall {a}, w (m a) -> m (w a).

Definition WKleisli (a b : Type) := w a -> m b.

Definition id {a} : WKleisli a a :=
  fun x => pure (extract x).

Definition comp {a b c} : WKleisli b c -> WKleisli a b -> WKleisli a c :=
  fun f g x =>
    subst f (distribute (extend g x)).

Definition funeq {a b} (f g : WKleisli a b) : Prop :=
  forall x, f x = g x.

Infix "=+" := funeq (at level 40).

(* Monad laws *)
Parameter subst_pure : forall a (u : m a),
    subst pure u = u.
Parameter subst_pure_r : forall a b (x : a) (f : a -> m b),
    subst f (pure x) = f x.
Parameter subst_subst : forall a b c (f : a -> m b) (g : b -> m c) (u : m a),
    subst g (subst f u) = subst (fun x => subst g (f x)) u.

Parameter subst_pure_f : forall a b (f : a -> b) (u : m a),
    subst (fun x => pure (f x)) u = fmap_m f u.

(* Comonad laws *)
Parameter extend_extract_f : forall a b (f : a -> b) (u : w a),
    extend (fun x => f (extract x)) u = fmap_w f u.
Parameter extract_extend : forall a b (f : w a -> b) (u : w a),
    extract (extend f u) = f u.

Parameter extend_extend : forall a b c (f : w a -> b) (g : w b -> c) (u : w a),
    extend g (extend f u) = extend (fun x => g (extend f x)) u.

(* Extra laws *)
Parameter distribute_pure : forall {a} (x : w a),
    distribute (fmap_w pure x) = pure x.

Parameter distribute_extract : forall {a} (u : w (m a)),
    fmap_m extract (distribute u) = extract u.

Lemma wtf:
  forall (a b c : Type) (f : WKleisli a b) (g : WKleisli b c) (x : w a),
    subst (fun x0 : w b => distribute (extend g x0)) (distribute (extend f x)) =
    distribute (extend (fun y : w (m b) => subst g (distribute y)) (extend f x)).
Proof.
  intros a b c f g x.
Admitted.

Infix "=<<" := subst (at level 70).
Infix "<<=" := extend (at level 70).

(*
    distribute (fmap_w pure x) = pure x.

    fmap_m extract (distribute u) = extract u.

    ((distribute . (g <<=)) =<< distribute (f <<= x))
    =
    distribute ((g =<<) . distribute y) <<= (f <<= x)
*)

(* Category laws (proofs) *)

Lemma comp_id {a b} (f : WKleisli a b) : comp f id =+ f.
Proof.
  intros x. unfold comp, id.
  rewrite extend_extract_f.
  rewrite distribute_pure.
  rewrite subst_pure_r.
  reflexivity.
Qed.

Lemma id_comp {a b} (f : WKleisli a b) : comp id f =+ f.
Proof.
  intros x. unfold comp, id.
  rewrite subst_pure_f.
  rewrite distribute_extract.
  rewrite extract_extend.
  reflexivity.
Qed.

Lemma comp_comp {a b c d} (f : WKleisli a b) (g : WKleisli b c) (h : WKleisli c d)
  : comp (comp h g) f =+ comp h (comp g f).
Proof.
  intros x. unfold comp.
  rewrite <- subst_subst.
  rewrite <- (extend_extend _ _ _ f (fun y => subst g (distribute y))).
  rewrite wtf.
  reflexivity.
Qed.