CT.v

Require Import Vectors.Vector.

Import VectorNotations.
Section CT.
  Context {F : Type -> Type}.
  Record Functor__Dict := {
                           fmap__ {a b} : (a -> b) -> F a -> F b;
                           fmap_id__ {t} : forall ft, fmap__ (fun a : t => a) ft = ft;
                           fmap_fusion__ {a b c} : forall (f : a -> b) (g : b -> c) fa, fmap__ g (fmap__ f fa) = fmap__ (fun e => g (f e)) fa
                         }.

  Definition Functor := forall r, (Functor__Dict -> r) -> r.

  Existing Class Functor.

  Definition fmap `{f : Functor} {a b} : (a -> b) -> F a -> F b :=
    f _ (fmap__) a b.

  (* Class Functor := { fmap {a b : Set} : (a -> b) -> F a -> F b; *)
  (*                    fmap_id {t : Set} : forall ft, fmap (fun a : t => a) ft = ft; *)
  (*                    fmap_fusion {a b c : Set} : forall (f : a -> b) (g : b -> c) fa, fmap g (fmap f fa) = fmap (fun e => g (f e)) fa  *)
  (*                  }. *)

  Record Pure__Dict := { pure__ {t} : t -> F t }.
  
  Definition Pure := forall r , (Pure__Dict -> r) -> r.

  Existing Class Pure.

  Definition pure `{p : Pure} {t} : t -> F t :=
    p _ (pure__) t.

  Record Applicative__Dict := { _f__ :> Functor;
                                _p__ :> Pure;
                                zip__ {a b} : F a -> F b -> F (a * b)%type;
                                ap__ {a b} : F (a -> b) -> F a -> F b := fun ff fa => fmap (fun t => match t with (f, e) => f e end) (zip__ ff fa);
                                zipWith__ {a b c} : (a -> b -> c) -> F a -> F b -> F c := fun f fa fb => ap__ (fmap f fa) fb
                              }.

  Definition Applicative :=
    forall r, (Applicative__Dict -> r) -> r.

  Existing Class Applicative.

  Definition zip `{A : Applicative} {a b} : F a -> F b -> F (a * b)%type :=
    A _ (zip__) a b.

  Definition ap `{A : Applicative} {a b} : F (a -> b) -> F a -> F b :=
    A _ (ap__) a b.

  Definition zipWith `{A : Applicative} {a b c} : (a -> b -> c) -> F a -> F b -> F c :=
    A _ (zipWith__) a b c.

  Definition _f `{A : Applicative} : Functor :=
    A _ (_f__).

  Definition _p `{A : Applicative} : Pure :=
    A _ (_p__).
  
  Record Pointed__Dict := { point__ {t} : F t }.
  Definition Pointed := forall r, (Pointed__Dict -> r) -> r.
  Existing Class Pointed.
  
  Definition point `{P : Pointed} {t} : F t :=
    P _ (point__) t.

  (* Class Monad `{Pure} := { join {t} : F (F t) -> F t }. *)
  
  (* Class MonadFilter `{Pointed} `{Monad} := { filter {t} (p : t -> bool) : F t -> F {e : t | p e = true }; *)
  (*                                          }. *)
End CT.

Section ExtCT.
  Context {F : Type -> Type} {G : Type -> Type}.
  Record Traversable__Dict := { t_f__ :> @Functor F; 
                                sequence__ `{@Applicative G} {t} : F (G t) -> G (F t);
                                traverse__ `{@Applicative G} {t u} : (t -> G u) -> F t -> G (F u) :=
                                  fun f ft => sequence__ (fmap f ft)
                              }.
  Definition Traversable := forall r, (Traversable__Dict -> r) -> r.
  Existing Class Traversable.

  Definition sequence `{T : Traversable} `{@Applicative G} {t} : F (G t) -> G (F t) :=
    T _ (sequence__) _ _.

  Definition traverse `{T: Traversable} `{@Applicative G} {t u} : (t -> G u) -> F t -> G (F u) :=
    T _ (traverse__) _ _ _.
End ExtCT.