notes on "Exploring the Design Space" and how it relates

critique.org

+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.