Indexed.lagda.rst 49.3 KB
Newer Older
Pierre-Évariste Dagand's avatar
Pierre-Évariste Dagand committed
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 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391 1392 1393 1394 1395 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 1407 1408 1409 1410 1411 1412 1413 1414 1415 1416 1417 1418 1419 1420 1421 1422 1423 1424 1425 1426 1427 1428 1429 1430 1431 1432 1433 1434 1435 1436 1437 1438 1439 1440 1441 1442 1443 1444 1445
..
  ::
  {-# OPTIONS --allow-unsolved-metas --type-in-type  #-}

  open import Level renaming (zero to zeroℓ ; suc to sucℓ)

  open import Data.Unit hiding (_≤_)
  open import Data.Bool
  open import Data.Nat hiding (_*_ ; _≤_)
  open import Data.Maybe
  open import Data.Product
  open import Data.List hiding (_++_)
  open import Data.String

  open import Function hiding (id ; const)

  open import Relation.Binary.PropositionalEquality

  module 02-dependent.Indexed where

================================================================
Indexed functional programming
================================================================

Last week:
  - monadic programming: "how to survive without (some) effects"
  - took advantage of dependent types for proofs (tactics, anyone?)
  - but wrote **simply**-typed programs (mostly)

Today, we shall:
  - write dependently-typed program: types will dependent on values
  - exploit inductive families to encode our invariants ("syntax")
  - take advantage of this precision to host these domain-specific languages ("semantics")

The vision: `The Proof Assistant as an Integrated Development Environment`_


..
  ::
  showNat : ℕ → String
  showNat zero    = "0"
  showNat (suc n) = "S(" ++ showNat n ++ ")"

************************************************
Typing ``sprintf``
************************************************

..
  ::

  module Format where

    open import Data.Char

    open import Function

Our introductory example is a Classic, introduced by Lennart
Augustsson in his seminal paper on `Cayenne`_. In plain ML (*ie.*
without GADTs), the ``sprintf`` function cannot be given an ML type:
the value of its arguments depending on the user-provided format.

.. code-block:: guess

   sprintf "foo %d"    : ℕ → String
   sprintf "bar %s"    : String → String
   sprintf "baz %d %s" : ℕ → String → String

Formats are not random strings of characters:
  - structure = syntax (`format`)
  - from string to structure = parser

::

    data format : Set where
      digit  : (k : format) → format
      string : (k : format) → format
      symb   : (c : Char)(k : format) → format
      end    : format

    parse : List Char → format
    parse ('%' ∷ 'd' ∷ cs ) = digit (parse cs)
    parse ('%' ∷ 's' ∷ cs ) = string (parse cs)
    parse ('%' ∷ c ∷ cs )   = symb c (parse cs)
    parse ( c ∷ cs)         = symb c (parse cs)
    parse []                = end

We can *embed* the semantics of a format by describing its meaning
within Agda itself::

    ⟦_⟧ : format → Set
    ⟦ digit k ⟧  = ℕ → ⟦ k ⟧
    ⟦ string k ⟧ = String → ⟦ k ⟧
    ⟦ symb c k ⟧ = ⟦ k ⟧
    ⟦ end ⟧      = String

    ⟦p_⟧ : String → Set
    ⟦p_⟧ = ⟦_⟧ ∘ parse ∘ toList


And we can easily realize this semantics::

    eval : (fmt : format) → String → ⟦ fmt ⟧
    eval (digit k) acc  = λ n → eval k (acc ++ showNat n)
    eval (string k) acc = λ s → eval k (acc ++ s)
    eval (symb c k) acc = eval k (acc ++ fromList (c ∷ []))
    eval end acc        = acc

    sprintf : (fmt : String) → ⟦p fmt ⟧
    sprintf fmt = eval (parse (toList fmt)) ""

``sprintf`` can thus be seen as an interpreter for a small language
(whose AST is described by ``format``) to the semantic domain
described by ``⟦_⟧``. And it works::

    test : sprintf "test %%d & %%s: %d & %s" 2 "hello world!"
           ≡ "test %d & %s: S(S(0)) & hello world!"
    test = refl

**Exercise (difficulty: 1)** Print ``%d`` using decimal numbers instead of Peano numbers

**Exercise (difficulty: 3)** Add support for the format ``%.ns`` where
`n` is a (decimal) number representing the maximum size of the prefix
of the string ``s`` to be printed. Careful, the formats ``%.s`` or
``%.cs`` are non-sensical: this should impact either parsing or
interpretation.

************************************************
Mostly correct-by-construction compiler
************************************************

..
  ::

  module Compiler where

    infixr 5 _∙_
    infixr 5 _#_

Using dependent types (in particular, inductive families), we can bake
our invariants in the datatypes we manipulate and make sure that they
are preserved as we process them. The advantage is twofold:

  - build *initial* models of a domain of interest (syntax!)
  - total denotational semantics in Agda itself (interpreter!)

We illustrate this approach with another Classic, a draft of James
McKinna & Joel Wright entitled `A type-correct, stack-safe, provably
correct, expression compiler`_. As suggested by the title, we are
going to implement a correct-by-construction compiler from a language
of expressions to a stack machine.

--------------------------------
Type-safe representation
--------------------------------

Because Agda's type system is extremely rich, we can in fact *absorb*
the type discipline of expressions in Agda. In programming terms, we
define a datatype ``exp`` that represents only well-typed expressions::

    data typ : Set where
       nat bool : typ

    sem : typ → Set
    sem nat  = ℕ
    sem bool = Bool

    data exp : typ → Set where
      val  : ∀ {T} → (v : sem T) → exp T
      plus : (e₁ e₂ : exp nat) → exp nat
      ifte : ∀ {T} → (c : exp bool)(e₁ e₂ : exp T) → exp T

We define the semantics of this language by interpretation within
Agda::

    eval : ∀ {T} → exp T → sem T
    eval (val v)        = v
    eval (plus e₁ e₂)   = eval e₁ + eval e₂
    eval (ifte c e₁ e₂) = if eval c then eval e₁ else eval e₂

If we were pedantic, we would call this a *denotational*
semantics.

Note that we crucially rely on the fact that ``sem`` computes at the
type level to ensure that, for example, the ``if_then_else_`` is
performed on a Boolean and not a natural number. This is called a
*tagless* interpreter. In a non-dependent setting, values would have
carried a tag (discriminating them based on their type) and the
evaluator would have to deal with type errors dynamically::

    module Tagged where

      data value : Set where
        isNat  : (n : ℕ) → value
        isBool : (b : Bool) → value

      data exp' : Set where
        val  : (v : value) → exp'
        plus : (e₁ e₂ : exp') → exp'
        ifte : (c e₁ e₂ : exp') → exp'

      eval' : exp' → Maybe value
      eval' (val v) = just v
      eval' (plus e₁ e₂)
        with eval' e₁ | eval' e₂
      ... | just (isNat n₁)
          | just (isNat n₂) = just (isNat (n₁ + n₂))
      ... | _ | _ = nothing
      eval' (ifte c e₁ e₂)
        with eval' c | eval' e₁ | eval' e₂
      ... | just (isBool b) | v₁ | v₂ = if b then v₁ else v₂
      ... | _ | _ | _ = nothing

**Exercise (difficulty: 1)** The above implementation is needlessly
verbose, use the Maybe monad to hide the treatment of errors.

The moral of this implementation is that we failed to encode our
invariant in the datatype ``exp'`` and paid the price in the
implementation of ``eval'``.

--------------------------------
Stack machine
--------------------------------

Our stack machine will interpret a fixed set of opcodes, transforming
input stack to output stack. A stack will contain values,
ie. Booleans or integers. We can therefore describe well-typed stacks
by identifying the type of each elements::

    stack-typ = List typ

    data stack : stack-typ → Set where
      ε   : stack []
      _∙_ : ∀ {T σ} → sem T → stack σ → stack (T ∷ σ)


In particular, a non-empty stack allows us to peek at the top element
and to take its tail::

    top : ∀ {T σ} → stack (T ∷ σ) → sem T
    top (t ∙ _) = t

    tail : ∀ {T σ} → stack (T ∷ σ) → stack σ
    tail (_ ∙ s) = s

Using an inductive family, we can once again garantee that
instructions are only applied onto well-formed and well-typed stacks::

    data code : stack-typ → stack-typ → Set where
      skip : ∀ {σ} → code σ σ
      _#_  : ∀ {σ₁ σ₂ σ₃} → (c₁ : code σ₁ σ₂)(c₂ : code σ₂ σ₃) → code σ₁ σ₃
      PUSH : ∀ {T σ} → (v : sem T) → code σ (T ∷ σ)
      ADD  : ∀ {σ} → code (nat ∷ nat ∷ σ) (nat ∷ σ)
      IFTE : ∀ {σ₁ σ₂} → (c₁ c₂ : code σ₁ σ₂) → code (bool ∷ σ₁) σ₂

As a result, we can implement a (total) interpreter for our stack
machine::

    exec : ∀ {σ-i σ-f} → code σ-i σ-f → stack σ-i → stack σ-f
    exec skip s                   = s
    exec (c₁ # c₂) s              = exec c₂ (exec c₁ s)
    exec (PUSH v) s               = v ∙ s
    exec ADD (x₁ ∙ x₂ ∙ s)        = x₁ + x₂ ∙ s
    exec (IFTE c₁ c₂) (true ∙ s)  = exec c₁ s
    exec (IFTE c₁ c₂) (false ∙ s) = exec c₂ s

**Exercise (difficulty: 1)** Implement a simply-typed version of
``code`` and update ``exec`` to work (partially) from list of tagged
values to list of tagged values.

--------------------------------
Compilation
--------------------------------

The compiler from expressions to stack machine code is then
straightforward, the types making sure that we cannot generate
non-sensical opcodes::

    compile : ∀ {T σ} → exp T → code σ (T ∷ σ)
    compile (val v)        = PUSH v
    compile (plus e₁ e₂)   = compile e₂ # compile e₁ # ADD
    compile (ifte c e₁ e₂) = compile c # IFTE (compile e₁) (compile e₂)

**Exercise (difficulty: 1)** Implement the (same) compiler on the
simply-typed representation of expressions ``exp'``.

Note that this does not guarantee that we preserve the semantics!

**Exercise (difficulty: 4)** We could address that remark by indexing
expressions (``exp``) not only by their type but also by their
denotation (a natural number):

.. code-block:: guess

    expSem : (T : typ) → ⟦ T ⟧ → Set

Similarly, the stack machine opcodes could be indexed by their
denotation (a stack):

.. code-block:: guess

    codeSem : (σ : stack-typ) → stack σ → Set

As a result, a type-safe ``compile`` function from ``expSem`` to
``codeSem`` could ensure semantics-preservation by
construction. Implement these source and target languages and the
correct-by-construction compiler.


--------------------------------
Correctness
--------------------------------

The correctness proof amounts to showing that the interpreter for
expressions agrees with the result of executing the stack
machine. Having baked the typing discipline in our input expressions
and output machine codes, we can focus on proving only the meaningful
cases::

    correctness : forall {T σ} → (e : exp T)(s : stack σ) → exec (compile e) s ≡ eval e ∙ s
    correctness (val v) s = refl
    correctness (plus e₁ e₂) s
      rewrite correctness e₂ s
              | correctness e₁ (eval e₂ ∙ s) = refl
    correctness (ifte c e₁ e₂) s
      rewrite correctness c s
      with eval c
    ... | true rewrite correctness e₁ s = refl
    ... | false rewrite correctness e₂ s = refl


**Exercise (difficulty: 2)** Prove the same theorem one the
simply-typed implementations. You may prefer to work in Coq, so as to
take advantage of tactics to automate the tedium.


This exercise has its roots in the very origin of most programming and
reasoning techniques we take for granted today:

  - the role of initiality in formal reasoning
  - the importance of equational reasoning for proving program correctness

These ideas were, for examples, in their inception at the first
edition of POPL with `Advice on structuring compilers and proving them
correct`_ (1973), which was further refined by `More on advice on
structuring compilers and proving them correct`_, (1980). This
reflects the influence it had on a generation of computer scientists
interested in language design on one hand (they gave us algebraic
datatypes) and verified compilation on the other hand (they gave us
denotational models).

************************************************
Computing normal forms of λ-terms
************************************************

In Lecture 1, we have seen that, by finding a suitable semantics
domain, we could auto-magically compute normal forms for monadic
programs. Could we do the same for the whole (effect-free) λ-calculus?

..
  ::

  module STLC where

    infix 35 _∈_
    infixl 40 _▹_
    infixr 50 _⇒_
    infixr 55 _*_
    infix 60 _!_

--------------------------------
Types and terms
--------------------------------

We consider the simply-typed λ-calculus, whose grammar of types and
contexts is as follows::

    data type : Set where
      unit    : type
      _⇒_ _*_ : (S T : type) → type

    data context : Set where
      ε   : context
      _▹_ : (Γ : context)(T : type) → context

Thanks to inductive families, we can represent *exactly* the
well-scoped and well-typed λ-terms::

    data _∈_ (T : type) : context → Set where
      here  : ∀ {Γ} → T ∈ Γ ▹ T
      there : ∀{Γ T'} → (h : T ∈ Γ) → T ∈ Γ ▹ T'

    data _⊢_ (Γ : context) : type → Set where
      lam : ∀{S T} →

          (b : Γ ▹ S ⊢ T) →
          ---------------
          Γ ⊢ S ⇒ T

      var : ∀{T} →

          (v : T ∈ Γ) →
          -----------
          Γ ⊢ T

      _!_ : ∀{S T} →

          (f : Γ ⊢ S ⇒ T)(s : Γ ⊢ S) →
          --------------------------
          Γ ⊢ T

      tt :

          --------
          Γ ⊢ unit

      pair : ∀{A B} →

          (a : Γ ⊢ A)(b : Γ ⊢ B) →
          ----------------------
          Γ ⊢ A * B

      fst : ∀{A B} →

          Γ ⊢ A * B →
          ---------
          Γ ⊢ A

      snd : ∀{A B} →

          Γ ⊢ A * B →
          ---------
          Γ ⊢ B

This representation of λ-terms is folklore amongst programmers of the
dependent kind. A comprehensive discussion of its pros and cons can be
found in the pedagogical `Strongly Typed Term Representations in
Coq`_.

-------------------------------------
Interlude: substitution, structurally
-------------------------------------

Substitution for de Bruijn λ-terms is usually (offhandedly) specified
in the following manner:

.. code-block:: guess

    n [σ]    = σ(n)
    (M N)[σ] = M[σ] N[σ]
    (λ M)[σ] = λ (M[0 · (σ ∘ λ n. suc n)])

    σ ∘ ρ    = λ n. (σ n)[ρ]

However, this definition contains a fair amount of mutual recursion,
whose validity is not obvious and will be a hard sell to a termination
checker. Let us exhibit this structure and, at the same time, exercise
ourselves in the art of unearthing initial models.

..
  ::

    module Exercise-mono where

      open import Data.Fin

**Exercise (difficulty: 2)** In Agda, the type of finite sets of
cardinality ``n`` is defined by an inductive family:

.. code-block:: guess

  data Fin : ℕ → Set where
    zero : {n : ℕ} → Fin (suc n)
    suc  : {n : ℕ} (i : Fin n) → Fin (suc n)

We are interested in **monotone** functions from ``Fin n`` to ``Fin
m``. We could obviously formalize this class of functions as "any
function from ``Fin n`` to ``Fin m`` as long as it is monotone"
however a more *intentional* characterization can be given by means of
an inductive family::

      data _⊇_ : (m : ℕ)(n : ℕ) → Set where
        -- COMPLETE

Intuitively, this datatype provides a grammar of monotone functions,
which we can then interpret back into actual (monotone) functions::

      ⟦_⟧ : ∀ {m n} → m ⊇ n → Fin n → Fin m
      ⟦ wk ⟧ k = {!!}

      lemma-valid : ∀{m n k l} → (wk : m ⊇ n) → k ≤ l → ⟦ wk ⟧ k ≤ ⟦ wk ⟧ l
      lemma-valid = {!!}


We can adapt this intentional characterization of monotone functions
to typed embeddings::

    data _⊇_ : context → context → Set where
      id    : ∀ {Γ} → Γ ⊇ Γ
      weak1 : ∀ {Γ Δ A} → (wk : Δ ⊇ Γ) → Δ ▹ A ⊇ Γ
      weak2 : ∀ {Γ Δ A} → (wk : Δ ⊇ Γ) → Δ ▹ A ⊇ Γ ▹ A

    shift : ∀ {Γ Δ T} → Γ ⊇ Δ → T ∈ Δ → T ∈ Γ
    shift id v                 = v
    shift (weak1 wk) v         = there (shift wk v)
    shift (weak2 wk) here      = here
    shift (weak2 wk) (there v) = there (shift wk v)

    rename : ∀ {Γ Δ T} → Γ ⊇ Δ → Δ ⊢ T → Γ ⊢ T
    rename wk (lam t)    = lam (rename (weak2 wk) t)
    rename wk (var v)    = var (shift wk v)
    rename wk (f ! s)    = rename wk f ! rename wk s
    rename wk tt         = tt
    rename wk (pair a b) = pair (rename wk a) (rename wk b)
    rename wk (fst p)    = fst (rename wk p)
    rename wk (snd p)    = snd (rename wk p)

    sub : ∀ {Γ Δ T} → Γ ⊢ T → (∀ {S} → S ∈ Γ →  Δ ⊢ S) → Δ ⊢ T
    sub (lam t) ρ    = lam (sub t (λ { here      → var here ;
                                       (there v) → rename (weak1 id) (ρ v) }))
    sub (var v) ρ    = ρ v
    sub (f ! s) ρ    = sub f ρ ! sub s ρ
    sub tt ρ         = tt
    sub (pair a b) ρ = pair (sub a ρ) (sub b ρ)
    sub (fst p) ρ    = fst (sub p ρ)
    sub (snd p) ρ    = snd (sub p ρ)

    sub1 : ∀ {Γ S T} → Γ ▹ S ⊢ T → Γ ⊢ S → Γ ⊢ T
    sub1 t s = sub t (λ { here → s ; (there v) → var v })

A formal treatment of this construction can be found in `Formalized
metatheory with terms represented by an indexed family of types`_, for
example.



**Exercise (difficulty: 2)** Weakenings interpret to renaming
functions and functions do compose so we are naturally driven to
implement composition directly on renamings::

    _∘wk_ : ∀ {Δ ∇ Γ} → Δ ⊇ ∇ → Γ ⊇ Δ → Γ ⊇ ∇
    _∘wk_ = {!!}

And we must make sure, that this notion of composition is the *right*
one::

    lemma-right-unit : ∀ {Γ Δ} → (wk : Γ ⊇ Δ) → wk ∘wk id ≡ wk
    lemma-right-unit = {!!}

    lemma-left-unit : ∀ {Γ Δ} → (wk : Γ ⊇ Δ) → id ∘wk wk ≡ wk
    lemma-left-unit = {!!}

    lemma-assoc : ∀ {Γ Δ ∇ Ω} → (wk₃ : Γ ⊇ Δ)(wk₂ : Δ ⊇ ∇)(wk₁ : ∇ ⊇ Ω) →
      (wk₁ ∘wk wk₂) ∘wk wk₃ ≡ wk₁ ∘wk (wk₂ ∘wk wk₃)
    lemma-assoc = {!!}




-------------------------------------
Normal forms
-------------------------------------


We can represent the equation theory as an inductive family::

    data _⊢_∋_↝βη_ : (Γ : context)(T : type) → Γ ⊢ T → Γ ⊢ T → Set where
      rule-β : ∀{Γ S T}{b : Γ ▹ S ⊢ T}{s : Γ ⊢ S} →

        ------------------------------------
        Γ ⊢ T ∋ (lam b) ! s ↝βη sub1 b s

      rule-η-fun : ∀{Γ S T}{f : Γ ⊢ S ⇒ T} →

        ------------------------------------------------------
        Γ ⊢ S ⇒ T ∋ f ↝βη lam (rename (weak1 id) f ! var here)

      rule-η-pair : ∀{Γ A B}{p : Γ ⊢ A * B} →

        ------------------------------------------------------
        Γ ⊢ A * B ∋ p ↝βη pair (fst p) (snd p)


    data _⊢_∋_∼βη_  : (Γ : context)(T : type) → Γ ⊢ T → Γ ⊢ T → Set where
      inc : ∀ {Γ T t₁ t₂} →

        Γ ⊢ T ∋ t₁ ↝βη t₂ →
        -----------------
        Γ ⊢ T ∋ t₁ ∼βη t₂


      reflexivity : ∀{Γ T t} →

        -----------
        Γ ⊢ T ∋ t ∼βη t

      symmetry : ∀{Γ T t t'} →

        Γ ⊢ T ∋ t ∼βη t' →
        ------------
        Γ ⊢ T ∋ t' ∼βη t

      transitivity : ∀{Γ T t t' t''} →

        Γ ⊢ T ∋ t ∼βη t' →
        Γ ⊢ T ∋ t' ∼βη t'' →
        --------------
        Γ ⊢ T ∋ t ∼βη t''

      struct-lam : ∀{Γ S T b b'} →

        Γ ▹ S ⊢ T ∋ b ∼βη b' →
        ----------------
        Γ ⊢ S ⇒ T ∋ lam b ∼βη lam b'

      struct-! : ∀{Γ S T f f' s s'} →

        Γ ⊢ S ⇒ T ∋ f ∼βη f' →
        Γ ⊢ S ∋ s ∼βη s' →
        -----------------
        Γ ⊢ T ∋ f ! s ∼βη f' ! s'

      struct-pair : ∀{Γ A B a a' b b'} →

        Γ ⊢ A ∋ a ∼βη a' →
        Γ ⊢ B ∋ b ∼βη b' →
        ----------------
        Γ ⊢ A * B ∋ pair a b ∼βη pair a' b'

      struct-fst : ∀{Γ A B p p'} →

        Γ ⊢ A * B ∋ p ∼βη p' →
        ------------------------
        Γ ⊢ A ∋ fst p ∼βη fst p'

      struct-snd : ∀{Γ A B p p'} →

        Γ ⊢ A * B ∋ p ∼βη p' →
        ------------------------
        Γ ⊢ B ∋ snd p ∼βη snd p'

..
  ::

  module NBE-gensym where

    open STLC

Compute η-long β-normal forms for the simply typed λ-calculus:
  - define a representation of terms (``term``)
  - interpret types and contexts in this syntactic model (``⟦_⟧`` and ``⟦_⟧context``)
  - interpret terms in this syntactic model (``eval``)

::

    data term : Set where
       lam  : (v : String)(b : term) → term
       var  : (v : String) → term
       _!_  : (f : term)(s : term) → term
       tt   : term
       pair : (x y : term) → term
       fst  : (p : term) → term
       snd  : (p : term) → term

    ⟦_⟧Type : type → Set
    ⟦ unit ⟧Type  = term
    ⟦ S ⇒ T ⟧Type = ⟦ S ⟧Type → ⟦ T ⟧Type
    ⟦ S * T ⟧Type = ⟦ S ⟧Type × ⟦ T ⟧Type

    ⟦_⟧context : context → Set
    ⟦ ε ⟧context     = ⊤
    ⟦ Γ ▹ T ⟧context = ⟦ Γ ⟧context × ⟦ T ⟧Type

    _⊩_ : context → type → Set
    Γ ⊩ T = ⟦ Γ ⟧context → ⟦ T ⟧Type

    lookup : ∀{Γ T} → T ∈ Γ → Γ ⊩ T
    lookup here (_ , x)      = x
    lookup (there h) (γ , _) = lookup h γ

    eval : ∀{Γ T} → Γ ⊢ T → Γ ⊩ T
    eval (var v) ρ    = lookup v ρ
    eval (f ! s) ρ    = eval f ρ (eval s ρ)
    eval (lam b) ρ    = λ s → eval b (ρ , s)
    eval (pair a b) ρ = eval a ρ , eval b ρ
    eval (fst p) ρ    = proj₁ (eval p ρ)
    eval (snd p) ρ    = proj₂ (eval p ρ)
    eval tt ρ         = tt


This is an old technique, introduced by Per Martin-Löf in `About
Models for Intuitionistic Type Theories and the Notion of Definitional
Equality`_, applied by Coquand & Dybjer to the simply-typed λ-calculus
in `Intuitionistic Model Constructions and Normalization Proofs`_.

..
  ::

    module Axiom where


Let us, for simplicity, assume that we have access to fresh name
generator, ``gensym``::

      postulate gensym : ⊤ → String

This would be the case if we were to write this program in OCaml, for
instance.

We could then back-translate the objects in the model (``⟦_⟧Type``)
back to raw terms (through ``reify``). However, to do so, one needs to
inject variables *in η-long normal form* into the model: this is the
role of ``reflect``::

      reify : ∀{T} → ⟦ T ⟧Type → term
      reflect : (T : type) → term → ⟦ T ⟧Type

      reify {unit} nf       = nf
      reify {A * B} (x , y) = pair (reify x) (reify y)
      reify {S ⇒ T} f       = let s = gensym tt in
                              lam s (reify (f (reflect S (var s))))

      reflect unit nf     = nf
      reflect (A * B) nf  = reflect A (fst nf) , reflect B (snd nf)
      reflect (S ⇒ T) neu = λ s → reflect T (neu ! reify s)

Given a λ-term, we can thus compute its normal form::

      norm :  ∀{Γ T} → Γ ⊢ T → term
      norm {Γ} Δ = reify (eval Δ (idC Γ))
        where idC : ∀ Γ → ⟦ Γ ⟧context
              idC ε       = tt
              idC (Γ ▹ T) = idC Γ , reflect T (var (gensym tt))


Just like in the previous lecture (and assuming that we have proved
the soundness of this procedure with respect to the equational theory
``_⊢_∋_∼βη_``), we can use it to check whether any two terms belong to
the same congruence class by comparing their normal forms::

      term₁ : ε ⊢ (unit ⇒ unit) ⇒ unit ⇒ unit
      term₁ =
        -- λ s. λ z. s (s z)
        lam (lam (var (there here) ! (var (there here) ! var here)))

      term₂ : ε ⊢ (unit ⇒ unit) ⇒ unit ⇒ unit
      term₂ =
        -- λ s. (λ r λ z. r (s z)) (λ x. s x)
        lam (lam (lam (var (there here) ! (var (there (there here)) ! var here))) ! lam (var (there here) ! var here))

      test-nbe : norm term₁ ≡ norm term₂
      test-nbe = refl

For instance, thanks to a suitable model construction, we have
surjective pairing::

      term₃ : ε ⊢ unit * unit ⇒ unit * unit
      term₃ =
        -- λ p. p
        lam (var here)

      term₄ : ε ⊢ unit * unit ⇒ unit * unit
      term₄ =
        -- λ p. (fst p, snd p)
        lam (pair (fst (var here)) (snd (var here)))

      test-nbe₂ : norm term₃ ≡ norm term₄
      test-nbe₂ = refl

**Exercise (difficulty: 4)** Modify the model so as to remove
surjective pairing (``rule-η-pair`` would not be valid) while
retaining the usual η-rule for functions (``rule-η-fun``). Hint: we
have used the *negative* presentation of products which naturally
leads to a model enabling η for pair. Using the *positive*
presentation would naturally lead to one in which surjective pairing
is not valid.

However, this implementation is a bit of wishful thinking: we do not
have a ``gensym``! So the following is also true, for the bad reason
that ``gensym`` is not actually producing unique names but always the
*same* name (itself)::


      term₅ : ε ⊢ unit ⇒ unit ⇒ unit
      term₅ =
        -- λ z₁ z₂. z₁
        lam (lam (var (there here)))

      term₆ : ε ⊢ unit ⇒ unit ⇒ unit
      term₆ =
        -- λ z₁ z₂. z₂
        lam (lam (var here))

      test-nbe₃ : norm term₅ ≡ norm term₆
      test-nbe₃ = refl -- BUG!

..
  ::

    module Impossible where

This might not deter the brave monadic programmer: we can emulate
``gensym`` using a reenactment of the state monad::

      Fresh : Set → Set
      Fresh A = ℕ → A × ℕ

      gensym : ⊤ → Fresh String
      gensym tt = λ n → showNat n , 1 + n

      return : ∀ {A} → A → Fresh A
      return a = λ n → (a , n)

      _>>=_ : ∀ {A B} → Fresh A → (A → Fresh B) → Fresh B
      m >>= k = λ n → let (a , n') = m n in k a n'

      run : ∀ {A} → Fresh A → A
      run f = proj₁ (f 0)

We then simply translate the previous code to a monadic style, a
computer could do it automatically::

      mutual
        reify : ∀{T} → ⟦ T ⟧Type → Fresh term
        reify {unit} nf       = return nf
        reify {A * B} (a , b) = reify a >>= λ a →
                                reify b >>= λ b →
                                return (pair a b)
        reify {S ⇒ T} f       = gensym tt >>= λ s →
                                reflect S (var s) >>= λ t →
                                reify (f t) >>= λ b →
                                return (lam s b)

        reflect : (T : type) → term → Fresh ⟦ T ⟧Type
        reflect unit nf     = return nf
        reflect (A * B) nf  = reflect A (fst nf) >>= λ a →
                              reflect B (snd nf) >>= λ b →
                              return (a , b)
        reflect (S ⇒ T) neu = return (λ s → {!!})
          -- XXX: cannot conclude with `reflect T (neu ! reify s)`

Excepted that, try as we might, we cannot reflect a function.

**Exercise (difficulty: 1)** Try (very hard) at home. Come up with a
simple explanation justifying why it is impossible.

**Exercise (difficulty: 3)** Inspired by this failed attempt, modify
the syntactic model with the smallest possible change so as to be able
to implement ``reify``, ``reflect`` and obtain a valid normalisaton
function. Hint: a solution is presented in `Normalization and Partial
Evaluation`_.

-------------------------------------
The Rising Sea
-------------------------------------

..
  ::

  module NBE-Presheaf where

    open STLC

    infix 30 _⊢Nf_
    infix 30 _⊢Ne_
    infix 40 _⟶_
    infix 45 _⇒̂_
    infix 50 _×̂_
    infix 30 _⊩_


Rather than hack our model, I propose to gear up and let the sea rise
because "when the time is ripe, hand pressure is enough". Another
argument against incrementally improving our model is its fragility:
whilst our source language is well structured (well-scoped, well-typed
λ-terms), our target language (raw λ-terms) is completely
destructured, guaranteeing neither that we actually produce normal
forms, nor that it is well-typed not even proper scoping.

To remedy this, let us
  - precisely describe η-long β-normal forms
  - check that they embed back into well-typed, well-scoped terms

::

    data _⊢Nf_ (Γ : context) : type → Set
    data _⊢Ne_ (Γ : context) : type → Set

    data _⊢Nf_ (Γ : context) where
         lam    : ∀ {S T} → (b : Γ ▹ S ⊢Nf T) → Γ ⊢Nf S ⇒ T
         pair   : ∀ {A B} → Γ ⊢Nf A → Γ ⊢Nf B → Γ ⊢Nf A * B
         tt     : Γ ⊢Nf unit
         ground : (grnd : Γ ⊢Ne unit) → Γ ⊢Nf unit

    data _⊢Ne_ (Γ : context) where
       var : ∀{T} → (v : T ∈ Γ) → Γ ⊢Ne T
       _!_ : ∀{S T} → (f : Γ ⊢Ne S ⇒ T)(s : Γ ⊢Nf S) → Γ ⊢Ne T
       fst : ∀ {A B} → (p : Γ ⊢Ne A * B) → Γ ⊢Ne A
       snd : ∀ {A B} → (p : Γ ⊢Ne A * B) → Γ ⊢Ne B

    ⌊_⌋Ne : ∀{Γ T} → Γ ⊢Ne T → Γ ⊢ T
    ⌊_⌋Nf : ∀{Γ T} → Γ ⊢Nf T → Γ ⊢ T

    ⌊ lam b ⌋Nf       = lam ⌊ b ⌋Nf
    ⌊ ground grnd ⌋Nf = ⌊ grnd ⌋Ne
    ⌊ pair a b ⌋Nf    = pair ⌊ a ⌋Nf ⌊ b ⌋Nf
    ⌊ tt ⌋Nf          = tt

    ⌊ var v ⌋Ne       = var v
    ⌊ f ! s ⌋Ne       = ⌊ f ⌋Ne ! ⌊ s ⌋Nf
    ⌊ fst p ⌋Ne       = fst ⌊ p ⌋Ne
    ⌊ snd p ⌋Ne       = snd ⌊ p ⌋Ne


We are going to construct a context-and-type-indexed model

.. code-block:: guess

    [_]⊩_ : context → type → Set

(reading ``[ Γ ]⊩ T`` as "an interpretation of ``T`` in context ``Γ``)
so as to ensure that the normal forms we produce by reification are
well-typed and well-scoped (and, conversely, to ensure that the
neutral terms we reflect are necessarily well-typed and
well-scoped). The types of ``reify`` and ``reflect`` thus become:

.. code-block:: guess

    reify   : ∀ {Γ T} → [ Γ ]⊩ T  → Γ ⊢Nf T
    reflect : ∀ {Γ} → (T : type) → Γ ⊢Ne T → [ Γ ]⊩ T

However, we expect some head-scratching when implementing ``reify`` on
functions: this is precisely were we needed the ``gensym`` earlier. We
can safely assume that function application is admissible in our
model, ie. we have an object

.. code-block:: guess

    app : ∀ {Γ S T} → [ Γ ]⊩ S ⇒ T → [ Γ ]⊩ S → [ Γ ]⊩ T

Similarly, using ``reflect``, we can easily lift the judgment ``var
here : Γ ▹ S ⊢ S`` into the model:

.. code-block:: guess

    reflect S (var here) : [ Γ ▹ S ]⊩ S

It is therefore tempting to implement the function case of ``reify``
as follows:

.. code-block:: guess

    reify {S ⇒ T} f = lam (reify (app f (reflect S (var here))))

However, ``f`` has type ``[ Γ ]⊩ S ⇒ T`` and we are working under a
lambda, in the context ``Γ ▹ S``. We need a weakening operator
(denoted ``ren``) in the model! Then we could just write:

.. code-block:: guess

    reify {S ⇒ T} f = lam (reify (app (ren (weak1 id) f) (reflect S (var here))))

**Remark:** We do not make the mistake of considering a (simpler)
weakening from ``Γ`` to ``Γ ▹ S``. As usual (eg. ``rename`` function
earlier), such a specification would not be sufficiently general and
we would be stuck when trying to go through another binder. Even
though we only use it with ``weak1 id``, the weakening operator must
therefore be defined over any weakening.

Translating these intuitions into a formal definition, this means that
our semantics objects are context-indexed families that come equipped
with renaming operation::

    record Sem : Set₁ where
      field
        _⊢ : context → Set
        ren : ∀ {Γ Δ} → Γ ⊇ Δ → Δ ⊢ → Γ ⊢

An implication in ``Sem`` is a family of implications for each context::

    _⟶_ : (P Q : Sem) → Set
    P ⟶ Q = ∀ {Γ} → Γ ⊢P → Γ ⊢Q
      where open Sem P renaming (_⊢ to _⊢P)
            open Sem Q renaming (_⊢ to _⊢Q)

We easily check that normal forms and neutral terms implement this
interface::

    rename-Nf : ∀{Γ Δ T} → Γ ⊇ Δ → Δ ⊢Nf T → Γ ⊢Nf T
    rename-Ne : ∀{Γ Δ T} → Γ ⊇ Δ → Δ ⊢Ne T → Γ ⊢Ne T

    rename-Nf wk (lam b)       = lam (rename-Nf (weak2 wk) b)
    rename-Nf wk (ground grnd) = ground (rename-Ne wk grnd)
    rename-Nf wk (pair a b)    = pair (rename-Nf wk a) (rename-Nf wk b)
    rename-Nf wk tt            = tt

    rename-Ne wk (var v)       = var (shift wk v)
    rename-Ne wk (f ! s)       = (rename-Ne wk f) ! (rename-Nf wk s)
    rename-Ne wk (fst p)       = fst (rename-Ne wk p)
    rename-Ne wk (snd p)       = snd (rename-Ne wk p)

    Nf̂ : type → Sem
    Nf̂ T = record { _⊢ = λ Γ → Γ ⊢Nf T
                  ; ren = rename-Nf }

    Nê : type → Sem
    Nê T = record { _⊢ = λ Γ → Γ ⊢Ne T
                  ; ren = rename-Ne }

Following our earlier model, we will interpret the ``unit`` type as
the normal forms of type unit::

    ⊤̂ : Sem
    ⊤̂ =  Nf̂ unit

    TT : ∀ {P} → P ⟶ ⊤̂
    TT ρ = tt

Similarly, we will interpret the ``_*_`` type as a product in
``Sem``, defined in a pointwise manner::

    _×̂_ : Sem → Sem → Sem
    P ×̂ Q = record { _⊢ = λ Γ → Γ ⊢P × Γ ⊢Q
                   ; ren = λ { wk (x , y) → ( ren-P wk x , ren-Q wk y ) } }
      where open Sem P renaming (_⊢ to _⊢P ; ren to ren-P)
            open Sem Q renaming (_⊢ to _⊢Q ; ren to ren-Q)

    PAIR : ∀ {P Q R} → P ⟶ Q → P ⟶ R → P ⟶ Q ×̂ R
    PAIR a b ρ = a ρ , b ρ

    FST : ∀ {P Q R} → P ⟶ Q ×̂ R → P ⟶ Q
    FST p ρ = proj₁ (p ρ)

    SND : ∀ {P Q R} → P ⟶ Q ×̂ R → P ⟶ R
    SND p ρ = proj₂ (p ρ)

We may be tempted to define the exponential in a pointwise manner too:

.. code-block:: guess

    _⇒̂_ : Sem → Sem → Sem
    P ⇒̂ Q = record { _⊢ = λ Γ → Γ ⊢P → Γ ⊢Q
                   ; ren = ?! }
      where open Sem P renaming (_⊢ to _⊢P)
            open Sem Q renaming (_⊢ to _⊢Q)

However, we are bitten by the contra-variance of the domain: there is
no way to implement ``ren`` with such a definition.

-------------------------------------
Interlude: Yoneda lemma
-------------------------------------

..
  ::

    module Yoneda (T : Sem)(Γ : context) where

      open Sem T renaming (_⊢ to _⊢T ; ren to ren-T)

Let ``_⊢T : context → Set`` be a semantics objects together with its
weakening operator ``ren-T : Γ ⊇ Δ → Δ ⊢T → Γ ⊢T``. By mere
application of ``ren-T``, we can implement::

      ψ : Γ ⊢T → (∀ {Δ} → Δ ⊇ Γ → Δ ⊢T)
      ψ t wk = ren-T wk t

were the ``∀ {Δ} →`` quantifier of the codomain type must be
understood in polymorphic sense. Surprisingly (perhaps), we can go
from the polymorphic function back to a single element, by providing
the ``id`` continuation::

      φ : (∀ {Δ} → Δ ⊇ Γ → Δ ⊢T) → Γ ⊢T
      φ k = k id

One could then prove that this establishes an isomorphism, for all
``Γ``::

      postulate
        ψ∘φ≡id : ψ ∘ φ ≡ λ k → k
        φ∘ψ≡id : φ ∘ ψ ≡ λ t → t

**Exercise (difficulty: 4)** To prove this, we need to structural
results on Sem, which we have eluded for now (because they are not
necessary for programming). Typically, we would expect that ``ren`` on
the identity weakening ``id`` behaves like an identity, etc. Complete
the previous definitions so as to provide these structural lemmas and
prove the isomorphism.

A slightly more abstract way of presenting this isomorphism consists
in noticing that any downward-closed set of context forms a valid
semantics objects. ``φ`` and ``ψ`` can thus be read as establishing an
isomorphism between the object ``Γ ⊢T`` and the morphisms in ``⊇[ Γ ]
⟶ T``::

      ⊇[_] : context → Sem
      ⊇[ Γ ] = record { _⊢ = λ Δ → Δ ⊇ Γ
                      ; ren = λ wk₁ wk₂ → wk₂ ∘wk wk₁ }

      ψ' : Γ ⊢T → ⊇[ Γ ] ⟶ T
      ψ' t wk = ren-T wk t

      φ' : ⊇[ Γ ] ⟶ T → Γ ⊢T
      φ' k = k id


Being isomorphic to ``_ ⊢T``, we expect the type ``λ Γ → ∀ {Δ} → Δ ⊇ Γ
→ Δ ⊢T`` to be a valid semantic object. This is indeed the case, where
renaming merely lifts composition of weakening::

      Y : Sem
      Y = record { _⊢ = λ Γ → ∀ {Δ} → Δ ⊇ Γ → Δ ⊢T
                 ; ren = λ wk₁ k wk₂ → k (wk₁ ∘wk wk₂) }


Note that ``Y`` does not depend on ``ren-T``: it is actually baked in
the very definition of ``_⊢``!

-------------------------------------
Back to the Sea
-------------------------------------


Let us assume that the exponential ``P ⇒̂ Q : Sem`` exists. This means,
in particular, that it satisfies the following isomorphism for all ``R
: Sem``:

.. code-block:: guess

    R ⟶ P ⇒̂ Q ≡ R ×̂ P ⟶ Q

We denote ``_⊢P⇒̂Q`` its action on contexts. Let ``Γ : context``. We
have the following isomorphisms:

.. code-block:: guess

    Γ ⊢P⇒̂Q ≡ ∀ {Δ} → Δ ⊇ Γ → Δ ⊢P⇒̂Q              -- by ψ
           ≡ ⊇[ Γ ] ⟶ P⇒̂Q                        -- by the alternative definition ψ'
           ≡ ⊇[ Γ ] ×̂ P ⟶ Q                      -- by definition of an exponential
           ≡ ∀ {Δ} → Δ ⊇ Γ → Δ ⊢P → Δ ⊢Q         -- by unfolding definition of ×̂, ⟶ and currying

As in the definition of ``Y``, it is easy to see that this last member
can easily be equipped with a renaming: we therefore take it as the
**definition** of the exponential::

    _⇒̂_ : Sem → Sem → Sem
    P ⇒̂ Q = record { _⊢ = λ Γ → ∀ {Δ} → Δ ⊇ Γ → Δ ⊢P → Δ ⊢Q
                   ; ren = λ wk₁ k wk₂ → k (wk₁ ∘wk wk₂) }
      where open Sem P renaming (_⊢ to _⊢P)
            open Sem Q renaming (_⊢ to _⊢Q)

    LAM : ∀ {P Q R} → P ×̂ Q ⟶ R → P ⟶ Q ⇒̂ R
    LAM {P} η p = λ wk q → η (ren-P wk p , q)
      where open Sem P renaming (ren to ren-P)

    APP : ∀ {P Q R} → P ⟶ Q ⇒̂ R → P ⟶ Q → P ⟶ R
    APP η μ = λ px → η px id (μ px)


**Remark:** The above construction of the exponential is taken from
MacLane & Moerdijk's `Sheaves in Geometry and Logic`_ (p.46).

At this stage, we have enough structure to interpret types::

    ⟦_⟧ : type → Sem
    ⟦ unit ⟧  = ⊤̂
    ⟦ S ⇒ T ⟧ = ⟦ S ⟧ ⇒̂ ⟦ T ⟧
    ⟦ A * B ⟧ = ⟦ A ⟧ ×̂ ⟦ B ⟧

To interpret contexts, we need a terminal object::

    ε̂ : Sem
    ε̂ = record { _⊢ = λ _ → ⊤
               ; ren = λ _ _ → tt }

    ⟦_⟧C : (Γ : context) → Sem
    ⟦ ε ⟧C     = ε̂
    ⟦ Γ ▹ T ⟧C = ⟦ Γ ⟧C ×̂ ⟦ T ⟧

As usual, a type in context will be interpreted as a morphism between
their respective interpretations. The interpreter then takes the
syntactic object to its semantical counterpart::

    _⊩_ : context → type → Set
    Γ ⊩ T = ⟦ Γ ⟧C ⟶ ⟦ T ⟧

    lookup : ∀ {Γ T} → T ∈ Γ → Γ ⊩ T
    lookup here (_ , v)      = v
    lookup (there x) (γ , _) = lookup x γ

    eval : ∀{Γ T} → Γ ⊢ T → Γ ⊩ T
    eval {Γ} (lam {S}{T} b)    = LAM {⟦ Γ ⟧C}{⟦ S ⟧}{⟦ T ⟧} (eval b)
    eval (var v)               = lookup v
    eval {Γ}{T} (_!_ {S} f s)  = APP {⟦ Γ ⟧C}{⟦ S ⟧}{⟦ T ⟧} (eval f) (eval s)
    eval {Γ} tt                = TT {⟦ Γ ⟧C}
    eval {Γ} (pair {A}{B} a b) = PAIR {⟦ Γ ⟧C}{⟦ A ⟧}{⟦ B ⟧} (eval a) (eval b)
    eval {Γ} (fst {A}{B} p)    = FST {⟦ Γ ⟧C}{⟦ A ⟧}{⟦ B ⟧} (eval p)
    eval {Γ} (snd {A}{B} p)    = SND {⟦ Γ ⟧C}{⟦ A ⟧}{⟦ B ⟧} (eval p)

Reify and reflect are defined at a given syntactic context, we
therefore introduce suitable notations::

    [_]⊩_ : context → type → Set
    [ Γ ]⊩ T = Γ ⊢⟦T⟧
      where open Sem ⟦ T ⟧ renaming (_⊢ to _⊢⟦T⟧)

    [_]⊩C_ : context → context → Set
    [ Γ ]⊩C Δ = Γ ⊢⟦Δ⟧C
      where open Sem ⟦ Δ ⟧C renaming (_⊢ to _⊢⟦Δ⟧C)

The sea has sufficiently risen: we can implement our initial plan,
using the renaming operator ``ren`` equipping ``Sem`` in the function
case in ``reify``::

    reify : ∀ {T Γ} → [ Γ ]⊩ T  → Γ ⊢Nf T
    reflect : ∀ {Γ} → (T : type) → Γ ⊢Ne T → [ Γ ]⊩ T

    reify {unit} v        = v
    reify {A * B} (a , b) = pair (reify a) (reify b)
    reify {S ⇒ T} f       = lam (reify (app {S}{T} (ren (weak1 id) f) (reflect S (var here))))
      where open Sem ⟦ S ⇒ T ⟧

            app : ∀{S T Γ} → [ Γ ]⊩ (S ⇒ T) → [ Γ ]⊩ S → [ Γ ]⊩ T
            app f s = f id s

    reflect unit v    = ground v
    reflect (A * B) v = reflect A (fst v) , reflect B (snd v)
    reflect (S ⇒ T) v = λ w s → reflect T (ren w v ! reify s)
      where open Sem (Nê (S ⇒ T))


We generalize ``reify`` to work on any "term in an environement",
using the identity context, from which we obtain the normalization
function::

    reify-id : ∀{Γ T} → Γ ⊩ T → Γ ⊢Nf T
    reify-id {Γ}{T} f = reify (f (idC Γ))
      where open Sem

            idC : ∀ Γ → [ Γ ]⊩C Γ
            idC ε       = tt
            idC (Γ ▹ T) = ren ⟦ Γ ⟧C (weak1 id) (idC Γ) , reflect T (var here)


    norm : ∀{Γ T} → Γ ⊢ T → Γ ⊢Nf T
    norm = reify-id ∘ eval

**Remark:** For pedagogical reasons, we have defined ``reify {S ⇒ T}
f`` using function application and weakening, without explicitly using
the structure of ``f : [ Γ ]⊩ S ⇒̂ T``. However, there is also a direct
implementation::

    remark-reify-fun : ∀ {Γ S T} → (f : [ Γ ]⊩ (S ⇒ T)) →
        reify {S ⇒ T} f ≡ lam (reify (f (weak1 id) (reflect S (var here))))
    remark-reify-fun f = refl



By defining a richly-structured model, we have seen how we could
implement a typed model of the λ-calculus and manipulate binders in
the model.

Takeaways:
  * You are *familiar* with the construction of denotational models in type theory
  * You are *able* to define an inductive family that captures exactly some structural invariant
  * You are *able* to write a dependently-typed program
  * You are *familiar* with normalization-by-evaluation proofs for the simply-typed calculus

**Exercises (difficulty: open ended):**

  #. Integrate the results from last week with this week's model of
     the λ-calculus so as to quotient this extended calculus. Hint:
     have a look at `Normalization by evaluation and algebraic
     effects`_

  #. The models we have constructed combine a semantical aspect (in
     Agda) and a syntactic aspect (judgments ``_⊢Nf_``). This has been
     extensively studied under the name of "glueing". We took this
     construction as granted here.

  #. Prove the correctness of the normalisation function ``norm``. The
     categorical semantics (described in the next section) provides
     the blueprint of the necessary proofs.

-------------------------------------
Optional: Categorical spotting
-------------------------------------

..
  ::

  module Cats where

    open STLC
    open NBE-Presheaf

    postulate
      ext : Extensionality zeroℓ zeroℓ
      ext-impl : {X : Set}{Y : X → Set}
          → {f g : {x : X} → Y x}
          → ((x : X) → f {x} ≡ g {x})
          → (λ {x} → f {x}) ≡ g

We have been using various categorical concepts in this lecture. For
the sake of completeness, we (partially) formalize these notions in
Agda with extensional equality.

**Remark:** The point of this exercise is **certainly not** to define
category theory in type theory: this would be, in my opinion, a
pointless exercise (from a pedagogical standpoint, anyway). Rather, we
merely use the syntactic nature of type theory and our computational
intuition for it to provide a glimpse of some categorical objects
(which are much richer than what we could imperfectly model here!).

First, we model the notion of category::

    record Cat : Set where
     field
        Obj : Set
        Hom[_∶_] : Obj → Obj → Set
        idC : ∀ {X} → Hom[ X ∶ X ]
        _∘C_ : ∀ {X Y Z} → Hom[ Y ∶ Z ] → Hom[ X ∶ Y ] → Hom[ X ∶ Z ]

    record IsCat (C : Cat) : Set where
      open Cat C
      field
        left-id : ∀ {A B} → ∀ (f : Hom[ A ∶ B ]) →
                  idC ∘C f ≡ f
        right-id : ∀ {A B} → ∀ (f : Hom[ A ∶ B ]) →
                   f ∘C idC ≡ f
        assoc : ∀ {A B C D} → ∀ (f : Hom[ A ∶ B ])(g : Hom[ B ∶ C ])(h : Hom[ C ∶ D ]) →
                (h ∘C g) ∘C f ≡ h ∘C (g ∘C f)

Contexts form a category, hence the emphasis we have put on defining
composition of weakenings::

    Context-Cat : Cat
    Context-Cat = record { Obj = context ;
                           Hom[_∶_] = _⊇_ ;
                           idC = id ;
                           _∘C_ = _∘wk_ }

Our model of semantics objects is actually an instance of a more
general object, called a "presheaf", and defined over any category as
the class of functors from the opposite category of ``C`` to ``Set``::

    record PSh (C : Cat) : Set₁ where
      open Cat C
      field
        _⊢ : Obj → Set
        ren : ∀ {X Y} → Hom[ X ∶ Y ] → Y ⊢ → X ⊢

    record IsPSh {C : Cat}(P : PSh C) : Set where
      open Cat C
      open PSh P
      field
        ren-id : ∀ {X} → ren (idC {X}) ≡ λ x → x
        ren-∘ : ∀ {X Y Z x} → (g : Hom[ Y ∶ Z ])(f : Hom[ X ∶ Y ]) →
                 ren (g ∘C f) x ≡ ren f (ren g x)

A presheaf itself is a category, whose morphisms are natural
transformations::

    Hom[_][_∶_] : ∀ (C : Cat)(P : PSh C)(Q : PSh C) → Set
    Hom[ C ][ P ∶ Q ] = ∀ {Γ} → Γ ⊢P → Γ ⊢Q
      where open PSh P renaming (_⊢ to _⊢P)
            open PSh Q renaming (_⊢ to _⊢Q)
            open Cat C

    record IsPShHom {C P Q}(η : Hom[ C ][ P ∶ Q ]) : Set where
      open Cat C
      open PSh P renaming (_⊢ to _⊢P ; ren to ren-P)
      open PSh Q renaming (_⊢ to _⊢Q ; ren to ren-Q)
      field
        naturality : ∀ {Γ Δ}(f : Hom[ Γ ∶ Δ ])(x : Δ ⊢P) →
                     η (ren-P f x) ≡ ren-Q f (η x)

    PSh-Cat : Cat → Cat
    PSh-Cat C = record { Obj = PSh C
                       ; Hom[_∶_] = λ P Q → Hom[ C ][ P ∶ Q ]
                       ; idC = λ x → x
                       ; _∘C_ = λ f g x → f (g x) }

    PSh-IsCat : (C : Cat) → IsCat (PSh-Cat C)
    PSh-IsCat C = record { left-id = λ f → refl
                         ; right-id = λ f → refl
                         ; assoc = λ f g h → refl }

**Remark:** We have been slightly cavalier in the definition of
``PSh-Cat``: we ought to make sure that the objects in ``Obj`` do
indeed satisfy ``IsPSh`` whereas the morphisms in ``Hom[_∶_]`` do
indeed satisfy ``IsPShHom``. However, these are not necessary to prove
that presheaves form a category so we eluded them here, for
simplicity.

Our definition of ``Sem`` thus amounts to ``PSh[context]``::

    PSh[context] = PSh Context-Cat

The ``Y`` operator is a general construction, called the Yoneda
lemma. Given any *function* ``F : context → Set``, the Yoneda
embedding gives us the ability to produce a presheaf from **any**
function::

    Yoneda : (F : context → Set) → PSh[context]
    Yoneda F = record { _⊢ = λ Γ → ∀ {Δ} → Hom[ Δ ∶ Γ ] → F Δ
                      ; ren = λ wk₁ k wk₂ → k (wk₁ ∘wk wk₂) }
           where open Cat Context-Cat

    Yoneda-IsPSh : {F : context → Set} → IsPSh (Yoneda F)
    Yoneda-IsPSh = record { ren-id = λ {X} → ext λ ρ →
                                             ext-impl (λ Γ →
                                             ext λ wk →
                                             cong (ρ {Γ}) (lemma-left-unit wk))
                          ; ren-∘ = λ {Δ}{∇}{Ω}{k} wk₁ wk₂ →
                                             ext-impl λ Γ →
                                             ext λ wk₃ →
                                             cong k (lemma-assoc wk₃ wk₂ wk₁) }

A precise treatment of the categorical aspects of
normalization-by-evaluation for the λ-calculus can be found in the
excellent `Normalization and the Yoneda embedding`_ or, in a different
style, in `Semantics Analysis of Normalisation by Evaluation for Typed
Lambda Calculus`_.


.. References (papers):
.. _`The Proof Assistant as an Integrated Development Environment`: https://doi.org/10.1007/978-3-319-03542-0_22
.. _`Cayenne`: https://doi.org/10.1145/291251.289451
.. _`A type-correct, stack-safe, provably correct, expression compiler`: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.105.4086
.. _`Advice on structuring compilers and proving them correct`: https://doi.org/10.1145/512927.512941
.. _`More on advice on structuring compilers and proving them correct`: https://doi.org/10.1016/0304-3975(81)90080-3
.. _`Strongly Typed Term Representations in Coq`: https://doi.org/10.1007/s10817-011-9219-0
.. _`Formalized metatheory with terms represented by an indexed family of types`: https://doi.org/10.1007/11617990_1
.. _`Normalization by evaluation and algebraic effects`: http://doi.org/10.1016/j.entcs.2013.09.007
.. _`Normalization and the Yoneda embedding`: http://doi.org/10.1017/S0960129597002508
.. _`Semantics Analysis of Normalisation by Evaluation for Typed Lambda Calculus`: http://doi.org/10.1145/571157.571161
.. _`About Models for Intuitionistic Type Theories and the Notion of Definitional Equality`: https://doi.org/10.1016/S0049-237X(08)70727-4
.. _`Intuitionistic Model Constructions and Normalization Proofs`: http://doi.org/10.1017/S0960129596002150
.. _`Categorical Reconstruction of a Reduction-free Normalization Proof`: http://doi.org/10.1007/3-540-60164-3_27
.. _`Normalization and Partial Evaluation`: https://doi.org/10.1007/3-540-45699-6_4
.. _`Sheaves in Geometry and Logic`: 10.1007/978-1-4612-0927-0

.. Local Variables:
.. mode: agda2
.. End: