-
Notifications
You must be signed in to change notification settings - Fork 0
/
Applicative.v
139 lines (116 loc) · 5.29 KB
/
Applicative.v
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
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
(* Verification of Applicative laws for (a generalization of) SqlDecoder *)
Set Warnings "-notation-overridden,-parsing".
(* Model Monoid & Applicative in general *)
Inductive MonoidDict (M : Type) :=
| monoid_dict : M -> (M -> M -> M) -> MonoidDict M.
Arguments monoid_dict {M} _ _.
Definition MonoidLaws {M : Type} (dict : MonoidDict M) :=
match dict with
| monoid_dict mempty append =>
(forall (m : M), append mempty m = m) (* left identity *)
/\ (forall (m : M), append m mempty = m) (* right identity *)
/\ (forall (a b c : M), append a (append b c) = append (append a b) c) (* associativity *)
end.
Definition Pure F := forall A, A -> F A.
Definition App F := forall A B, F (A -> B) -> F A -> F B.
(* Definition ApplicativeDict F := (Pure F, App F). *)
Inductive ApplicativeDict F := applicative_dict : Pure F -> App F -> ApplicativeDict F.
Arguments applicative_dict {F} _ _.
(* The Monoidal type generalizes SqlDecoder, substituting any Monoid M
for the [Text], and any Applicative F for the SqlParser. *)
Inductive Monoidal (M : Type) (F : Type -> Type) (A : Type) : Type :=
| monoidal : M -> (F A) -> Monoidal M F A.
Arguments monoidal {M} {F} {A} _ _.
Definition pure_monoidal {M : Type} {F : Type -> Type}
(m_dict : MonoidDict M) (f_dict : ApplicativeDict F) : Pure (Monoidal M F) :=
match m_dict, f_dict with
| monoid_dict mempty _, applicative_dict pure_f _ =>
fun {A : Type} (a : A) => monoidal mempty (pure_f A a)
end.
Definition app_monoidal {M : Type} {F : Type -> Type}
(m_dict : MonoidDict M) (f_dict : ApplicativeDict F) : App (Monoidal M F) :=
match m_dict, f_dict with
| monoid_dict _ append, applicative_dict _ app =>
fun {A : Type} {B : Type} (mo : Monoidal M F (A -> B)) (no : Monoidal M F A) =>
match mo, no with
| monoidal m1 fab, monoidal m2 fa => monoidal (append m1 m2) (app A B fab fa)
end
end.
Definition ApplicativeMonoidal {M : Type} {F : Type -> Type}
(m_dict : MonoidDict M) (f_dict : ApplicativeDict F) : ApplicativeDict (Monoidal M F) :=
applicative_dict (pure_monoidal m_dict f_dict) (app_monoidal m_dict f_dict).
Definition identity (A : Type) (a : A) : A := a.
Definition ApplicativeIdentity {F : Type->Type} (dict : ApplicativeDict F) : Prop :=
match dict with
| applicative_dict pure app =>
forall A fa, app A A (pure (A -> A) (fun x => x)) fa = fa
end.
Theorem app_id_monoidal : forall (M : Type) (F : Type -> Type) (A : Type)
(m_dict : MonoidDict M) (m_laws : MonoidLaws m_dict)
(f_dict : ApplicativeDict F) (f_id : ApplicativeIdentity f_dict)
(v : Monoidal M F A),
ApplicativeIdentity (ApplicativeMonoidal m_dict f_dict).
Proof.
intros. destruct v.
destruct m_dict as [mempty append].
destruct m_laws as [left_id [right_id m_assoc]].
destruct f_dict as [pure app].
simpl. intros. destruct fa. rewrite left_id. rewrite f_id. reflexivity.
Qed.
Definition ApplicativeHomomorphism { F : Type -> Type} (dict : ApplicativeDict F) : Prop :=
match dict with
| applicative_dict pure app =>
forall (A B : Type) (f : A -> B) (a : A),
app A B (pure (A->B) f) (pure A a) = pure B (f a)
end.
Theorem homomorphism_monoidal : forall (M : Type) (F : Type -> Type)
(m_dict : MonoidDict M) (m_laws : MonoidLaws m_dict) (f_dict : ApplicativeDict F)
(homomorphism_f : ApplicativeHomomorphism f_dict),
ApplicativeHomomorphism (ApplicativeMonoidal m_dict f_dict).
Proof.
intros.
destruct m_dict as [mempty append].
destruct m_laws as [left_id [right_id m_assoc]].
destruct f_dict as [pure app].
simpl. intros. rewrite left_id.
(* unfold ApplicativeHomomorphism in homomorphism_f. *)
rewrite homomorphism_f. reflexivity.
Qed.
Definition andThen {A B : Type} (a : A) : (A -> B) -> B :=
fun f => f a.
Definition ApplicativeInterchange { F : Type -> Type} (dict : ApplicativeDict F) : Prop :=
match dict with
| applicative_dict pure app =>
forall (A B : Type) (u : F (A -> B)) (y : A),
app A B u (pure A y) = app (A->B) B (pure ((A->B) -> B) (andThen y) ) u
end.
Theorem interchange_monoidal : forall (M : Type) (F : Type -> Type)
(m_dict : MonoidDict M) (m_laws : MonoidLaws m_dict) (f_dict : ApplicativeDict F)
(interchange_f : ApplicativeInterchange f_dict),
ApplicativeInterchange (ApplicativeMonoidal m_dict f_dict).
Proof.
intros.
destruct m_dict as [mempty append].
destruct m_laws as [left_id [right_id m_assoc]].
destruct f_dict as [pure app].
simpl. intros. destruct u.
rewrite interchange_f. rewrite left_id, right_id. reflexivity.
Qed.
Definition ApplicativeComposition { F : Type -> Type} (dict : ApplicativeDict F) : Prop :=
match dict with
| applicative_dict pure app =>
forall (A B : Type) (u : F (A -> B)) (y : A),
app A B u (pure A y) = app (A->B) B (pure ((A->B) -> B) (andThen y) ) u
end.
Theorem composition_monoidal : forall (M : Type) (F : Type -> Type)
(m_dict : MonoidDict M) (m_laws : MonoidLaws m_dict) (f_dict : ApplicativeDict F)
(composition_f : ApplicativeComposition f_dict),
ApplicativeComposition (ApplicativeMonoidal m_dict f_dict).
Proof.
intros.
destruct m_dict as [mempty append].
destruct m_laws as [left_id [right_id m_assoc]].
destruct f_dict as [pure app].
simpl. intros. destruct u.
rewrite composition_f. rewrite left_id, right_id. reflexivity.
Qed.