From 7edc94a2f846c4fa2bfef7cad870c33a971d98d8 Mon Sep 17 00:00:00 2001 From: Max New <maxsnew@gmail.com> Date: Thu, 4 Apr 2019 10:47:13 -0400 Subject: [PATCH] write up my gradual type theory talk notes --- talk/amal-class-spring-2019/gtt-talk.org | 144 ++++++++++++++++------- 1 file changed, 102 insertions(+), 42 deletions(-) diff --git a/talk/amal-class-spring-2019/gtt-talk.org b/talk/amal-class-spring-2019/gtt-talk.org index 028c0da..5a50d7a 100644 --- a/talk/amal-class-spring-2019/gtt-talk.org +++ b/talk/amal-class-spring-2019/gtt-talk.org @@ -1,45 +1,105 @@ * 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. -- GitLab