/
Lambda.lagda.md
774 lines (643 loc) · 31.5 KB
/
Lambda.lagda.md
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
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
<!--
```agda
open import Cat.Diagram.Product.Solver
open import Cat.Diagram.Exponential
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Prelude
import Cat.Functor.Bifunctor as Bifunctor
import Cat.Reasoning
```
-->
```agda
module Cat.CartesianClosed.Lambda
```
# Simply-typed lambda calculus {defines="simply-typed-lambda-calculus STLC"}
<!--
```agda
{o ℓ} (C : Precategory o ℓ) (fp : has-products C) (term : Terminal C)
(cc : Cartesian-closed C fp term)
where
open Binary-products C fp hiding (unique₂)
open Cartesian-closed cc
open Cat.Reasoning C
```
-->
The **simply typed $\lambda$-calculus** (STLC) is a very small typed
programming language very strongly associated with [Cartesian closed
categories]. In this module, we define the syntax for STLC with base
types, and inhabitants of these, given by the objects and morphisms of
an arbitrary CCC. This syntax can be used to _reflect_ morphisms of a
CCC, making the "structural" morphisms explicit. We then build a
_normalisation_ procedure, which can be used to effectively compare
morphisms in the CCC.
[Cartesian closed categories]: Cat.Diagram.Exponential.html
The types of STLC are generated by function types `` a `⇒ b `` and
product types `` a `× b ``, along with an inclusion of objects from the
target category to serve as "base types", e.g. the natural numbers. The
contexts are simply lists of types.
```agda
data Ty : Type o where
_`×_ : Ty → Ty → Ty
_`⇒_ : Ty → Ty → Ty
`_ : Ob → Ty
data Cx : Type o where
∅ : Cx
_,_ : Cx → Ty → Cx
```
<!--
```agda
private variable
Γ Δ Θ : Cx
τ σ : Ty
```
-->
To use contexts, we introduce _variables_. A variable $v : \Gamma \ni
\tau$ gives an index in $\Gamma$ where something of type $\tau$ can be
found. It can either be right here, in which case we `stop`{.Agda}, or
it can be further back in the context, and we must `pop`{.Agda} the top
variable off to get to it.
```agda
data Var : Cx → Ty → Type o where
stop : Var (Γ , τ) τ
pop : Var Γ τ → Var (Γ , σ) τ
```
<!--
```agda
⟦_⟧ᵗ : Ty → Ob
⟦_⟧ᶜ : Cx → Ob
data Expr (Γ : Cx) : Ty → Typeω
```
-->
We can now write down the type of expressions, or, really, of _typing
judgements_. An inhabitant of `Expr Γ τ` is a tree representing a
complete derivation of something of type `τ`. We insist on the name
_expression_ rather than _term_ since there are more expressions than
there are terms: For example, in the context $\varnothing , a : \tau$, the
expressions $(\lambda b \to b)\; a$ and $a$ denote the same term.
```agda
data Expr Γ where
`var : Var Γ τ → Expr Γ τ
`π₁ : Expr Γ (τ `× σ) → Expr Γ τ
`π₂ : Expr Γ (τ `× σ) → Expr Γ σ
`⟨_,_⟩ : Expr Γ τ → Expr Γ σ → Expr Γ (τ `× σ)
`λ : Expr (Γ , τ) σ → Expr Γ (τ `⇒ σ)
`$ : Expr Γ (τ `⇒ σ) → Expr Γ τ → Expr Γ σ
`_ : Hom ⟦ Γ ⟧ᶜ ⟦ τ ⟧ᵗ → Expr Γ τ
```
Using the Cartesian closed structure, we can interpret types, contexts,
variables and expressions in terms of the structural morphisms: For
example, the empty context is interpreted by the terminal object,
and^[since contexts are built by extension on the _right_] the zeroth
variable is given by the second projection map $\Gamma \times A \to A$.
```agda
⟦ X `× Y ⟧ᵗ = ⟦ X ⟧ᵗ ⊗₀ ⟦ Y ⟧ᵗ
⟦ X `⇒ Y ⟧ᵗ = Exp.B^A ⟦ X ⟧ᵗ ⟦ Y ⟧ᵗ
⟦ ` X ⟧ᵗ = X
⟦ Γ , τ ⟧ᶜ = ⟦ Γ ⟧ᶜ ⊗₀ ⟦ τ ⟧ᵗ
⟦ ∅ ⟧ᶜ = Terminal.top term
⟦_⟧ⁿ : Var Γ τ → Hom ⟦ Γ ⟧ᶜ ⟦ τ ⟧ᵗ
⟦ stop ⟧ⁿ = π₂
⟦ pop x ⟧ⁿ = ⟦ x ⟧ⁿ ∘ π₁
⟦_⟧ᵉ : Expr Γ τ → Hom ⟦ Γ ⟧ᶜ ⟦ τ ⟧ᵗ
⟦ `var x ⟧ᵉ = ⟦ x ⟧ⁿ
⟦ `π₁ p ⟧ᵉ = π₁ ∘ ⟦ p ⟧ᵉ
⟦ `π₂ p ⟧ᵉ = π₂ ∘ ⟦ p ⟧ᵉ
⟦ `⟨ a , b ⟩ ⟧ᵉ = ⟨ ⟦ a ⟧ᵉ , ⟦ b ⟧ᵉ ⟩
⟦ `λ e ⟧ᵉ = ƛ ⟦ e ⟧ᵉ
⟦ `$ f x ⟧ᵉ = ev ∘ ⟨ ⟦ f ⟧ᵉ , ⟦ x ⟧ᵉ ⟩
⟦ ` x ⟧ᵉ = x
```
The type of expressions could (and, to some extent, _should_) be
higher-inductive-recursive, with path constructors expressing the
$\beta$/$\eta$ rules --- the universal properties that we want to
capture. However, this would significantly complicate the development of
the rest of this module. We choose to work with raw derivations,
instead, for convenience. Equality of `Expr`{.Agda} being coarser than
that of `Hom` does not significantly affect our application, which is
metaprogramming.
## Context inclusions
We will implement our semantics using *normalisation by evaluation*, by
embedding our expressions into a domain where the judgemental equalities
of the object-level are also judgemental at the meta-level. We choose
presheaves on a category of *inclusions*, where the objects are contexts
and the maps $\Gamma \to \Delta$ indicate that, starting from $\Gamma$,
you can get to $\Delta$ by *dropping* some of the variables, and keeping
everything else in-order.
```agda
data Ren : Cx → Cx → Type (o ⊔ ℓ) where
stop : Ren Γ Γ
drop : Ren Γ Δ → Ren (Γ , τ) Δ
keep : Ren Γ Δ → Ren (Γ , τ) (Δ , τ)
```
Here we must confess to another crime: Since our (types, hence our)
contexts include objects of the base category, they do not form a set:
therefore, neither does the type `Ren`{.Agda} of context inclusions.
This means that we can not use `Ren`{.Agda} as the morphisms in a
(pre)category. This could be remedied by instead working relative to a
given set of base types, which are equipped with a map into semantic
objects. This does not significantly alter the development, but it would
be an additional inconvenience.
Regardless, we can define composition of context inclusions by
recursion, and, if necessary, we could prove that this is associative
and unital. However, since we are not building an actual category of
presheaves (only gesturing towards one), we omit these proofs.
```agda
_∘ʳ_ : ∀ {Γ Δ Θ} → Ren Γ Δ → Ren Δ Θ → Ren Γ Θ
stop ∘ʳ ρ = ρ
drop σ ∘ʳ ρ = drop (σ ∘ʳ ρ)
keep σ ∘ʳ stop = keep σ
keep σ ∘ʳ drop ρ = drop (σ ∘ʳ ρ)
keep σ ∘ʳ keep ρ = keep (σ ∘ʳ ρ)
```
If we fix a type $\tau$, then the family $- \ni \tau$ which sends a
context to the variables in that context is actually a presheaf. Put
less pretentiously, renamings act on variables:
```agda
ren-var : ∀ {Γ Δ τ} → Ren Γ Δ → Var Δ τ → Var Γ τ
ren-var stop v = v
ren-var (drop σ) v = pop (ren-var σ v)
ren-var (keep σ) stop = stop
ren-var (keep σ) (pop v) = pop (ren-var σ v)
```
Finally, we can define an interpretation of renamings into our model
CCC. Note that this interpretation lands in monomorphisms.
```agda
⟦_⟧ʳ : Ren Γ Δ → Hom ⟦ Γ ⟧ᶜ ⟦ Δ ⟧ᶜ
⟦ stop ⟧ʳ = id
⟦ drop r ⟧ʳ = ⟦ r ⟧ʳ ∘ π₁
⟦ keep r ⟧ʳ = ⟦ r ⟧ʳ ⊗₁ id
```
## Normals and neutrals
To define evaluation, we need a type of normal forms: In our setting,
these include lambda abstractions and pairs, along with morphisms of the
base category. However, we are not working with evaluation, rather with
_normalisation_, where reduction takes place in arbitrary contexts.
Therefore, there are expressions that we can not *give a value to*, but
for which no further normalisation can happen: for example, applying a
variable. Therefore, we define mutually inductive types of **normal
forms** and **neutral forms**.
```agda
data Nf : Cx → Ty → Type (o ⊔ ℓ)
data Ne : Cx → Ty → Type (o ⊔ ℓ)
```
A **normal form** is indeed one for which no more reduction is possible:
lambda expressions and pairs. A neutral form is also normal. These come
primarily from non-empty contexts. Neutral forms are, essentially,
variables together with a stack of *pending eliminations* (applications
or projections that will be reduced in the future). However, in our
setting, we also consider the base terms as neutral _at base types_.
```agda
data Nf where
lam : Nf (Γ , τ) σ → Nf Γ (τ `⇒ σ)
pair : Nf Γ τ → Nf Γ σ → Nf Γ (τ `× σ)
ne : Ne Γ σ → Nf Γ σ
data Ne where
var : Var Γ τ → Ne Γ τ
app : Ne Γ (τ `⇒ σ) → Nf Γ τ → Ne Γ σ
fstₙ : Ne Γ (τ `× σ) → Ne Γ τ
sndₙ : Ne Γ (τ `× σ) → Ne Γ σ
hom : ∀ {o} → Hom ⟦ Γ ⟧ᶜ o → Ne Γ (` o)
```
By a fairly obvious recursion, renamings act on neutrals and normals,
thus making these, too, into presheaves.
```agda
ren-ne : ∀ {Γ Δ τ} → Ren Δ Γ → Ne Γ τ → Ne Δ τ
ren-nf : ∀ {Γ Δ τ} → Ren Δ Γ → Nf Γ τ → Nf Δ τ
```
This is the only case that requires attention: to rename a morphism of
the base category, we must reify the renaming into its denotation, and
compose with the morphism. The alternative here would be to keep a stack
of pending renamings at each `hom`{.Agda}, which could then be optimised
before composing at the end.
```agda
ren-ne σ (hom h) = hom (h ∘ ⟦ σ ⟧ʳ)
```
<!--
```agda
ren-ne σ (var v) = var (ren-var σ v)
ren-ne σ (app f a) = app (ren-ne σ f) (ren-nf σ a)
ren-ne σ (fstₙ a) = fstₙ (ren-ne σ a)
ren-ne σ (sndₙ a) = sndₙ (ren-ne σ a)
ren-nf σ (lam n) = lam (ren-nf (keep σ) n)
ren-nf σ (pair a b) = pair (ren-nf σ a) (ren-nf σ b)
ren-nf σ (ne x) = ne (ren-ne σ x)
```
-->
Normals and neutrals also have a straightforward denotation given by the
Cartesian closed structure.
```agda
⟦_⟧ₙ : Nf Γ τ → Hom ⟦ Γ ⟧ᶜ ⟦ τ ⟧ᵗ
⟦_⟧ₛ : Ne Γ τ → Hom ⟦ Γ ⟧ᶜ ⟦ τ ⟧ᵗ
⟦ lam h ⟧ₙ = ƛ ⟦ h ⟧ₙ
⟦ pair a b ⟧ₙ = ⟨ ⟦ a ⟧ₙ , ⟦ b ⟧ₙ ⟩
⟦ ne x ⟧ₙ = ⟦ x ⟧ₛ
⟦ var x ⟧ₛ = ⟦ x ⟧ⁿ
⟦ app f x ⟧ₛ = ev ∘ ⟨ ⟦ f ⟧ₛ , ⟦ x ⟧ₙ ⟩
⟦ fstₙ h ⟧ₛ = π₁ ∘ ⟦ h ⟧ₛ
⟦ sndₙ h ⟧ₛ = π₂ ∘ ⟦ h ⟧ₛ
⟦ hom h ⟧ₛ = h
```
We also have to prove a few hateful lemmas about how renamings, and its
action on variables, neutrals and normals, interact with the denotation
brackets. These lemmas essentially say that $\sem{f[\rho]} =
\sem{f}\sem{\rho}$, so that it doesn't matter whether we first pass to
the semantics in $\cC$ or apply a renaming.
```agda
⟦⟧-∘ʳ : (ρ : Ren Γ Δ) (σ : Ren Δ Θ) → ⟦ ρ ∘ʳ σ ⟧ʳ ≡ ⟦ σ ⟧ʳ ∘ ⟦ ρ ⟧ʳ
ren-⟦⟧ⁿ : (ρ : Ren Δ Γ) (v : Var Γ τ) → ⟦ ren-var ρ v ⟧ⁿ ≡ ⟦ v ⟧ⁿ ∘ ⟦ ρ ⟧ʳ
ren-⟦⟧ₛ : (ρ : Ren Δ Γ) (t : Ne Γ τ) → ⟦ ren-ne ρ t ⟧ₛ ≡ ⟦ t ⟧ₛ ∘ ⟦ ρ ⟧ʳ
ren-⟦⟧ₙ : (ρ : Ren Δ Γ) (t : Nf Γ τ) → ⟦ ren-nf ρ t ⟧ₙ ≡ ⟦ t ⟧ₙ ∘ ⟦ ρ ⟧ʳ
```
<details>
<summary>If you want, you can choose to read the proofs of these
substitution correctness lemmas by clicking on this `<details>`{.html}
tag.
</summary>
```agda
⟦⟧-∘ʳ stop σ = intror refl
⟦⟧-∘ʳ (drop ρ) σ = pushl (⟦⟧-∘ʳ ρ σ)
⟦⟧-∘ʳ (keep ρ) stop = introl refl
⟦⟧-∘ʳ (keep ρ) (drop σ) = pushl (⟦⟧-∘ʳ ρ σ) ∙ sym (pullr π₁∘⟨⟩)
⟦⟧-∘ʳ (keep ρ) (keep σ) = sym $ Product.unique (fp _ _) _
(pulll π₁∘⟨⟩ ∙ pullr π₁∘⟨⟩ ∙ pulll (sym (⟦⟧-∘ʳ ρ σ)))
(pulll π₂∘⟨⟩ ∙ pullr π₂∘⟨⟩ ∙ idl _)
ren-⟦⟧ⁿ stop v = intror refl
ren-⟦⟧ⁿ (drop ρ) v = pushl (ren-⟦⟧ⁿ ρ v)
ren-⟦⟧ⁿ (keep ρ) stop = sym (π₂∘⟨⟩ ∙ idl _)
ren-⟦⟧ⁿ (keep ρ) (pop v) = pushl (ren-⟦⟧ⁿ ρ v) ∙ sym (pullr π₁∘⟨⟩)
ren-⟦⟧ₛ ρ (var x) = ren-⟦⟧ⁿ ρ x
ren-⟦⟧ₛ ρ (app f x) = ap₂ _∘_ refl
(ap₂ ⟨_,_⟩ (ren-⟦⟧ₛ ρ f) (ren-⟦⟧ₙ ρ x) ∙ sym (⟨⟩∘ _))
∙ pulll refl
ren-⟦⟧ₛ ρ (fstₙ t) = pushr (ren-⟦⟧ₛ ρ t)
ren-⟦⟧ₛ ρ (sndₙ t) = pushr (ren-⟦⟧ₛ ρ t)
ren-⟦⟧ₛ ρ (hom x) = refl
ren-⟦⟧ₙ ρ (lam t) =
ap ƛ (ren-⟦⟧ₙ (keep ρ) t)
∙ sym (unique _ (ap₂ _∘_ refl rem₁ ∙ pulll (commutes ⟦ t ⟧ₙ)))
where
rem₁ : (⟦ lam t ⟧ₙ ∘ ⟦ ρ ⟧ʳ) ⊗₁ id ≡ (⟦ lam t ⟧ₙ ⊗₁ id) ∘ ⟦ ρ ⟧ʳ ⊗₁ id
rem₁ = Bifunctor.first∘first ×-functor
ren-⟦⟧ₙ ρ (pair a b) = ap₂ ⟨_,_⟩ (ren-⟦⟧ₙ ρ a) (ren-⟦⟧ₙ ρ b) ∙ sym (⟨⟩∘ _)
ren-⟦⟧ₙ ρ (ne x) = ren-⟦⟧ₛ ρ x
```
</details>
## Normalization
We would like to write a map of type `Expr Γ τ → Nf Γ τ`. However, *by
design*, this is not straightforward: the type of normal forms is...
$\beta$-normal.^[It is not, however, $\eta$-long.] However, note that,
since both `Nf` and `Ne` are "presheaves" on the "category of
renamings", we can use the Cartesian closed structure *of presheaves* to
interpret the lambda calculus. The idea here is that presheaves, being
functors into $\Sets$, have a computational structure on the relevant
connectives that closely matches that of $\Sets$ itself: for example,
composing the first projection with a pairing, in the category of
presheaves, is (componentwise) definitionally equal to the first
component of the pair. It's a boosted up version of exactly the same
idea used for [the category solver].
[the category solver]: Cat.Solver.html
Then, as long as we can *reify* these presheaves back to normal forms,
we have a normalisation procedure! Expressions are interpreted as
sections of the relevant presheaves, then reified into normal forms.
And, to be clear, we only need to reflect the presheaves that actually
represent types: these can be built by recursion (on the type!) so that
they are very easy to reify.
However, that still leaves the question of _correctness_ for the NbE
algorithm. Given an expression $\Gamma \vdash e : \tau$, we will have
two wildly different approaches to interpreting $e$ as a morphism
$\sem{\Gamma} \to \sem{\tau}$. There's the naïve denotation
`⟦_⟧ᵉ`{.Agda}, which interprets an expression directly using the
relevant connections; But now we can also interpret an expression
$\Gamma \vdash e : \tau$ into a section $v : \cR^\tau(\Gamma)$, then
reify that to a normal form $n : \operatorname{Nf}(\Gamma, \tau)$, and
take the denotation $\sem{n} : \sem{\Gamma} \to \sem{\tau}$.
Normalisation _should_ compute a $\beta$-normal form, and $\beta$ is
validated by CCCs, so $\sem{n}$ and $\sem{e}$ should be the same. How do
we ensure this?
It would be totally possible to do this in two passes - first define the
algorithm, then prove it correct. But the proof of correctness would
mirror the structure of the algorithm almost 1:1! Can we define the
algorithm in a way that is _forced_ into correctness? It turns out
that we can! The idea here is an adaptation of the **gluing** method in
the semantics of type theory. Rather than have a mere presheaf
$\cR^\tau(-)$ to represent the semantic values in $\tau$, our full
construction `Tyᵖ`{.Agda} has _three_ arguments: The type $\tau$, the
context $\Gamma$ (over which it is functorial), and a _denotation_ $h :
\sem{\Gamma} \to \sem{\tau}$ --- and in prose, we'll write `Tyᵖ`{.Agda}
as $\cR^\tau_{h}(\Gamma)$; we say that $s$ **tracks** $h$ when $s :
\cR^\tau_{h}(\Gamma)$.
Since all our operations on semantic values will be written against a
type _indexed by_ their denotations, the core of the algorithm will
_have to_ be written in a way that evidently preserves denotations ---
the type checker is doing most of the work. Our only actual correctness
theorem boils down to showing that, given $s : \cR^\tau_{h}(\Gamma)$, we
have $\sem{\reify s} = h$ in $\hom(\sem{\Gamma}, \sem{\tau})$.
To summarize all the parts, we have:
- **Expressions** $\Gamma \vdash e : \tau$ --- the user writes these, and
they may have redices.
- **Denotations** $\sem{e} : \sem{\Gamma} \to \sem{\tau}$. Since a CCC
has "structural" morphisms corresponding to each kind of expression, we
can directly read off a morphism from an expression.
- **Neutrals** $n : \Ne(\Gamma, \tau)$ and **normals** $n : \Nf(\Gamma, \tau)$.
A neutral is something that wants to reduce but can't (e.g. a
projection applied to a variable), and a normal is something that
definitely won't reduce anymore (e.g. a lambda expression). Normals
and neutrals also have denotations, so we may also write $\sem{n}$
when $n : \Nf(-,-)$ or $n : \Ne(-,-)$.
- **Semantic values**, $\cR^\tau_h(\Gamma)$. The presheaf
$\cR^\tau_{h}(\Gamma)$ is computed by recursion on $\tau$ so that its
sections have a good computational representation. As mentioned above, it's
indexed by a denotation $h : \sem{\Gamma} \to \sem{\tau}$, forcing the
core of the algorithm to preserve denotations.
- The **reification and reflection** transformations $\reify :
\cR^\tau_{-}(\Gamma) \to \Nf(\Gamma, \tau)$, which turns a semantic
value into a normal form, and $\reflect : \Ne(\Gamma, \tau) \to
\cR^\tau_{-}(\Gamma)$ which witnesses that the semantic values include
the neutrals.
Our main objective is a normalisation function $\operatorname{expr}$
that maps expressions $\Gamma \vdash e : \tau$ to semantic values
$\operatorname{expr}(e) : \cR^\tau_{\sem{e}}(\Gamma)$. Let's get
started.
:::{.warning}
While we have been talking about presheaves above, the actual code does
_not_ actually set up a presheaf category to work in. The reason for
this is parsimony. Referring to presheaves for the motivation, but
working with simpler type families, lends itself better to
formalisation; many of the details, e.g. functoriality of
$\cR^\tau_{-}(-)$, are not used, and would simply be noise.
:::
### Semantic values
```agda
Tyᵖ : (τ : Ty) (Γ : Cx) → Hom ⟦ Γ ⟧ᶜ ⟦ τ ⟧ᵗ → Type (o ⊔ ℓ)
```
We define $\cR^{\tau}_{-}(-)$ by recursion on $\tau$, and its
definition is mostly unsurprising: at each case, we use the Cartesian
closed structure of presheaf categories to interpret the given type into
a presheaf that has the right universal property, but is "definitionally
nicer". Let's go through it case-by-case. When faced with a product type
in the object language, we can simply return a meta-language product
type. However, we must also preserve the tracking information: if a
section of a product type is to track $h$, what should each component
track? Well, we know that $h = \langle \pi_1h, \pi_2h \rangle$, by the
uniqueness property of Cartesian products. So the first component should
track $\pi_1h$, and the second $\pi_2h$!
```agda
Tyᵖ (τ `× σ) Γ h = Tyᵖ τ Γ (π₁ ∘ h) × Tyᵖ σ Γ (π₂ ∘ h)
```
For a function type, we once again appeal to the construction in
presheaves. The components of the exponential $(Q^P)(\Gamma)$ are
defined to be the natural transformations $\yo(\Gamma) \times P \To Q$,
which, at the component, are given by maps $\hom(\Gamma, \Delta) \times
P(\Delta) \to Q(\Delta)$. A function value must preserve tracking
information: A function which tracks $h$, if given an argument tracking
$a$, it must return a value which tracks the application of $h$ to $a$,
relative to the renaming $\rho$. In a CCC, that's given by
$$
\operatorname{ev} \langle h \circ \rho , a \rangle
$$,
which is precisely what we require.
```agda
Tyᵖ (τ `⇒ σ) Γ h =
∀ {Δ} (ρ : Ren Δ Γ) {a}
→ Tyᵖ τ Δ a
→ Tyᵖ σ Δ (ev ∘ ⟨ h ∘ ⟦ ρ ⟧ʳ , a ⟩)
```
Finally, we have the case of base types, for which the corresponding
presheaf is that of neutral forms. Here, we can finally discharge the
tracking information: a neutral $n$ tracks $h$ iff. $\sem{n} = h$.
```agda
Tyᵖ (` x) Γ h = Σ (Ne Γ (` x)) λ n → ⟦ n ⟧ₛ ≡ h
```
To work on open contexts, we can define (now by induction), the presheaf
of _parallel substitutions_, which are decorated sequences of terms.
These also have a morphism of $\cC$ attached, but keep in mind that a
parallel substitution $\Gamma \to \Delta$ interprets as an element of
$\hom(\Delta, \Gamma)$, hence that is what they are indexed over.
```agda
data Subᵖ : ∀ Γ Δ → Hom ⟦ Δ ⟧ᶜ ⟦ Γ ⟧ᶜ → Type (o ⊔ ℓ) where
∅ : ∀ {i} → Subᵖ ∅ Δ i
_,_ : ∀ {h} → Subᵖ Γ Δ (π₁ ∘ h) → Tyᵖ σ Δ (π₂ ∘ h) → Subᵖ (Γ , σ) Δ h
```
<!--
```agda
tyᵖ⟨_⟩ : ∀ {τ Γ h h'} → h ≡ h' → Tyᵖ τ Γ h → Tyᵖ τ Γ h'
tyᵖ⟨_⟩ {τ `× σ} p (a , b) = tyᵖ⟨ ap (π₁ ∘_) p ⟩ a , tyᵖ⟨ ap (π₂ ∘_) p ⟩ b
tyᵖ⟨_⟩ {τ `⇒ σ} p ν ρ x = tyᵖ⟨ ap (λ e → ev ∘ ⟨ e ∘ ⟦ ρ ⟧ʳ , _ ⟩) p ⟩ (ν ρ x)
tyᵖ⟨_⟩ {` x} p (n , q) .fst = n
tyᵖ⟨_⟩ {` x} p (n , q) .snd = q ∙ p
subᵖ⟨_⟩ : ∀ {Γ Δ h h'} → h ≡ h' → Subᵖ Γ Δ h → Subᵖ Γ Δ h'
subᵖ⟨_⟩ p ∅ = ∅
subᵖ⟨_⟩ p (r , x) = subᵖ⟨ ap (π₁ ∘_) p ⟩ r , tyᵖ⟨ ap (π₂ ∘_) p ⟩ x
```
-->
As always, we must show that these have an action by renamings.
Renamings act on the semantic component, too: if $v$ tracks $h$, then
$v[\rho]$ tracks $h\sem{\rho}$.
```agda
ren-tyᵖ : ∀ {Δ Γ τ m} (ρ : Ren Δ Γ) → Tyᵖ τ Γ m → Tyᵖ τ Δ (m ∘ ⟦ ρ ⟧ʳ)
ren-subᵖ : ∀ {Δ Γ Θ m} (ρ : Ren Θ Δ) → Subᵖ Γ Δ m → Subᵖ Γ Θ (m ∘ ⟦ ρ ⟧ʳ)
```
<!--
```agda
ren-tyᵖ {τ = τ `× σ} r (a , b) =
tyᵖ⟨ sym (assoc _ _ _) ⟩ (ren-tyᵖ r a)
, tyᵖ⟨ sym (assoc _ _ _) ⟩ (ren-tyᵖ r b)
ren-tyᵖ {τ = τ `⇒ σ} r t {Θ} ρ {α} a =
tyᵖ⟨ ap (λ e → ev ∘ ⟨ e , α ⟩) (pushr (⟦⟧-∘ʳ ρ r)) ⟩ (t (ρ ∘ʳ r) a)
ren-tyᵖ {τ = ` x} r (f , p) = ren-ne r f , ren-⟦⟧ₛ r f ∙ ap₂ _∘_ p refl
ren-subᵖ r ∅ = ∅
ren-subᵖ r (c , x) =
subᵖ⟨ sym (assoc _ _ _) ⟩ (ren-subᵖ r c)
, tyᵖ⟨ sym (assoc _ _ _) ⟩ (ren-tyᵖ r x)
```
-->
### Reification and reflection
We can now define the reification and reflection functions. Reflection
embeds a neutral form into semantic values; Reification turns semantic
values into normal forms. Since we have defined the semantic values by
recursion, we can exploit the good computational behaviour of Agda types
in our reification/reflection functions: for example, when reifying at a
product type, we know that we have an honest-to-god product of semantic
values at hand.
```agda
reifyᵖ : ∀ {h} → Tyᵖ τ Γ h → Nf Γ τ
reflectᵖ : (n : Ne Γ τ) → Tyᵖ τ Γ ⟦ n ⟧ₛ
reifyᵖ-correct : ∀ {h} (v : Tyᵖ τ Γ h) → ⟦ reifyᵖ v ⟧ₙ ≡ h
reifyᵖ {τ = τ `× s} (a , b) = pair (reifyᵖ a) (reifyᵖ b)
reifyᵖ {τ = τ `⇒ s} f = lam (reifyᵖ (f (drop stop) (reflectᵖ (var stop))))
reifyᵖ {τ = ` x} d = ne (d .fst)
reflectᵖ {τ = τ `× σ} n = reflectᵖ (fstₙ n) , reflectᵖ (sndₙ n)
reflectᵖ {τ = τ `⇒ σ} n ρ a = tyᵖ⟨ ap₂ (λ e f → ev ∘ ⟨ e , f ⟩) (ren-⟦⟧ₛ ρ n) (reifyᵖ-correct a) ⟩
(reflectᵖ (app (ren-ne ρ n) (reifyᵖ a)))
reflectᵖ {τ = ` x} n = n , refl
```
The interesting cases deal with function types: To reify a lambda ---
which is semantically represented by a *function* that operates on (a
renaming and) the actual argument --- we produce a `lam`{.Agda}
constructor, but we must then somehow reify "all possible bodies".
However, since the semantic value of a function takes arguments and
returns results in an arbitrary extension of the given context, we can
introduce a new variable --- thus a new neutral --- and apply the body
_to that_. Evaluation keeps going, but anything that actually depends on
the body will be blocked on this new neutral!
Conversely, reflection starts from a neutral, and must build a semantic
value that captures all the pending applications. At the case of a
lambda, we have a neutral $n : \Gamma \vdash A \to B$, a renaming $\rho
: \Delta \to \Gamma$, and an argument $a : \Delta \vdash A$. We can thus
build the stuck application $n[\rho]\; a : \Delta \vdash B$.
This is also where we encounter the only correctness lemma that is not
forced on us by the types involved, since the type of normal forms
$\Nf(\Gamma, \tau)$ is not indexed by a denotation in $\cC$. We must
write an external function `reifyᵖ-correct`{.Agda}, actually
establishing that $\sem{\reify v} = h$ when $v$ tracks $h$.
```agda
reifyᵖ-correct {τ = τ `× σ} (a , b) = sym $
Product.unique (fp _ _) _ (sym (reifyᵖ-correct a)) (sym (reifyᵖ-correct b))
reifyᵖ-correct {τ = τ `⇒ σ} {h = h} ν =
let
p : ⟦ reifyᵖ (ν (drop stop) (reflectᵖ (var stop))) ⟧ₙ ≡ ev ∘ ⟨ h ∘ id ∘ π₁ , π₂ ⟩
p = reifyᵖ-correct (ν (drop stop) (reflectᵖ (var stop)))
in ap ƛ p
∙ sym (unique _ (ap₂ _∘_ refl (ap₂ ⟨_,_⟩ (sym (pulll (elimr refl))) (eliml refl))))
reifyᵖ-correct {τ = ` x} d = d .snd
```
<!--
```agda
⟦_⟧ˢ : ∀ {Γ Δ h} → Subᵖ Γ Δ h → Hom ⟦ Δ ⟧ᶜ ⟦ Γ ⟧ᶜ
⟦_⟧ˢ ∅ = Terminal.! term
⟦_⟧ˢ (c , x) = ⟨ ⟦ c ⟧ˢ , ⟦ reifyᵖ x ⟧ₙ ⟩
⟦⟧ˢ-correct : ∀ {Γ Δ h} (ρ : Subᵖ Γ Δ h) → ⟦ ρ ⟧ˢ ≡ h
⟦⟧ˢ-correct ∅ = Terminal.!-unique term _
⟦⟧ˢ-correct (ρ , x) = sym (Product.unique (fp _ _) _ (sym (⟦⟧ˢ-correct ρ)) (sym (reifyᵖ-correct x)))
```
-->
### Interpreting expressions
With our semantic values carefully chosen to allow reflection and
reification, we can set out to build an `Expr`{.Agda}-algebra. To work
in open contexts, an expression $\Gamma \vdash e : \tau$ will be
interpreted as a natural transformation from parallel substitutions to
types: the parallel substitution acts as our "environment", so is used
in the interpretation of variables:
```agda
varᵖ : ∀ {ρ} (π : Var Δ τ) → Subᵖ Δ Γ ρ → Tyᵖ τ Γ (⟦ π ⟧ⁿ ∘ ρ)
varᵖ stop (_ , x) = x
varᵖ (pop v) (c , _) = tyᵖ⟨ assoc _ _ _ ⟩ (varᵖ v c)
```
We must interpret morphisms from the model category in a type-directed
way, and eta-expand as we go. That's because we made the decision to
only have morphisms as neutrals _at base type_. Therefore, if a morphism
from the base category lands in (e.g.) products, we must interpret it as
the semantic product of its projections:
```agda
baseᵖ : ∀ {h'} (h : Hom ⟦ Δ ⟧ᶜ ⟦ τ ⟧ᵗ) → Subᵖ Δ Γ h' → Tyᵖ τ Γ (h ∘ h')
baseᵖ {τ = τ `× τ₁} x c =
tyᵖ⟨ sym (assoc _ _ _) ⟩ (baseᵖ (π₁ ∘ x) c)
, tyᵖ⟨ sym (assoc _ _ _) ⟩ (baseᵖ (π₂ ∘ x) c)
baseᵖ {τ = τ `⇒ σ} {h' = h'} h c ρ {α} a = tyᵖ⟨ pullr (Product.unique (fp _ _) _ (pulll π₁∘⟨⟩ ∙ extendr π₁∘⟨⟩) (pulll π₂∘⟨⟩ ∙ π₂∘⟨⟩)) ⟩
(baseᵖ (ev ∘ ⟨ h ∘ π₁ , π₂ ⟩) (
subᵖ⟨ sym π₁∘⟨⟩ ⟩ (ren-subᵖ ρ c), tyᵖ⟨ sym π₂∘⟨⟩ ⟩ a))
baseᵖ {τ = ` t} x c = hom (x ∘ ⟦ c ⟧ˢ) , ap (x ∘_) (⟦⟧ˢ-correct c)
```
Those are the hard bits, we can now interpret everything else by a
simple recursion! Note that, when interpreting a lambda expression, we
return a function which evaluates the body, and when eliminating it, we
apply it to the value of its argument^[and the identity renaming, since
our argument lives in the same context].
```agda
exprᵖ : ∀ {h} (e : Expr Δ τ) (ρ : Subᵖ Δ Γ h) → Tyᵖ τ Γ (⟦ e ⟧ᵉ ∘ h)
exprᵖ (`var x) c = varᵖ x c
exprᵖ (`π₁ p) c = tyᵖ⟨ assoc _ _ _ ⟩ (exprᵖ p c .fst)
exprᵖ (`π₂ p) c = tyᵖ⟨ assoc _ _ _ ⟩ (exprᵖ p c .snd)
exprᵖ `⟨ a , b ⟩ c =
tyᵖ⟨ sym (pulll π₁∘⟨⟩) ⟩ (exprᵖ a c) , tyᵖ⟨ sym (pulll π₂∘⟨⟩) ⟩ (exprᵖ b c)
exprᵖ {h = h} (`$ f a) c = tyᵖ⟨ ap (ev ∘_) (ap₂ ⟨_,_⟩ (idr _) refl ∙ sym (⟨⟩∘ h)) ∙ assoc _ _ _ ⟩
(exprᵖ f c stop (exprᵖ a c))
exprᵖ (` x) c = baseᵖ x c
exprᵖ {h = h} (`λ f) ρ σ {m} a = tyᵖ⟨ fixup ⟩ (exprᵖ f
( subᵖ⟨ sym π₁∘⟨⟩ ⟩ (ren-subᵖ σ ρ)
, tyᵖ⟨ sym π₂∘⟨⟩ ⟩ a ))
```
<!--
```agda
where abstract
fixup : ⟦ f ⟧ᵉ ∘ ⟨ h ∘ ⟦ σ ⟧ʳ , m ⟩ ≡ ev ∘ ⟨ (⟦ `λ f ⟧ᵉ ∘ h) ∘ ⟦ σ ⟧ʳ , m ⟩
fixup = sym $
ev ∘ ⟨ (⟦ `λ f ⟧ᵉ ∘ h) ∘ ⟦ σ ⟧ʳ , m ⟩ ≡˘⟨ ap₂ _∘_ refl (Product.unique (fp _ _) _ (pulll π₁∘⟨⟩ ∙ extendr π₁∘⟨⟩) (pulll π₂∘⟨⟩ ·· pullr π₂∘⟨⟩ ·· eliml refl)) ⟩
ev ∘ ⟦ `λ f ⟧ᵉ ⊗₁ id ∘ ⟨ h ∘ ⟦ σ ⟧ʳ , m ⟩ ≡⟨ pulll (is-exponential.commutes has-is-exp _) ⟩
⟦ f ⟧ᵉ ∘ ⟨ h ∘ ⟦ σ ⟧ʳ , m ⟩ ∎
```
-->
If we apply the semantic value of an expression to the "identity
parallel substitution", a context where all the variables are given a
neutral value, we get a normal form!
```agda
id-subᵖ : ∀ Γ → Subᵖ Γ Γ id
id-subᵖ ∅ = ∅
id-subᵖ (Γ , x) =
subᵖ⟨ idl _ ·· idl _ ·· sym (idr _) ⟩ (ren-subᵖ (drop stop) (id-subᵖ Γ))
, tyᵖ⟨ sym (idr _) ⟩ (reflectᵖ (var stop))
nf : Expr Γ τ → Nf Γ τ
nf x = reifyᵖ (exprᵖ x (id-subᵖ _))
```
Moreover, we can appeal to our key correctness theorem to conclude the
correctness of the entire normalisation procedure. That's the only
explicit theorem we proved, with the rest of the pieces being threaded
through the definitions of the various transformations.
```agda
opaque
nf-sound : (e : Expr Γ τ) → ⟦ nf e ⟧ₙ ≡ ⟦ e ⟧ᵉ
nf-sound {Γ = Γ} e = reifyᵖ-correct (exprᵖ e (id-subᵖ Γ)) ∙ elimr refl
```
As a demonstration, we can normalise the expression
$$
a : A, b : B \vdash e = \pi_1 \langle ((\lambda c \to c) a) , b \rangle : A
$$
which lets Agda reduce it away to be simply the variable $a$ (which is
the second in the context). Moreover, by appeal to the correctness
theorem, we can prove that the complicated morphism that $e$ denotes is
equal to the much simpler $\pi_2\pi_1$.
```agda
module _ {a b : Ob} where private
e1 : Expr ((∅ , ` a) , ` b) _
e1 = `π₁ `⟨ `$ (`λ (`var stop)) (`var (pop stop)) , `var stop ⟩
_ : nf e1 ≡ ne (var (pop stop))
_ = refl
_ : π₂ ∘ π₁ ≡ π₁ ∘ ⟨ ev ∘ ⟨ ƛ π₂ , π₂ ∘ π₁ ⟩ , π₂ ⟩
_ = nf-sound e1
-- An attempt to normalise this proof produced 4 MiB of garbage, and
-- ran for over an hour before our patience ran out.
```
<!--
```agda
solve : (e e' : Expr Γ τ) → nf e ≡ nf e' → ⟦ e ⟧ᵉ ≡ ⟦ e' ⟧ᵉ
solve e e' prf = sym (nf-sound e) ·· ap ⟦_⟧ₙ prf ·· nf-sound e'
```
-->
## An application
The normalisation algorithm serves to decide the semantic equality of
expressions in the simply-typed lambda calculus, but I'll freely admit
that's not a task that comes up every day. We can also use this
algorithm to prove things about the simply-typed lambda calculus! As an
example, we have **canonicity**: every term in a base type denotes an
actual element of the base type. In our categorical setting, that means
that, given $\Gamma \vdash e : A$, where $A$ is one of the non-pair,
non-function types we have included from the category $\cC$, then there
is a global element $h : \hom(\top, A)$ which $e$ denotes.
```agda
canonicity : ∀ {a} → (e : Expr ∅ (` a)) → Σ (Hom (Terminal.top term) a) λ h → ⟦ e ⟧ᵉ ≡ h
canonicity {a = a} e = go (nf e) (nf-sound e) where
no-functions : ∀ {a b} → Ne ∅ (a `⇒ b) → ⊥
no-pairs : ∀ {a b} → Ne ∅ (a `× b) → ⊥
no-functions (app f _) = no-functions f
no-functions (fstₙ x) = no-pairs x
no-functions (sndₙ x) = no-pairs x
no-pairs (app f _) = no-functions f
no-pairs (fstₙ x) = no-pairs x
no-pairs (sndₙ x) = no-pairs x
go : (nf : Nf ∅ (` a)) → ⟦ nf ⟧ₙ ≡ ⟦ e ⟧ᵉ → Σ (Hom (Terminal.top term) a) λ h → ⟦ e ⟧ᵉ ≡ h
go (ne (app f _)) p = absurd (no-functions f)
go (ne (fstₙ x)) p = absurd (no-pairs x)
go (ne (sndₙ x)) p = absurd (no-pairs x)
go (ne (hom x)) p = x , sym p
```