write up my gradual type theory talk notes

talk/amal-class-spring-2019/gtt-talk.org

 * Outline
 ** Intro: What semantics of Gradual Typing is Right?
-*** DONE Pop Quiz: How does this program run?
-    - (lambda (f : ? -> ?). true)  3
-      - dynamic typing: evaluates to true
-      - almost every gradual language: error: 3 is not ? -> ?
-      - pi_1 ((lambda (f : ? -> ?). (true, f)) 3)
-      - why? if we just added a rule that said this 
-      - lesson 1: gradual typing introduces errors even when
-        unneccessary for safety theorems to be true
-    - λ p : A_1 x A_2. λ f. f (pi1 p)
-      - (λ p : Int x Bool. λ f. f (pi1 p)) ((3, 4) :: ?)
-      - (λ p : Int x Bool. let y = pi1 p in λ f. f y) ((3, 4) :: ?)
-      - as a general principle, in a typed cbv lang should
-        (λ p. λ f. f(pi1 p) == λ p. let y = pi1 p in λ f. f y)
-      - lesson 2: we should think about how cast insertion affects the
-        safety of our operations
-    - Julia's example: (((λ x:?. x) :: I -> I) :: ?) :: B -> B
-      - should it
-	1. be equivalent to (λ x:B. x)
-	2. be equivalent to (λ x:B. error)
-	3. be equivalent to `error`?
-*** Why do programs error?
-    - Type Safety, Blame safety? neither prevent dropping intermediate
-      casts
-    - Let's be positive: types are there to *help us*, to allow us to
-      refactor, optimize in a modular way
-** Relational Soundness Theorems
-*** Contextual Equivalence + βη-equivalence
-*** Graduality as Contextual Approximation
+*** DONE Pop Quiz
+    Any answer is good if it can be *justified*. Best justifications
+    are *violations of soundness theorems*
+    1. How does (lambda (x : ? * Int). true) (3 :: ?) evaluate?
+       - dynamic typing: evaluates to true
+       - almost every gradual language: error: 3 is not ? -> ?
+       - pi_1 ((lambda (x : ? * Int). (true, x)) 3)
+       - most people answered error, but why? doesn't violate a
+         soundness theorem.
+       - lesson 1: gradual typing introduces errors even when
+         unneccessary for safety theorems to be true
+    2. Are λ p : A_1 x A_2. λ f. let x1,x2 = p in f x1 and
+       λ p : A_1 x A_2. let x1,x2 = p in λ f. f x1 equivalent?
+       - not in transient semantics
+       - equivalent in stlc
+       - not space-equivalent: second one x2 is clearly not in f's
+         closure
+       - we want these to be equivalent so we can make this
+         space-saving optimization
+    3. Julia's example: (((λ x:?. x) :: I -> I) :: ?) :: B -> B
+       - should it
+	 1. be equivalent to (λ x:B. x)
+	 2. be equivalent to (λ x:B. error)
+	 3. be equivalent to `error`?
+       - what about if instead of that middle cast I was wrapping it in
+         a logging function? Loggify(f) = λ x. log(x); f(x)
+       - eager semantics breaks functional reasoning.
+    then I promise I will show soundness theorems that give us an
+    answer to all 3 questions
+** What soundness theorems should we want
+   Gradually typed languages should be
+   1. Typed: satisfy a type soundness theorem
+   2. Gradual: satisfy a graduality theorem.
+*** Contextual Equivalence
+    - define contextual equivalence in the presence of divergence and
+      errors. mention it depends on effects
+    - sound typing means having reasoning principles for contextual
+      equivalence: justify compiler and programmer
+      reasoning/optimization.
+**** Pairs
+     - show intro, elim (pattern match), cbv beta, cbv eta
+     - note that beta is valid in untyped language
+     - eta is the difference between typed and untyped reasoning
+     - note that sums, ints, bools are similar.
+     - show examples 1 should error because eta says we should be able
+       to pattern match and example 2 is equivalent by eta.
+**** Functions
+     - show intro, elim, cbv beta, cbv eta
+     - mention the cbn beta/eta in passing
+     - "there's nothing more to a function than what happens when you
+       apply it"
+     - show that example 3 we should be able to eta expand in the
+       middle, which rules out an error.
+     - caveat: not true in the presence of eq?/object identity, but
+       note that in that case the normal cast semantics isn't valid
+       either!
+*** Graduality
+    - when I add types, my program should still work
+**** Syntactic Type and Term precision
+     - show normal definition of type precision (everything is
+       monotone)
+     - define syntactic term precision as having the same type erasure
+       and the corresponding annotations are <=.
+**** Semantic Term Precision
+     Modify the definition of contextual equivalence to an ordering.
+     - graduality is syntactic term precision => semantic term precision
 ** Gradual Type Theory
-   - Now that we have formulated what we *want* out of gradual
-     languages, we can ask: what are the consequences of the
-     definition? How much design freedom do we really have?
-   - We accomplish this by *axiomatizing* these properties in a type
-     theory we call Gradual Type Theory
-   - The result of this axiomatization is that we can *prove*
-     operational reductions follow from our relational soundness
-     theorems. So most of the semantics is totally determined.
-*** DONE What to present?
-    - Examples
-    - beta-eta as ctx equivalences
-    - graduality as ctx approximation
-    - casts as lubs/glbs
-    - "headline theorem": derive contracts from soundness
+*** Motivation
+    - normally we define our semantics and then prove our soundness
+      theorems.
+    - with GTT we want to take our soundness theorems as given, and
+      *derive* an operational semantics.
+    - how? We show that for (almost) every reduction in the cast
+      semantics t |-> t', we can *justify* it by showing that t and t'
+      must be *contextually equivalent* if our type soundness and
+      graduality theorems hold.
+    - to make that argument precise we *axiomatize* our type soundness
+      and graduality theorems in a type theory with a logic for
+      semantic precision.
+*** Basic Rules
+    - show them the judgmental structure: types, terms, type and term
+      precision, point out the side-conditions on term precision.
+    - say that we add congruence rules (encoding syntactic term
+      precision), and beta-eta.
+    - add in errors and minimality of error rule.
+*** Cast Rules
+    - motivate: casts should be as similar as possible to the original
+    - downcasts
+      - the downcast should be below the original because it may error
+        but blah
+      - but with just that the error would be acceptable: need to make
+        sure it's not too small: make it the largest such thing
+      - glb
+    - upcasts
+      - upcast should be above because its behavior should be related
+      - but we don't want to hide error behaviors with good behavior:
+        make sure it's the smallest such thing
+      - lub
+    - by defining them as glbs and lubs this is defining them
+      precisely.
+*** Cast Uniqueness Principles
+   - just had time to show that we can prove an equivalence between
+     the function cast and a functional implementation of that cast.