Apr 6, 2014
Ronald Garcia: Gradual Effect Systems
Effect systems have the potential to help software developers, but their
? practical adoption as part of language definitions has been very limited.
? We conjecture that this??is due in part to the difficulty of transitioning from a system
? where effects are implicit and unrestricted to a system with a static effect
? discipline, which must settle for conservative checking in order to be
? decidable. ?To address this, we develop a theory of gradual effect
? checking, which makes it possible to incrementally annotate and statically
? check effects, while still rejecting statically effect-inconsistent programs. ?We
? extend the generic type-and-effect framework of Marino and Millstein with a
? notion of unknown effects, which turns out to be significantly more subtle
? than unknown types in traditional gradual typing.
This is joint work with Felipe Bañados Schwerter and Éric Tanter