Notes on Chapter 8 of "The Little Typer"

playground.pie

;;   ___ _              _             ___
;;  / __| |_  __ _ _ __| |_ ___ _ _  ( _ )
;; | (__| ' \/ _` | '_ \  _/ -_) '_| / _ \
;;  \___|_||_\__,_| .__/\__\___|_|   \___/
;;                |_|


;; 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."