Preliminary exam: Yuheng Long
Title: First-class Effect Reflection
Major Professor: Dr. Hridesh Rajan
A type-and-effect system is a very important reasoning aid. It has been shown to help programmers in analyzing locking disciplines, dynamic updating mechanisms, checked exceptions, detecting race conditions, etc. The basic idea behind a type-and-effect system is to add an encoding of computational effects into semantic objects of a language and a discipline for controlling these effects into its type system. These effects describe how the state of a program will be modified by expressions in the language, e.g. a field expression may have a read or write effect to represent reading from or writing into memory.
Traditionally, effect system has been used mainly as pure static program reasoning. For example, it helps the programmers understand the side-effect of evaluating an expression at compile time; it helps the static compilers identify compile-time optimization opportunities, e.g., stack allocation, code motion and concurrent evaluation; it helps programmers specify the constraints and privileges of expressions, etc.
In previous work on static effect reasoning, the compiler, the runtime system or the framework, here onward cumulatively referred to as tools, have access to the computational side effects of program expressions, e.g. as an additional attribute of the abstract syntax tree. These tools then analyze effects to make effect-guided decisions, e.g. running two non-conflicting tasks in parallel. This logic, programmatically processing the side-effects for effect-guided decisions, is typically written by a compiler or a program analysis expert. The end-user programmer is generally a consumer of effect-guided decisions.
Even though effects are not currently available as data to programs, computations (analyses) that use effects have already been used for solving several important problems. My thesis is: could making computational side-effects available as data to programs enable more? In particular, if effects are available as data, program-specific, programmer-specified, effect-guided decisions can now be realized as part of the program itself.
Motivated by this possibility, I will discuss a new language design, where the programmer can query the potential side effects of an expression, which may or may not have been evaluated yet. The results of this query is an effect value, i.e. computational effects are first-class citizens in this programming model. To do meaningful program reasonings, programmers can then write mathematical formulas with effect, union, intersection, minus and subset to name a few. We show that it is very challenging to enable a wide range of mathematical formulas using the traditional effect representation. The problem is that the traditional effect representation is opaque, abstract and conservative. To deal with this problem, we provide a flexible effect system, called first class effect, which provides highly precise effect reasonings by dynamic typing. In first class effect, the effect representation is more transparent and encodes more type-and-effect information useful for a wide range of mathematical operations on effect reasonings. I also discuss my work on intensional effect polymorphism, which makes dynamic typing more precise, and related ideas.