From f22fa8f61d19eb0670ea9adfa28f6e280a8dfa5e Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Fri, 15 Mar 2019 15:33:50 -0400
Subject: [PATCH] examples

---
 talk/amal-class-spring-2019/gtt-talk.org | 22 +++++++++++++++++++---
 1 file changed, 19 insertions(+), 3 deletions(-)

diff --git a/talk/amal-class-spring-2019/gtt-talk.org b/talk/amal-class-spring-2019/gtt-talk.org
index 9bfbb9a..27571d4 100644
--- a/talk/amal-class-spring-2019/gtt-talk.org
+++ b/talk/amal-class-spring-2019/gtt-talk.org
@@ -1,9 +1,25 @@
 * 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
-- 
GitLab