-
Notifications
You must be signed in to change notification settings - Fork 0
/
Elim.agda
207 lines (155 loc) · 7.83 KB
/
Elim.agda
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
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
-- This posts describes how to derive eliminators of described data types.
{-# OPTIONS --type-in-type #-}
open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Product
infixr 6 _⊛_
-- I'll be using the form of descriptions introduced in the previous post:
-- http://effectfully.blogspot.com/2016/04/descriptions.html
data Desc I : Set where
var : I -> Desc I
π : ∀ A -> (A -> Desc I) -> Desc I
_⊛_ : Desc I -> Desc I -> Desc I
⟦_⟧ : ∀ {I} -> Desc I -> (I -> Set) -> Set
⟦ var i ⟧ B = B i
⟦ π A D ⟧ B = ∀ x -> ⟦ D x ⟧ B
⟦ D ⊛ E ⟧ B = ⟦ D ⟧ B × ⟦ E ⟧ B
Extend : ∀ {I} -> Desc I -> (I -> Set) -> I -> Set
Extend (var i) B j = i ≡ j
Extend (π A D) B i = ∃ λ x -> Extend (D x) B i
Extend (D ⊛ E) B i = ⟦ D ⟧ B × Extend E B i
data μ {I} (D : Desc I) j : Set where
node : Extend D (μ D) j -> μ D j
-- It is crucial to define `μ` as a `data` and not as an inductive `record`,
-- because termination checker works better with `data`s.
-- While defining the generic `elim` function, we'll be keeping in mind some
-- described constructor. Let it be `_∷_` for vectors:
-- `cons-desc = π ℕ λ n -> π A λ _ -> var n ⊛ var (suc n)`
module Verbose where
-- How to get the actual type of the constructor from this description?
-- Each `π` correspons to some `->` and each `_⊛_` corresponds to it as well.
-- I.e. the actual type is `(n : ℕ) -> A -> Vec A n -> Vec (suc n)`.
-- After generalizing `Vec A` to `B`, we get the following definition:
Cons : ∀ {I} -> (I -> Set) -> Desc I -> Set
Cons B (var i) = B i
Cons B (π A D) = ∀ x -> Cons B (D x)
Cons B (D ⊛ E) = ⟦ D ⟧ B -> Cons B E
-- `Cons B cons-desc` evaluates to `(n : ℕ) -> A -> B n -> B (suc n)` as required.
-- Eliminator of `_∷_` (with `Vec A` generalized to `B`) looks like this:
-- `(n : ℕ) -> (x : A) -> {xs : B n} -> P xs -> P (x ∷ xs)`
-- so we need to eliminate `cons-desc` again, but now with `_∷_ : Cons B cons-desc` provided
-- (to form the final `P (x ∷ xs)` part). Note that each inductive occurrence in a description
-- becomes replaced by the corresponding induction hypothesis, hence the `_⊛_` case
-- in the function below:
ElimBy : ∀ {I B} -> ((D : Desc I) -> ⟦ D ⟧ B -> Set) -> (D : Desc I) -> Cons B D -> Set
ElimBy P (var i) x = P (var i) x
ElimBy P (π A D) f = ∀ x -> ElimBy P (D x) (f x)
ElimBy P (D ⊛ E) f = ∀ {x} -> P D x -> ElimBy P E (f x)
-- The type of `P` is `(D : Desc I) -> ⟦ D ⟧ B -> Set` instead of `∀ {i} -> B i -> Set`,
-- because there can be a higher-order inductive occurrence (like in `W`) and
-- the induction hypothesis have to be computed by induction on a `Desc`.
-- We'll do this in a moment.
-- The next step is to compute the constructor.
-- As described in the previous post the actual `_∷_` can be recovered as
-- `_∷_ {n} x xs = node (n , x , xs , refl)`
-- (it's `node (false, n , x , xs , refl)` for the actual `Vec`,
-- because the first element in a tuple allows to distinguish `[]` and `_∷_`)
-- So all we need is to define a function that receives `n` arguments,
-- puts them in a tuple and applies `node` to it. That's the usual CPS stuff:
cons : ∀ {I B} -> (D : Desc I) -> (∀ {j} -> Extend D B j -> B j) -> Cons B D
cons (var i) k = k refl
cons (π A D) k = λ x -> cons (D x) (k ∘ _,_ x)
cons (D ⊛ E) k = λ x -> cons E (k ∘ _,_ x)
-- However note that `ElimBy` and `cons` are defined by the same induction on `D`.
-- Hence we can drop `Cons` and `cons` stuff and compute `ElimBy` directly.
-- Here is the final definition of `ElimBy`:
ElimBy : ∀ {I B}
-> ((D : Desc I) -> ⟦ D ⟧ B -> Set)
-> (D : Desc I)
-> (∀ {j} -> Extend D B j -> B j)
-> Set
ElimBy C (var i) k = C (var i) (k refl)
ElimBy C (π A D) k = ∀ x -> ElimBy C (D x) (k ∘ _,_ x)
ElimBy C (D ⊛ E) k = ∀ {x} -> C D x -> ElimBy C E (k ∘ _,_ x)
-- Now we need to compute induction hypotheses. Recall how `W` looks like:
data W (A : Set) (B : A -> Set) : Set where
sup : ∀ x -> (B x -> W A B) -> W A B
-- Its eliminator is
elimW : ∀ {α β π} {A : Set α} {B : A -> Set β}
-> (P : W A B -> Set π)
-> (∀ {x} {g : B x -> W A B} -> (∀ y -> P (g y)) -> P (sup x g))
-> ∀ w
-> P w
elimW P h (sup x g) = h (λ y -> elimW P h (g y))
-- I.e. the induction hypothesis for higher-order `g : B x -> W A B` is
-- `(y : B x) -> P (g y)` (higher-order as well).
Hyp : ∀ {I B} -> (∀ {i} -> B i -> Set) -> (D : Desc I) -> ⟦ D ⟧ B -> Set
Hyp C (var i) y = C y
Hyp C (π A D) f = ∀ x -> Hyp C (D x) (f x)
Hyp C (D ⊛ E) (x , y) = Hyp C D x × Hyp C E y
-- When an inductive occurrence is a tuple, the induction hypothesis is a tuple too,
-- hence the `_⊛_` case above.
-- Finally, the type of a function that eliminator receives
-- (I'll call it "an eliminating function") is
Elim : ∀ {I B}
-> (∀ {i} -> B i -> Set)
-> (D : Desc I)
-> (∀ {j} -> Extend D B j -> B j)
-> Set
Elim = ElimBy ∘ Hyp
-- It only remains to construct the actual generic eliminator.
module _ {I} {D₀ : Desc I} (P : ∀ {j} -> μ D₀ j -> Set) (h : Elim P D₀ node) where
mutual
elimExtend : ∀ {j}
-> (D : Desc I) {k : ∀ {j} -> Extend D (μ D₀) j -> μ D₀ j}
-> Elim P D k
-> (e : Extend D (μ D₀) j)
-> P (k e)
elimExtend (var i) z refl = z
elimExtend (π A D) h (x , e) = elimExtend (D x) (h x) e
elimExtend (D ⊛ E) h (d , e) = elimExtend E (h (hyp D d)) e
hyp : ∀ D -> (d : ⟦ D ⟧ (μ D₀)) -> Hyp P D d
hyp (var i) d = elim d
hyp (π A D) f = λ x -> hyp (D x) (f x)
hyp (D ⊛ E) (x , y) = hyp D x , hyp E y
elim : ∀ {j} -> (d : μ D₀ j) -> P d
elim (node e) = elimExtend D₀ h e
-- No surpise we need a family of mutually defined functions.
-- `D₀` is the description of a data being eliminated. It's in the module parameter
-- among with `P` and an eliminating function `h`, because otherwise it would be required
-- to trace them explicitly through all three functions and these parameters never change.
-- `elim` unfolds a `μ` and delegates the work to `elimExtend`.
-- `elimExtend` is defined by induction on `D`:
-- - At the end of a description we simply return what has been computed so far.
-- - On encountering a non-inductive argument to a constructor we
-- apply the eliminating function to it.
-- - On encountering an inductive argument to a constructor we
-- compute recursively (`hyp` calls `elim` in the `var` case) and
-- apply the elimination function to the result of the computation.
-- That's basically it. An example:
open import Data.Bool.Base
open import Data.Nat.Base
_<?>_ : ∀ {α} {A : Bool -> Set α} -> A true -> A false -> ∀ b -> A b
(x <?> y) true = x
(x <?> y) false = y
_⊕_ : ∀ {I} -> Desc I -> Desc I -> Desc I
D ⊕ E = π Bool (D <?> E)
vec : Set -> Desc ℕ
vec A = var 0
⊕ π ℕ λ n -> π A λ _ -> var n ⊛ var (suc n)
Vec : Set -> ℕ -> Set
Vec A = μ (vec A)
pattern [] = node (true , refl)
pattern _∷_ {n} x xs = node (false , n , x , xs , refl)
elimVec : ∀ {n A}
-> (P : ∀ {n} -> Vec A n -> Set)
-> (∀ {n} x {xs : Vec A n} -> P xs -> P (x ∷ xs))
-> P []
-> (xs : Vec A n)
-> P xs
elimVec P f z = elim P (z <?> λ _ -> f)
-- Since vectors have two constructors, `vec` starts with `π Bool` which allows to split
-- the description into two parts: the one that describes `[]` and the other that describes `_∷_`.
-- That's why an eliminating function for vectors is of the form `(b : Bool) -> ...` and
-- we use `_<?>_` to choose between an eliminating function for `[]` (just a value `z`) and
-- an eliminating function for `_∷_` (which ignores `n : ℕ`).