Created
March 2, 2023 00:01
-
-
Save rebcabin/da729315bd3f6b2290c5c598de6300bc to your computer and use it in GitHub Desktop.
Notes on Chapter 8 of "The Little Typer"
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
;; ___ _ _ ___ | |
;; / __| |_ __ _ _ __| |_ ___ _ _ ( _ ) | |
;; | (__| ' \/ _` | '_ \ _/ -_) '_| / _ \ | |
;; \___|_||_\__,_| .__/\__\___|_| \___/ | |
;; |_| | |
;; This is a challenging chapter because it's not | |
;; clear at the start where it's going. I figured it | |
;; out by reading it and writing about it several | |
;; times, and the notes below are my current | |
;; iteration. | |
;; We'll prove that `(+ 1)` _equals_ `add1`, and | |
;; then that `incr` _equals_ `add1`. `Equals`, here, | |
;; is not the same as "the same as," which we | |
;; already know about from judgments: | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; T h e F o u r F o r m s | |
;; o f J u d g m e n t | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; 1. ____ is a ____. | |
;; | |
;; 2. ____ is the same ____ as ____. | |
;; | |
;; 3. ____ is a type [as opposed to an instance] | |
;; | |
;; 4. ____ and ____ are the same type. | |
;; Judgments are for humans; formal statements and | |
;; proofs of statements are for computers. "Formal" | |
;; means "machine-checkable." We write a formal | |
;; statement as a `claim` and a formal proof as a | |
;; `define`, that is, by exhibiting an instance or | |
;; witness of the claim. Claims, implicitly, are | |
;; statements that something exists, so showing an | |
;; instance is a good proof of a claim like that. | |
;; To say formally what we mean by `equals`, we | |
;; introduce a type constructor, `=`, its companion | |
;; value constructor `same`, and some eliminators | |
;; for `=`. See [the | |
;; documentation](https://docs.racket-lang.org/pie/#%28part._.Equality%29) | |
;; for more. | |
;; The first claim and proof of equality will look | |
;; like this: | |
;; (claim +1=add1 | |
;; (Π ((n Nat)) ; Read: for every Nat n, | |
;; (= Nat (+ 1 n) (add1 n)))) ; ... | |
;; (define +1=add1 ; Proof by constructing | |
;; (λ (n) (same (add1 n)))) ; a "same" value for it. | |
;; We'll work up to a proof that `incr` equals | |
;; `add1`. We'll define `incr` as we go along. | |
;; Bottoming out in `add1` is a good idea because | |
;; it's a built-in. | |
;; We'll use "same as" judgments as human | |
;; motivations along the way. Remember that two | |
;; expressions are the same, according to some type, | |
;; if and only if (iff) their normal forms are | |
;; identical, up to consistent renaming of their | |
;; variables. | |
;; We now have three similar notions in the air: (1) | |
;; "identical," which is machine checkable, even | |
;; with consistent renaming of variables [footnote]; | |
;; (2) "same," which we check by judgments and which | |
;; sometimes means "identical," so can be checked by | |
;; machine; and (3) "equals," which we are going to | |
;; show now, but solves problems that checking for | |
;; identical normal forms cannot solve. | |
;; footnote:: Checking that two expressions are | |
;; identical up to consistent renaming is | |
;; surprisingly tricky, and the greats have | |
;; published mistakes about it. See [de Bruijn | |
;; Index](https://en.wikipedia.org/wiki/De_Bruijn_index). | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; P r o v i n g t h a t + 1 E q u a l s a d d 1 | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; We start by showing that the normal forms of | |
;; `(+ 1)` and `add1` are identical (up to | |
;; consistent renaming of variables). That means | |
;; they're "the same." Then we'll write that fact up | |
;; via `=` and `same`, showing that they're `equal`. | |
;; The later proof that `incr` equals `add1` | |
;; requires new eliminators for `=`, namely `cong` | |
;; and `replace`, because the normal forms for these | |
;; two are not identical (up to consistent renaming | |
;; of variables). | |
;; Start with the normal form of `(+ 1)`, which is | |
;; partial application of `+` to `1`: | |
;; Recall the definition of `+`: | |
;; (define + | |
;; (λ (n j) ;; Don't use the name n-1 here. | |
;; ;; target base step ; the pattern | |
;; ;; |------|----|-------| | |
;; (iter-Nat n j step-+ ))) | |
;; where `(define step-+ (λ (n-1) (add1 n-1)))` | |
;; bottoms out at the built-in `add1`. | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; N o r m a l F o r m o f ( + 1 ) | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; Calculate the normal form of `(+ 1)`: | |
;; (+ 1) | |
;; (+ (add1 zero)) destructuring | |
;; (λ (j) | |
;; (iter-Nat (add1 zero) j step-+)) subst. def | |
;; (λ (j) -----v----- | |
;; (step-+ _^__ | |
;; (iter-Nat zero j step-+)) elimination | |
;; (λ (j) | |
;; (add1 ,------- n-1 -------. subst. def of step-+ | |
;; (iter-Nat zero j step-+))) | |
;; / | |
;; ---- | |
;; / | |
;; (λ (j) (add1 j)) elimination | |
;; That's the normal form of `(+ 1)`. Remember or | |
;; bookmark it. | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; N o r m a l F o r m o f a d d 1 | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; The normal form of `(+ 1) is identical to the | |
;; normal form of `add1` if we wrap `add1` in a | |
;; minimal function, and we must. The Pie REPL | |
;; reveals that a naked `add1` doesn't have a normal | |
;; form: | |
;; add1 ; <-- REPL input ~~> REPL response --> | |
; ../playground.pie:11:0: add1: expected valid Pie name | |
; at: add1 | |
; in: add1 | |
;; But the wrapped `add1` is fine (with a type hint) | |
;; and is already in normal form -- the Pie REPL | |
;; can't reduce it any more: | |
;; (the (→ Nat Nat) (λ (n) (add1 n))) ; input to REPL | |
; (the (→ Nat ; response from REPL | |
; Nat) | |
; (λ (n) | |
; (add1 n))) | |
;; If `add1` were a function, we could use the Final | |
;; Law of Application (Page 139, Fifth Printing), or | |
;; even the Initial Law of Application (Page 38, | |
;; Fifth Printing) to show that `add1` is "the same" | |
;; as `(λ (n) (add1 n))`. | |
;; This pattern of wrapping `add1` is exactly like | |
;; the common need to wrap macros with functions in | |
;; C and Lisp. We must often do that so we can pass | |
;; around the functions as values. Macros are not | |
;; values, but functions _are_ values because they | |
;; have the constructor λ up top; that's the | |
;; definition of a value -- it has a constructor up | |
;; top. | |
;; Let's call it a day: `(λ (n) (add1 n))` _is_ "the | |
;; normal form of `add1`". The easiest way to write | |
;; something that the REPL reduces to the normal | |
;; form is `(+ 1)`. You can't present a naked `add1` | |
;; to the REPL. | |
;; We've now shown that `(+ 1)` and `add1` have | |
;; identical normal forms (up to renaming), so | |
;; they're "the same" by Big Box on Page 13. That | |
;; doesn't mean they're `equal`. So let's write | |
;; `equal` as a statement -- a `claim` or a type -- | |
;; and its proof as a `define`. | |
;; Frame 8.23, Page 177 (Fifth Printing): | |
;; Here is a type that _states_ the equality of | |
;; `(+ 1 n)` and `(add1 n)`. The statement boils | |
;; down to stating that the normal forms are | |
;; identical, hence the same. That's not a proof of | |
;; equality, but a precise statement of it. We'll | |
;; need a witness, conveniently packaged in a | |
;; `define`. | |
(Π ((n Nat)) ; input to REPL | |
(= Nat (+ 1 n) (add1 n))) | |
; (the U ; response from REPL | |
; (Π ((n Nat)) | |
; (= Nat | |
; (add1 n) | |
; (add1 n)))) | |
;; The REPL converged the normal forms to | |
;; `(add1 n)`! They're "the same" by construction. | |
;; So we can write the formal proof of the equality | |
;; statement by defining something that constructs a | |
;; value by the sole constructor for =, namely | |
;; _same_. | |
;; ----------------------------------------------- | |
(claim +1=add1 | |
(Π ((n Nat)) ; For every Nat, n, ... | |
(= Nat (+ 1 n) (add1 n)))) | |
(define +1=add1 | |
(λ (n) (same (add1 n)))) | |
;; Really, just the fact that the definition | |
;; satisfies the claim _is_ the proof! Here is the | |
;; whole magillah without `claim` or `define`, just | |
;; a type and a witness, with the type streamlined a | |
;; bit ("defines are never necessary!" Page 58, | |
;; Fifth Printing). | |
(the (Π ((n Nat)) ; input to REPL | |
(= Nat (+ 1 n) (add1 n))) | |
(λ (n) (same (add1 n)))) | |
; (the (Π ((n Nat)) ; response from REPL | |
; (= Nat | |
; (add1 n) | |
; (add1 n))) | |
; (λ (n) | |
; (same (add1 n)))) | |
;; -+-+-+-+-+-+-+-+-+-+-+-+- | |
;; T h e L a w o f = | |
;; -+-+-+-+-+-+-+-+-+-+-+-+- | |
;; Page 174 (Fifth Printing): "An expression | |
;; | |
;; (= X from to) | |
;; | |
;; is a type if X is a type, _from_ is an X, and | |
;; _to_ is an X." | |
;; When discussing an = type expression, call the | |
;; second argument the FROM of the expression and | |
;; the third argument the TO of the expression, with | |
;; the words FROM and TO in all-caps. | |
;; The FROM and TO might be types or not, but they | |
;; must be of type X. Therefore, an (= ...) is a | |
;; dependent type because it might depend on things | |
;; that might not, themselves, be types. | |
;; Some examples of = types for describing equality | |
;; -- remember, types _describe_ values, but they | |
;; are also propositions in logic that _state_ that | |
;; a value satisfying the type exists. | |
(= Nat (+ 6 7) 13) ; input to REPL | |
; (the U ; response from REPL | |
; (= Nat 13 13)) | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; P r o o f t h a t i n c r E q u a l s a d d 1 | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; Here is `incr`: | |
;; ----------------------------------------------- | |
(claim incr (→ Nat Nat)) | |
(define incr | |
(λ (n) | |
(iter-Nat n ; target | |
1 ; base | |
(+ 1)))) ; step | |
;; The normal forms of `(+ 1)` and `incr` are not | |
;; "the same." We'll show so by showing that their | |
;; normal forms are not identical (up to renaming). | |
;; Check your hand calculation by computing the | |
;; normal forms in the REPL: | |
;; playground.pie> (+ 1) ; input to REPL | |
; (the (→ Nat ; response from REPL | |
; Nat) | |
; (λ (j) | |
; (add1 j))) | |
; | |
;; playground.pie> incr ; input to REPL | |
; (the (→ Nat ; response from REPL | |
; Nat) | |
; (λ (n) | |
; (iter-Nat n | |
; (the Nat 1) | |
; (λ (j) | |
; (add1 j))))) | |
;; I made up the following exercise to express the | |
;; claim -- the statement, the type -- that they're | |
;; equal, though not the same. | |
(Π ((n Nat)) | |
(= Nat (+ 1 n) (incr n))) ; input to REPL | |
; (the U ; response from REPL | |
; (Π ((n Nat)) | |
; (= Nat | |
; (add1 n) | |
; (iter-Nat n | |
; (the Nat 1) | |
; (λ (j) | |
; (add1 j)))))) | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; T h e L a w o f s a m e | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; My edits after incorporating Frame 8.37, Page 179. | |
;; The expression (same e3) is an (= X e1 e2) if e1, | |
;; e2, and e3 are each an X and e1 is the same as e2 | |
;; (identical normal forms). We've seen that (+ 1 n) | |
;; and (add1 n) are the same but (+ 1 n) and | |
;; (incr n) are not the same. | |
;; Writing a formal type-witness proof of sameness | |
;; is called _internalizing_ a sameness judgment. | |
;; Π-expressions are statements of universal | |
;; quantifications, i.e, "for-every," ∀, statements | |
;; (Page 187, Fifth Printing). (→ Y X) is a | |
;; shorthand for (Π ((y Y)) X) when the name of Y's | |
;; instance, y, is not needed in X (Page 138, Fifth | |
;; Printing). | |
;; "By combining Π with =, we can write statements | |
;; that are true for arbitrary Nats, while we could | |
;; only make judgments about particular Nats. Here's | |
;; an example:" | |
;; Here is a commented-out copy of the formal proof | |
;; of +1=add1 above just to remind us. | |
;; ----------------------------------------------- | |
;; (claim +1=add1 | |
;; (Π ((n Nat)) | |
;; (= Nat (+ 1 n) (add1 n)))) | |
;; (define +1=add1 | |
;; (λ (n) (same (add1 n)))) | |
;; ... proves the statement that for every Nat n, (+ | |
;; 1 n) equals (add1 n). Equals, here is via the | |
;; type constructor =. | |
;; But incr=add1 doesn't prove so easily, as noted. | |
;; Here is a statement of the proposition, copied | |
;; from above and attached to a name via `claim`. | |
;; ----------------------------------------------- | |
(claim incr=add1 | |
(Π ((n Nat)) | |
(= Nat (incr n) (add1 n)))) | |
;; This is _harder_ to prove because the normal | |
;; forms of (incr n) and (add1 n) are not identical. | |
;; (define incr=add1 | |
;; (λ (n) | |
;; (same (add1 n)))) ; input to REPL | |
; The expressions ; response from REPL | |
; (iter-Nat n | |
; (the Nat 1) | |
; (λ (j) ; same as (+ 1) | |
; (add1 j))) ; and add1 | |
; and | |
; (add1 n) | |
; are not the same Nat | |
;; The normal form of (incr n) is | |
;; (iter-Nat n 1 (+ 1) (we must add a type hint for | |
;; Pie): | |
(the (→ Nat Nat) (λ (n) (incr n))) ; input to REPL | |
; (the (→ Nat ; response from REPL | |
; Nat) | |
; (λ (n) | |
; (iter-Nat n | |
; (the Nat 1) | |
; (λ (j) ; same as add1 or | |
; (add1 j))))) ; (+ 1 | |
;; __ ___ __ | |
;; ___ ___ __ __/ /________ _/ (_) /___ __ | |
;; / _ \/ -_) // / __/ __/ _ `/ / / __/ // / | |
;; /_//_/\__/\_,_/\__/_/ \_,_/_/_/\__/\_, / | |
;; /___/ | |
;; The book goes on a long discourse about | |
;; neutrality, here, to make needed observations | |
;; about normal forms. | |
;; This normal form of (incr n), | |
;; | |
;; (iter-Nat n 1 (+ 1)) | |
;; | |
;; is neutral, because it's not a value (no | |
;; constructor up top) and it cannot (yet) be | |
;; evaluated because of the variable n. From Page | |
;; 182 (Fifth Edition): | |
;; "Variables that are not defined are neutral. If | |
;; the target of an eliminator expression [like | |
;; iter-Nat] is neutral, then the eliminator | |
;; expression is neutral. _Thus values are not | |
;; neutral_." | |
;; This implication needed [a little | |
;; clarification](https://racket.discourse.group/t/the-little-typer-implicattion-that-values-are-not-neutral/1737) | |
;; for me. The gist is that neutral variables and | |
;; neutrally targeted eliminator expressions are | |
;; _the only_ kinds of neutral expressions. No value | |
;; can be of either kind. `(add1 n)` though | |
;; seemingly neutral, is not a neutral expression by | |
;; a convenient definition, or perhaps because its | |
;; normal form, `(λ (j) (add1 j))`, reported by Pie, | |
;; is a value with a λ constructor up top. | |
;; Now, we're going to do a lot of talking about | |
;; whether neutral expressions are normal. This is | |
;; the most tricky bit of reasoning in the book | |
;; through Chapter 8, but we shall exhibit neutral | |
;; expressions that are not normal because they to | |
;; values and values can never be neutral. | |
;; Frame 2.26, Page 40: "Expressions that are not | |
;; values and cannot yet be evaluated due to a | |
;; variable are called _neutral_." | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; N o r m a l a n d N e u t r a l | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; Frames 8.48-8.49, Page 181 (Fifth Printing): the | |
;; normal form of `(incr n)`, namely | |
;; (iter-Nat n 1 (+ 1)) is neutral because (1) it is | |
;; not a value (no constructor up top) and (2) it | |
;; cannot yet be evaluated due to the variable n. | |
;; This is normal and neutral. | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; N o r m a l b u t N o t N e u t r a l | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; (λ (x) (add1 x)) is not neutral because it's | |
;; already in normal form with the function | |
;; constructor λ up top. This is normal but not | |
;; neutral. | |
(the (→ Nat Nat) (λ (x) (add1 x))) ; input to REPL | |
; (the (→ Nat ; response from REPL | |
; Nat) | |
; (λ (x) | |
; (add1 x))) | |
;; itself; normal but not neutral | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; N e i t h e r N o r m a l n o r N e u t r a l | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
(+ 1) ; ~~> neither neutral nor normal; its normal | |
; form is (the (→ Nat Nat) (λ (x) (add1 x))), as above. | |
;; (+ 1) ; input to REPL | |
; (the (→ Nat ; response from REPL | |
; Nat) | |
; (λ (j) | |
; (add1 j))) | |
;; `(add1 x)` is not neutral by definition, or, if | |
;; you prefer because its normal form | |
;; `(λ (j) (add1 j))` is not neutral because it has | |
;; λ up top. | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; N e u t r a l b u t N o t N o r m a l | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; Page 183 (Fifth Printing): | |
;; the neutral expression (the (→ Nat Nat) f) is | |
;; "the same" as (λ (n) (f n)) (by the Laws of λ) | |
;; when n does not occur in f. (λ (n) (f n)) is not | |
;; neutral because it is a value. So f is reckoned | |
;; "neutral but not normal." | |
;; Page 184, Fifth Printing: Likewise, any neutral | |
;; (Pair A D), p, is not normal because its normal | |
;; form, (cons (car p) (cdr p)) is not neutral. | |
;; -+-+-+-+-+-+-+-+-+-+-+-+- | |
;; B a c k t o W o r k | |
;; -+-+-+-+-+-+-+-+-+-+-+-+- | |
;; Remember our claim: | |
;; (claim incr=add1 | |
;; (Π ((n Nat)) | |
;; (= Nat (incr n) (add1 n)))) | |
;; Let's try | |
;; (define incr=add1 | |
;; (λ (n) (same (iter-Nat n 1 (+ 1))))) ; input to REPL | |
; The expressions ; response from REPL | |
; (add1 n) | |
; and | |
; (iter-Nat n | |
; (the Nat 1) | |
; (λ (j) | |
; (add1 j))) | |
; are not the same Nat | |
;; This fails because the normal form of `(add1 n)`, | |
;; namely `(λ (n) (add1 n))`, is not neutral because | |
;; it's a value, but `(iter-Nat n 1 (+ 1))` is | |
;; neutral even thought it's normal. | |
;; Check it a couple of more ways: | |
;; (check-same (→ Nat Nat) | |
;; (λ (n) (iter-Nat n 1 (+ 1))) | |
;; (λ (n) (add1 n))) | |
; The expressions | |
; (λ (n) | |
; (iter-Nat n | |
; (the Nat 1) | |
; (λ (j) | |
; (add1 j)))) | |
; and | |
; (λ (n) | |
; (add1 n)) | |
; are not the same | |
; (→ Nat | |
; Nat) | |
;; (check-same (→ Nat Nat) | |
;; (λ (n) (iter-Nat n 1 (+ 1))) | |
;; (λ (n) (+ 1 n))) | |
; The expressions | |
; (λ (n) | |
; (iter-Nat n | |
; (the Nat 1) | |
; (λ (j) | |
; (add1 j)))) | |
; and | |
; (λ (n) | |
; (add1 n)) | |
; are not the same | |
; (→ Nat | |
; Nat) | |
;; Socrates, on the left-hand side of every frame, | |
;; says "try ind-Nat." We'll need a target, a base, | |
;; a motive, and a step. | |
;; -+-+-+-+- | |
;; b a s e | |
;; -+-+-+-+- | |
;; Here is a base case that makes an `=` statement | |
;; about `zero`: | |
;; ----------------------------------------------- | |
(claim base-incr=add1 | |
(= Nat (incr 0) (add1 zero))) | |
(define base-incr=add1 | |
(same (add1 zero))) | |
;; -+-+-+-+-+-+- | |
;; m o t i v e | |
;; -+-+-+-+-+-+- | |
;; Here is a motive that makes an `=` statement | |
;; about any Nat: | |
;; ----------------------------------------------- | |
(claim mot-incr=add1 | |
(→ Nat U)) | |
(define mot-incr=add1 | |
(λ (k) | |
(= Nat (incr k) (add1 k)))) | |
;; -+-+-+-+- | |
;; s t e p | |
;; -+-+-+-+- | |
;; The step must move us from an `=` statement about | |
;; Nat k to an `=` statement about `(add1 k)`: | |
;; The following attempt works, but it considered | |
;; not ideal for reasons to-be-revealed: | |
;; (claim step-incr=add1 | |
;; (Π (( n-1 Nat )) | |
;; (→ (mot-incr=add1 n-1) | |
;; (mot-incr=add1 (add1 n-1))))) | |
;; Git rid of the references to the motive: | |
;; (claim step-incr=add1 | |
;; (Π (( n-1 Nat )) | |
;; (→ (= Nat | |
;; (incr n-1) | |
;; (add1 n-1)) | |
;; (= Nat | |
;; (incr (add1 n-1)) | |
;; (add1 (add1 n-1)))))) | |
;; The following claim is considered ideal because | |
;; it pulls the add1 up top in the output of | |
;; step-incr=add1. See Page 188 (Fifth Printing) for | |
;; a lengthy calculation. | |
(claim step-incr=add1 | |
(Π (( n-1 Nat )) | |
(→ (= Nat | |
(incr n-1) | |
(add1 n-1)) | |
(= Nat | |
(add1 (incr n-1)) | |
(add1 (add1 n-1)))))) | |
;; To prove this claim, i.e., to write the | |
;; corresponding `define`, we introduce `cong` | |
;; ("congruent"). `cong` is an eliminator for =. | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; T h e L a w o f c o n g | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; Page 190 (Fifth Printing): If f is an (→ X Y) and | |
;; target is an (= X from to), then then (cong | |
;; target f) is an (= Y (f from) (f to)). | |
;; This looks like [The Yoneda Lemma](https://en.wikipedia.org/wiki/Yoneda_lemma) to my eyes. | |
;; In our example, we must transform | |
;; (= Nat | |
;; (incr n-1) | |
;; (add1 n-1)) | |
;; into | |
;; (= Nat | |
;; (add1 (incr n-1)) | |
;; (add1 (add1 n-1)))) | |
;; by eliminating =: | |
(define step-incr=add1 | |
(λ (n-1) | |
(λ (incr=add_n-1) | |
(cong incr=add_n-1 (+ 1))))) | |
;; We're done: | |
(define incr=add1 | |
(λ (n) | |
(ind-Nat n | |
mot-incr=add1 | |
base-incr=add1 | |
step-incr=add1))) | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; T h e C o m m a n d m e n t o f c o n g | |
;; -+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+-+- | |
;; Page 194 (Fifth Printing): If x is an X and f is | |
;; an (→ X Y), then (cong (same x) f) is the same (= | |
;; Y (f x) (f x)) as (same (f x)) | |
;; Frame 8.89, Page 195 (Fifth Printing): | |
;; Soc: "The interplay between judging sameness and | |
;; stating equality is at the heart of dependent | |
;; types. This taste only scratches the surface." | |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment