tealeaves/Tealeaves/Classes/Categorical/DecoratedTraversableMonad.v at master · dunnl/tealeaves · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
From Tealeaves Require Export
  Classes.Categorical.DecoratedMonad
  Classes.Categorical.TraversableMonad
  Classes.Categorical.DecoratedTraversableFunctor.

Import Product.Notations.
Import Monad.Notations.
Import Comonad.Notations.

#[local] Generalizable Variables T F G W A B C.

(** * Decorated-traversable monads *)
(******************************************************************************)
Class DecoratedTraversableMonad
  (W : Type)
  (T : Type -> Type)
  `{op : Monoid_op W}
  `{unit : Monoid_unit W}
  `{Map T} `{Return T} `{Join T}
  `{Decorate W T} `{ApplicativeDist T} :=
  { dtmon_decorated :> DecoratedMonad W T;
    dtmon_traversable :> TraversableMonad T;
    dtmon_functor :> DecoratedTraversableFunctor W T;
  }.

(** Now we verify that the sub-classes can be inferred as well. *)
(******************************************************************************)
Section test_typeclasses.

  Context
    `{DecoratedTraversableMonad W T}.

  Goal Functor T. typeclasses eauto. Qed.
  Goal Monad T. typeclasses eauto. Qed.
  Goal DecoratedFunctor W T. typeclasses eauto. Qed.
  Goal DecoratedMonad W T. typeclasses eauto. Qed.
  Goal TraversableFunctor T. typeclasses eauto. Qed.
  Goal TraversableMonad T. typeclasses eauto. Qed.
  Goal DecoratedTraversableFunctor W T. typeclasses eauto. Qed.
(*
  Goal SetlikeFunctor T. typeclasses eauto. Qed.
  Goal SetlikeMonad T. Fail typeclasses eauto. Abort.
  Goal ListableFunctor T. typeclasses eauto. Qed.
  Goal ListableMonad T. Fail typeclasses eauto. Abort.
 *)

End test_typeclasses.