Skip to content
Snippets Groups Projects
Select Git revision
  • main default protected
  • master
2 results
Blame Permalink
critique.org 820 B

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.