Plugin Architecture - lrytz/efftp GitHub Wiki

This page explains the main ideas in the architecture of the compiler plugin.

Effect Domains

Every effect domain is a subclass of EffectDomain and defines:

• A representation for effects in the domain
• The lattice operations on those effects
• Methods to translate between the effect representation and the corresponding effect annotations
• Optionally a method computing the effect for specific abstract syntax trees (e.g. try / catch trees in the case of exceptions)

If multiple effect domains are being checked, their domain definitions are combined when the plugin is created using the class BiEffectDomain.

Type Constraints

Effect annotations extend from TypeConstraint. This ensures that effect annotations in types are not erased by type maps such as asSeenFrom:

class C {
  val f1: (A => B) { def apply(a: A): B @pure } = .....
  val f2 = this.f1
}

The type of f2 has effect annotations only because they extend TypeConstraint, other annotations are removed in the asSeenFrom type transformation.

Annotation Checker

The effects plugin registers an annotation checker, defined in class TypeCheckerPlugin, which is invoked on subtype tests when at least one of the two types has an annotation.

The annotation checker is not used to check the latent effect of methods (explained below). It is only used to check subtyping of refinement types that have effect annotations. The following produces a type error due to the annotation checker:

val f: { def f: Unit @pure } = new { def f = { println() } }

The annotation checker also drives inference of refined types (again through subtyping tests issued by the compiler). In the following example, value c has a refined type C { def f: Int @pure }:

trait C { def f: Int }
val c = new C { def f = 10 }

Analyzer Plugin

The main component of the plugin is an analyzer plugin, defined in class TypeCheckerPlugin.

Effect checking for method bodies is performed in the method pluginsTyped which is invoked by the Scala type checker after type checking each tree. If the tree is a method definition, then the effect of the method body is computed and compared against the effect annotations on the methods return type.

Effect inference for method bodies is handled in the method pluginsTypeSig. This method is called whenever the compiler first assigns a type to a symbol (i.e. when the lazy type of a symbol gets completed). For method symbols, if the type of the method was inferred (not annotated), the plugin will also infer the effect of the method body.

Anonymous functions get a special treatment in pluginsTyped: the compiler always assigns a FunctionN type to anonymous function trees (Function(params, body)). The effects plugin assigns a more precise type to those anonymous functions which includes the inferred effect of the function body. This effect is added in the form of a type refinement, for instance (A => B) { def apply(a: A): B @pure }.

Most of the other code in the file TypeCheckerPlugin is necessary to correctly handle constructor effects.

Removing effect annotations from terms

Effect annotations only have a meaning if they appear on the return type of a method (with a few exceptions for constructors, default arguments, effect ascriptions).

However, because the plugin uses an annotation checker (see above), effect annotations on terms are not simply ignored: the annotation checker is invoked on every subtype test where one of the two types has some annotations.

Combined with the fact that effect annotations are type constraints (see above), this leads to misleading propagation of effect annotations:

def f(): Int @pure = 1
def g() = {
  println()
  f()
}

In this example, the Scala compiler assigns the type Int @pure to the method invocation f(). Since this is the last statement in the block, this type would be assigned as return type of method g, which is clearly wrong - method g is not pure.

A similar problem occurs when the expected type has effect annotations:

val i: Int = 1
def f(): Int @pure = i

When type checking the body of method f, the Scala compiler uses Int @pure as the expected effect. It will check if the the type of the body, Int, is a subtype of the expected type. This type check will fail (due to the annotation checker) and lead to a spurious type mismatch error.

These two problems are overcome by removing effect annotations from terms and expected types:

• In pluginsTyped which is called after every tree that is type checked, we remove all effect annotations from the inferred type. This addresses the first example.
• The method pluginsPt is called by the type checker before type checking a tree and allows modifying the expected type. The effects plugin removes all effect annotations from the expected type before type checking any tree. This addresses the second example.

Open Issues

There are still some unresolved issues related to the fact that the compiler propagates effect annotations to undesired places:

• #3
• #1