Require Import Vectors.Vector.


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)
                              }.
  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__) _ _ _.

  Definition traverse `{T : Traversable} `{@Applicative G} {t u} : (t -> G u) -> F t -> G (F u) :=
    let f := T _ (t_f__) in fun f ft => sequence (fmap f ft).
End ExtCT.
Section VectorU.
  Import VectorNotations.
  Program Definition vFunctor {n} : @Functor__Dict (fun t => Vector.t t n)  := {| fmap__ _ _ f := map f;
                                                                            |}.
  Next Obligation. induction ft; simpl; f_equal; auto. Defined.
  Next Obligation. induction fa; simpl; f_equal; auto. Defined.
  Global Instance vector_Functor {n} : @Functor (fun t => Vector.t t n) := fun r f => f vFunctor.

  Definition vPointed : @Pointed__Dict (fun t => Vector.t t 0) := {| point__ := nil |}.
  Global Instance vector_Pointed : @Pointed (fun t => Vector.t t 0) := fun r f => f vPointed.

  Definition vPure : @Pure__Dict (fun t => Vector.t t 1) := {| pure__ _ x := [x] |}.
  Global Instance vector_Pure : @Pure (fun t => Vector.t t 1) := fun r f => f vPure.

  Definition vSequence {G} {n} `{Applicative G} : forall T, Vector.t (G T) n -> G (Vector.t T n).
    intros. induction X; pose proof _f as f; pose proof _p as p. apply pure; trivial. apply (@point (fun f => Vector.t f 0) _ _). eapply ap. apply (fmap (fun a b => a :: b) h). exact IHX.
  Defined.
  Definition vTraversable {G} {n} : @Traversable__Dict (fun t => Vector.t t n) G := {| sequence__ _ := vSequence;
                                                                                    traverse__ _ _ _ := fun f ft => vSequence _ (fmap f ft)
                                                                                 |}.
  Global Instance vector_Traversable {n} {G} : @Traversable (fun t => Vector.t t n) G := fun r f => f vTraversable.
End VectorU.
Section ListU.
  Require Import Lists.List.
  Import ListNotations.
  Definition lFunctor : @Functor__Dict list := {| fmap__ := map;
                                                  fmap_id__ := map_id;
                                                  fmap_fusion__ := map_map
                                               |}.
  Global Instance list_Functor : @Functor list := fun r f => f lFunctor.

  Definition lPointed : @Pointed__Dict list := {| point__ := @nil |}.
  Global Instance list_Pointed : @Pointed list := fun r f => f lPointed.

  Definition lPure : @Pure__Dict list := {| pure__ _ a := [a] |}.
  Global Instance list_Pure : @Pure list := fun r f => f lPure.

  Definition lApp : @Applicative__Dict list := {| zip__ := @combine |}.
  Global Instance list_Applicative : @Applicative list := fun r f => f lApp.
End ListU.
Section Demo.
Import ListNotations.
Inductive t1 : Set :=
| a1 : t1
| a2 {n} : Vector.t t1 n -> t1
| a3 {n} : Vector.t t2 n -> t1
with t2 : Set :=
     | b1 : t2
     | b2 {n} : Vector.t t1 n -> t2
     | b3 {n} : Vector.t t2 n -> t2.

Inductive t3 : Set :=
| c1 : t3 -> t3 -> t3
| c2 {n} : Vector.t t1 n -> t3
| c3 {n} : Vector.t t2 n -> t3.

Inductive t4 : Set :=
| d1 : t4
| d2 : t4 -> t4 -> t4
| d3 {n} : Vector.t t4 n -> t4
| d4 {n} : Vector.t t4 n -> t4.

(** works *)
Fixpoint f1 f : list t1 :=
  match f with
  | d1 => [a1]
  | d2 x x0 => f1 x ++ f1 x0
  | d3 x => map a2 (sequence (Vector.map f1 x))
  | d4 x => map a3 (sequence (Vector.map f2 x))
  end
with f2 f : list t2 :=
  match f with
  | d1 => [b1]
  | d2 x x0 => f2 x ++ f2 x0
  | d3 x => map b2 (sequence (Vector.map f1 x))
  | d4 x => map b3 (sequence (Vector.map f2 x))
  end.

(** should ideally work *)
Fail Fixpoint f1' f : list t1 :=
  match f with
  | d1 => [a1]
  | d2 x x0 => f1' x ++ f1' x0
  | d3 x => map a2 (traverse f1' x)
  | d4 x => map a3 (traverse f2' x)
  end
with f2' f : list t2 :=
  match f with
  | d1 => [b1]
  | d2 x x0 => f2' x ++ f2' x0
  | d3 x => map b2 (traverse f1' x)
  | d4 x => map b3 (traverse f2' x)
  end.

(** should alternatively work *)
Fail Fixpoint f1'' f : list t1 :=
  match f with
  | d1 => [a1]
  | d2 x x0 => f1'' x ++ f1'' x0
  | d3 x => map a2 (traverse' f1'' x)
  | d4 x => map a3 (traverse' f2'' x)
  end
with f2'' f : list t2 :=
  match f with
  | d1 => [b1]
  | d2 x x0 => f2'' x ++ f2'' x0
  | d3 x => map b2 (traverse' f1'' x)
  | d4 x => map b3 (traverse' f2'' x)
  end.

End Demo.