1
------------------------------------------------------------------------
2
-- The reflexive transitive closures of McBride, Norell and Jansson
3
------------------------------------------------------------------------
5
-- This module could be placed under Relation.Binary. However, since
6
-- its primary purpose is to be used for _data_ it has been placed
11
open import Relation.Binary
12
open import Data.Function
17
-- Reflexive transitive closure.
19
data Star {I : Set} (T : Rel I zero) : Rel I zero where
20
ε : Reflexive (Star T)
21
_◅_ : ∀ {i j k} (x : T i j) (xs : Star T j k) → Star T i k
22
-- The type of _◅_ is Trans T (Star T) (Star T); I expanded
23
-- the definition in order to be able to name the arguments (x
26
-- Append/transitivity.
30
_◅◅_ : ∀ {I} {T : Rel I zero} → Transitive (Star T)
32
(x ◅ xs) ◅◅ ys = x ◅ (xs ◅◅ ys)
34
-- Sometimes you want to view cons-lists as snoc-lists. Then the
35
-- following "constructor" is handy. Note that this is _not_ snoc for
36
-- cons-lists, it is just a synonym for cons (with a different
41
_▻_ : ∀ {I} {T : Rel I zero} {i j k} →
42
Star T j k → T i j → Star T i k
45
-- A corresponding variant of append.
49
_▻▻_ : ∀ {I} {T : Rel I zero} {i j k} →
50
Star T j k → Star T i j → Star T i k
53
-- A generalised variant of map which allows the index type to change.
55
gmap : ∀ {I} {T : Rel I zero} {J} {U : Rel J zero} →
56
(f : I → J) → T =[ f ]⇒ U → Star T =[ f ]⇒ Star U
58
gmap f g (x ◅ xs) = g x ◅ gmap f g xs
60
map : ∀ {I} {T U : Rel I zero} → T ⇒ U → Star T ⇒ Star U
63
-- TransFlip is used to state the type signature of gfold.
65
TransFlip : {A : Set} → Rel A zero → Rel A zero → Rel A zero → Set
66
TransFlip P Q R = ∀ {i j k} → Q j k → P i j → R i k
68
-- A generalised variant of fold.
70
gfold : ∀ {I J T} (f : I → J) P →
71
Trans T (P on f) (P on f) →
72
TransFlip (Star T) (P on f) (P on f)
74
gfold f P _⊕_ ∅ (x ◅ xs) = x ⊕ gfold f P _⊕_ ∅ xs
76
fold : ∀ {I T} (P : Rel I zero) →
77
Trans T P P → Reflexive P → Star T ⇒ P
78
fold P _⊕_ ∅ = gfold id P _⊕_ ∅
80
gfoldl : ∀ {I J T} (f : I → J) P →
81
Trans (P on f) T (P on f) →
82
Trans (P on f) (Star T) (P on f)
83
gfoldl f P _⊕_ ∅ ε = ∅
84
gfoldl f P _⊕_ ∅ (x ◅ xs) = gfoldl f P _⊕_ (∅ ⊕ x) xs
86
foldl : ∀ {I T} (P : Rel I zero) →
87
Trans P T P → Reflexive P → Star T ⇒ P
88
foldl P _⊕_ ∅ = gfoldl id P _⊕_ ∅
90
concat : ∀ {I} {T : Rel I zero} → Star (Star T) ⇒ Star T
91
concat {T = T} = fold (Star T) _◅◅_ ε
93
-- If the underlying relation is symmetric, then the reflexive
94
-- transitive closure is also symmetric.
96
revApp : ∀ {I} {T U : Rel I zero} → Sym T U →
97
∀ {i j k} → Star T j i → Star U j k → Star U i k
99
revApp rev (x ◅ xs) ys = revApp rev xs (rev x ◅ ys)
101
reverse : ∀ {I} {T U : Rel I zero} → Sym T U → Sym (Star T) (Star U)
102
reverse rev xs = revApp rev xs ε
104
-- Reflexive transitive closures form a (generalised) monad.
106
-- return could also be called singleton.
108
return : ∀ {I} {T : Rel I zero} → T ⇒ Star T
111
-- A generalised variant of the Kleisli star (flip bind, or
114
kleisliStar : ∀ {I J} {T : Rel I zero} {U : Rel J zero} (f : I → J) →
115
T =[ f ]⇒ Star U → Star T =[ f ]⇒ Star U
116
kleisliStar f g = concat ∘ gmap f g
118
_⋆ : ∀ {I} {T U : Rel I zero} →
119
T ⇒ Star U → Star T ⇒ Star U
124
_>>=_ : ∀ {I} {T U : Rel I zero} {i j} →
125
Star T i j → T ⇒ Star U → Star U i j
128
-- Note that the monad-like structure above is not an indexed monad
129
-- (as defined in Category.Monad.Indexed). If it were, then _>>=_
130
-- would have a type similar to
132
-- ∀ {I} {T U : Rel I zero} {i j k} →
133
-- Star T i j → (T i j → Star U j k) → Star U i k.
135
-- Note, however, that there is no scope for applying T to any indices
136
-- in the definition used in Category.Monad.Indexed.
added
removed
src/Data/Star.agda
