From 31b540ec97a077eb5670aae1fe94e2a0f55623f9 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Mon, 2 Apr 2018 16:44:31 -0400
Subject: [PATCH] notes on "Exploring the Design Space" and how it relates

---
 critique.org | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)
 create mode 100644 critique.org

diff --git a/critique.org b/critique.org
new file mode 100644
index 0000000..5954266
--- /dev/null
+++ b/critique.org
@@ -0,0 +1,20 @@
+The related work in this paper is more important than in the last
+because it's actual call-by-value stuff.
+
+There is a difficulty though. Our result here is graduality + eta +
+function casts are pure => wrapping function casts.
+
+Exploring the Design Space of Higher-Order Casts (Siek-Garcia-Taha)
+does a bit of a survey. What is wrong (or right) with it from our
+perspective?
+
+1. The eager semantics is not extensional.
+   The cast where (B = bool, I = int, D = dyn)
+
+   <B -> I <= D -> D><D -> D <= I -> I>(lambda x. t) |-> err
+   but if we eta-expand the inside, it is a value(!)
+   <B -> I <= D -> D>(lambda y. (<D -> D <= I -> I>(lambda x. t) y)
+
+2. The downcast semantics is not *compositional* in that
+   upcasts/downcasts A -> B -> C do not factorize. Does it actually
+   violate the gradual guarantee? Doubtful.
-- 
GitLab