Write a Blog >>
Fri 23 Jun 2017 10:55 - 11:20 at Auditorium, Vertex Building - Types and Effects Chair(s): Philipp Haller

Effect systems are lightweight extensions to type systems that can verify a wide range of important properties with modest developer burden. But our general understanding of effect systems is limited primarily to systems where the order of effects is irrelevant. Understanding such systems in terms of a lattice of effects grounds understanding of the essential issues, and provides guidance when designing new effect systems. By contrast, sequential effect systems — where the order of effects is important — lack a clear algebraic characterization.

We derive an algebraic characterization from the shape of prior concrete sequential effect systems. We present an abstract polymorphic effect system with singleton effects parameterized by an effect quantale — an algebraic structure with well-defined properties that can model a range of existing order-sensitive effect systems. We define effect quantales, derive useful properties, and show how they cleanly model a variety of known sequential effect systems. We show that effect quantales provide a free, general notion of iterating a sequential effect, and that for systems we consider the derived iteration agrees with the manually designed iteration operators in prior work. Identifying and applying the right algebraic structure led us to subtle insights into the design of order-sensitive effect systems, which provides guidance on non-obvious points of designing order-sensitive effect systems. Effect quantales have clear relationships to the recent category theoretic work on order-sensitive effect systems, but are explained without recourse to category theory. In addition, some of our derived constructs (iteration) should generalize to these semantic structures, addressing limitations of that work.

Fri 23 Jun
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10: ECOOP Research Papers - Types and Effects at Auditorium, Vertex Building
Chair(s): Philipp HallerKTH Royal Institute of Technology
ecoop-2017-papers10:30 - 10:55
Elias CastegrenUppsala University, Tobias WrigstadUppsala University
Link to publication Media Attached
ecoop-2017-papers10:55 - 11:20
Colin GordonDrexel University
Link to publication Pre-print Media Attached
ecoop-2017-papers11:20 - 11:45
Edlira KuciTU Darmstadt, Germany, Sebastian ErdwegTU Delft, Oliver BračevacTU Darmstadt, Andi BejleriTU Darmstadt, Germany, Mira MeziniTU Darmstadt
Link to publication Media Attached
ecoop-2017-papers11:45 - 12:10
Alceste ScalasImperial College London, Ornela DardhaUniversity of Glasgow, Raymond HuImperial College London, Nobuko YoshidaImperial College London
Link to publication Media Attached