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
|
Require Import MathClasses.interfaces.abstract_algebra.
Require MathClasses.theory.setoids.
Section functor_class.
Context `{Category C} `{Category D} (M: C → D).
Class Fmap: Type := fmap: ∀ {v w: C}, (v ⟶ w) → (M v ⟶ M w).
Class Functor `(Fmap): Prop :=
{ functor_from: Category C
; functor_to: Category D
; functor_morphism:: ∀ a b: C, Setoid_Morphism (@fmap _ a b)
; preserves_id: `(fmap (cat_id: a ⟶ a) = cat_id)
; preserves_comp `(f: y ⟶ z) `(g: x ⟶ y): fmap (f ◎ g) = fmap f ◎ fmap g }.
End functor_class.
Set Warnings "-unsupported-attributes". (* FIXME: remove when minimal Coq version is enough *)
#[global]
Typeclasses Transparent Fmap.
Set Warnings "+unsupported-attributes".
(* The usual notational convention for functor application is to use the
name of the functor to refer to both its object map and its arrow map, relying
on additional conventions regarding object/arrow names for disambiguation
(i.e. "F x" and "F f" map an object and an arrow, respectively, because
"x" and "f" are conventional names for objects and arrows, respectively.
In Coq, for a term F to function as though it had two different types
simultaneously (namely the object map and the arrow map), there must
either (1) be coercions from the type of F to either function, or (2) F must
be (coercible to) a single function that is able to consume both object and
arrow arguments. The following snippet shows that (1) doesn't appear to be
supported in Coq:
Section test.
Context (A B: Type).
Record R := { Ra:> A → unit; Rb:> B → unit }.
Variables (r: R) (a: A) (b: B).
Check (r a). (* ok so far *)
Check (r b). (* Error: The term "b" has type "B" while it is expected to have type "A". *)
End test.
And even if this /did/ work, we could not use it, because leaving
computational components unbundled is a key aspect of our approach.
For (2), if it could be made to work at all (which is not clear at all), F would need
a pretty egregious type considering that arrow types are indexed by objects,
and that the type of the arrow map (namely "∀ x y, (x ⟶ y) → (F x ⟶ F y)")
must refer to the object map.
We feel that these issues are not limitations of the Coq system, but merely
reflect the fact that notationally identifying these two different and interdependent
maps is a typical example of an "abus de notation" that by its very nature
is ill-suited to a formal development where software engineering concerns apply.
Hence, we do not adopt this practice, and use "fmap F" (name taken from the Haskell
standard library) to refer to the arrow map of a functor F.
TODO: Sharpen. *)
Section id_functor.
Context `{Category C}.
Global Instance: Fmap id := λ _ _, id.
Global Instance id_functor: Functor (id: C → C) _.
Proof.
constructor; try reflexivity; try apply _.
Qed.
End id_functor.
Section compose_functors.
Context
A B C
`{!Arrows A} `{!Arrows B} `{!Arrows C}
`{!CatId A} `{!CatId B} `{!CatId C}
`{!CatComp A} `{!CatComp B} `{!CatComp C}
`{∀ x y: A, Equiv (x ⟶ y)}
`{∀ x y: B, Equiv (x ⟶ y)}
`{∀ x y: C, Equiv (x ⟶ y)}
`{!Functor (f: B → C) f'} `{!Functor (g: A → B) g'}.
Global Instance comp_Fmap: Fmap (f ∘ g) := λ _ _, fmap f ∘ fmap g.
Global Instance compose_functors: Functor (f ∘ g) _.
Proof with intuition; try apply _.
pose proof (functor_from g).
pose proof (functor_to g).
pose proof (functor_to f).
constructor; intros; try apply _.
apply (@setoids.compose_setoid_morphism _ _ _ _ _ _)...
apply (@functor_morphism _ _ _ _ _ _ _ _ _ _ f _)...
(* todo: this part really should be automatic *)
change (fmap f (fmap g (cat_id: a ⟶ a)) = cat_id).
repeat try rewrite preserves_id...
change (fmap f (fmap g (f0 ◎ g0)) = fmap f (fmap g f0) ◎ fmap f (fmap g g0)).
repeat try rewrite preserves_comp...
Qed.
End compose_functors.
(** The Functor class is nice and abstract and theory-friendly, but not as convenient
to use for regular programming as Haskell's Functor class. The reason for this is that
our Functor is parameterized on two Categories, which by necessity bundle setoid-
ness and setoid-morphism-ness into objects and arrows, respectively.
The Haskell Functor class, by contrast, is essentially specialized for endofunctors on
the category of Haskell types and functions between them. The latter corresponds to our
setoid.Object category.
To recover convenience, we introduce a second functor type class tailored specifically to
functors of this kind. The specialization allows us to forgo bundling, and lets us recover
the down-to-earth Type→Type type for the type constructor, and the (a→b)→(F a→F b)
type for the function map, with all setoid/morphism proofs hidden in the structure class
in Prop.
To justify this definition, in theory/functors we show that instances of this new functor
class do indeed give rise to instances of the original nice abstract Functor class. *)
Class SFmap (M : Type → Type) := sfmap: ∀ `(A → B), (M A → M B).
Class SFunctor (M : Type → Type)
`{∀ `{Equiv A}, Equiv (M A)} `{SFmap M} : Prop :=
{ sfunctor_setoid `{Setoid A} :: Setoid (M A)
; sfmap_proper `{Setoid A} `{Setoid B} ::
Proper (((=) ==> (=)) ==> ((=) ==> (=))) (@sfmap M _ A B)
; sfmap_id `{Setoid A} : sfmap id = id
; sfmap_comp `{Equiv A} `{Equiv B} `{Equiv C} `{!Setoid_Morphism (f : B → C)} `{!Setoid_Morphism (g : A → B)} :
sfmap (f ∘ g) = sfmap f ∘ sfmap g }.
|
