Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- 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.
Add Comment
Please, Sign In to add comment