examples

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

 * Outline
 ** Intro: What semantics of Gradual Typing is Right?
 *** URGENT Pop Quiz: How does this program run?
-    - x:
-    - ->:
-    - refactoring: lift a pattern match out of a lambda.
+    - (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