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.