lrytz / efftp Goto Github PK

View Code? Open in Web Editor NEW

83.0 83.0 5.0 3.19 MB

Scala 72.15% Java 27.85%

efftp's People

Contributors

Stargazers

Watchers

Forkers

xeno-by janduracz amirsh martinring

efftp's Issues

relative effects in result type are not yet substituted

  def foo(f: Int => Int) = new {
    def bar(x: Int): Int @pure(f.apply(%)) = f(x)
  }

  // not yet supported.. has top effect
  def t2: Any @pure = foo(x => x).bar(10)

Purity Domain fails in REPL

scala> lamppc11:scala-2.10 luc$ ~/scala/scala-2.10.1/bin/scala -cp effects-plugin_2.10-0.1-SNAPSHOT.jar -Xplugin:effects-plugin_2.10-0.1-SNAPSHOT.jar -P:effects:domains:purity
Welcome to Scala version 2.10.1 (Java HotSpot(TM) 64-Bit Server VM, Java 1.6.0_45).

scala> 1
<console>:5: error: effect type mismatch;
 found   : @mod($eval.this) @loc(any)
 required: @mod() @loc(any)
@mod($eval.this) does not conform to @mod()
  lazy val $result = `res0`
           ^

local fields can alias each other

MutableList.scala has two local fields which alias each other, similar to the following:

  class Counter {
    private var x = 0
    def inc(): Int @pure @mod(this) = { x += 1; x }
  }

  class MUHA {
    @local var firstC = new Counter
    @local var lastC = firstC

    def f(): Counter @loc(this) = {
      lastC
    }
  }

the above should work. the below should not:

  class MUHA {
    var firstC = new Counter  // non-local
    @local var lastC = firstC  // should fail

    def f(): Counter @loc(this) = {
      lastC
    }
  }

Effect Annotations propagate incorrectly when the plugin is disabled

class C { def m(): Int @pure = 1 }
def makeC: C @io = { println("In Factory"); new C }
def test = makeC.m()

When the effects plugin is not enabled, method test gets type Int @pure - bad.

implicit search influenced by effect annotations

class C

trait A {
  implicit val cOne: C
}

abstract class B(implicit cTwo: C) extends A {
  def foo = implicitly[C]
}

Without the plugin, the compiler picks cTwo. It's more specific than cOne because it's defined in a subclass.

When enabling the plugin the two implicits become ambiguous. The reason is that cOne is a reference to the getter function, which has a method type and an effect annotation. cTwo does not have a getter, so it's a direct reference to the field, and has no effect annotation:

[search] scala.this.Predef.implicitly[C] with pt=C in class B, eligible:
  cTwo: C
  cOne: => C @scala.annotation.effects.noIo

Implicit search will verify if cTwo improves over cOne, which is no longer the case. The problem is that C is not a subtype of C @noIo due to the annotation checker (which picks the top effect @io as default if there are no effect annotations).

Workaround: make cTwo a val parameter, then the implicit search will use the getter symbol which has a method type, and an effect annotation.

Fix: One way is to have a analyzer plugin hook in Implicits.improves, which invokes isStrictlyMoreSpecific. Then the plugin could remove the effect annotations from the types.

Pending test in https://github.com/lrytz/efftp/blob/master/tests/src/test/resources/scala/tools/nsc/effects/io/ClassesSuite-files/implicitsPending.scala

Change Syntax for effect casts

Currently, simple ascriptions are interpreted as effect casts:

  println(): @noIo

This is inconsistent with the behavior for normal types, where ascription triggers a type check. Also there is no way to trigger an effect check at a specific location, which would often be useful.

So we will change this:

Simple ascription will trigger an effect check, so println(): @noIo will trigger an error message
Effect casts will require an additional @unchecked annnotation, i.e. @println() @unchecked @noIo is an effect cast

Distinguish between checked and unchecked exceptions

Similar to what Java does (only subclasses of Exception are checked, but not subclasses of RuntimeException).

Mask @mod(this) for constructors

Constructors (almost) always have a @mod(this) effect, but since this is known to be fresh (unless there are some other effects), that could be masked:

@pure class C(x: Int) // does not compile

If there are other effects, the @mod(this) needs to be kept:

class C(@local a: A)

def foo() = {
  vla a = new A
  val c = new C(a) // should have effect @mod(a, c)
}

Lazy Vals get an effect annotation

It's probably a bad idea to put the effect on the lazy val type - it's the only place where a value has an effect annotation, and this is exactly what we try to avoid (in pluginsTyped we remove all effect annotations from terms).

Having effect annotations on values leads to all random interactions with the typer, because terms suddenly have effects, which triggers the annotationChecker.

Alternative to putting the effect on the lazy val type: put it as an attachment in the symbol. That might not work across separate compilation though.

Maybe we can put it inside another annotation which is not a TypeConstraint (@lazyValEffect(...)).

should default arguments be pure by default?

right now, argument types are used as-is for default getters, therefore default getters are impure unless there's an @pure annotation:

def f(x: Int = 1)
def g(x: Int @pure = 1)
f() // has unknown effect
g() // pure

maybe we should treat default getters for argument types without effect annotation to be pure

support underscore in relative effects

recognize anonymous function expressions as relative effects. all of the following should work (hopefully - or is an explicit parameter type required?):

def m(f: Int => Int): Int @pure(f.apply(_)) = f(1)
def m(f: Int => Int): Int @pure(f.apply _) = f(1)
def m(f: Int => Int): Int @pure(x => f.apply(x)) = f(1)

Synthetic code generation leads to effect annotations in terms

Synthetic code (such as the one generated by phase patmat) is not always type checked, but types are directly assigned (e.g. when using gen.mkAttributedRef, I think).

This is problematic because the plugin does not get a chance to strip off effect annotations from terms.

The bug is distilled in https://github.com/lrytz/efftp/blob/master/tests/src/test/resources/scala/tools/nsc/effects/io/PatMatSuite-files/patMatPending.scala

A symptomatic error message:

lucmac:sandbox luc$ ~/scala/scala-2.10.1/bin/scalac -J-agentlib:jdwp=transport=dt_socket,server=y,suspend=n,address=5006 -cp /Users/luc/scala/efftp/target/scala-2.10/effects-plugin_2.10-0.1-SNAPSHOT.jar -Xplugin:/Users/luc/scala/efftp/target/scala-2.10/effects-plugin_2.10-0.1-SNAPSHOT.jar -P:effects:domains:io -d out /Users/luc/scala/scala/src/library/scala/collection/immutable/RedBlack.scala
Listening for transport dt_socket at address: 5006
/Users/luc/scala/scala/src/library/scala/collection/immutable/RedBlack.scala:62: error: error during expansion of this match (this is a scalac bug).
The underlying error was: type arguments [RedBlack.this.RedTree[B1] @scala.annotation.effects.noIo] do not conform to method asInstanceOf's type parameter bounds [T0]
    private[this] def balanceLeft[B1 >: B](isBlack: Boolean, z: A, zv: B, l: Tree[B1], d: Tree[B1])/*: NonEmpty[B1]*/ = l match {
                                                                                                                          ^
/Users/luc/scala/scala/src/library/scala/collection/immutable/RedBlack.scala:70: error: error during expansion of this match (this is a scalac bug).
The underlying error was: type arguments [RedBlack.this.RedTree[B1] @scala.annotation.effects.noIo] do not conform to method asInstanceOf's type parameter bounds [T0]
    private[this] def balanceRight[B1 >: B](isBlack: Boolean, x: A, xv: B, a: Tree[B1], r: Tree[B1])/*: NonEmpty[B1]*/ = r match {
                                                                                                                           ^
two errors found

Spurious error creating anonymous class with mutable field

class E {
  val c = new { var x = 0 }
}

gives

T.scala:47: error: type mismatch;
 found   : AnyRef{def x: Int @scala.annotation.effects.mod @scala.annotation.effects.throws[Nothing] @scala.annotation.effects.noIo; def x_=(x$1: Int): Unit @scala.annotation.effects.mod($anon.this) @scala.annotation.effects.throws[Nothing] @scala.annotation.effects.noIo; var x: Int}
 required: AnyRef{def x: Int @scala.annotation.effects.mod @scala.annotation.effects.throws[Nothing] @scala.annotation.effects.noIo; def x_=(x$1: Int): Unit @scala.annotation.effects.mod($anon.this) @scala.annotation.effects.throws[Nothing] @scala.annotation.effects.noIo}
Type error occured while type checking a tree for effect inference.
  val c = new { var x = 0 }
          ^

Better syntax for effect annotations on Function types

Currently function types have to be effect-annotated using a refined type:

val pureFun: (Int => Int) { def apply(x: Int): Int @pure } = ...

It would be nice to support something as simple as Int => Int @pure.

More precise mismatch error messages for polymorphic method invocations

When invoking an effect-polymorphic method, the resulting effect consists of the latent, absolute effect, plus the effect of the argument.

The error message currently does not distinguish where the effect mismatch originates, so it is hard to find the cause of an effect mismatch sometimes:

  def h(f: Int => Int): Int @rel(f) = f(10)
    def test: Int @pure = {
    val x = 1
    h(x => {
      println()
      x + 1
    })
  }

The error is reported at the invocation of h, not at the println() statement:

T.scala:45: error: effect type mismatch;
 found   : @mod(any) @assign(any) @loc(any)
 required: @mod(x,f$1) @assign(x,any) @assign(f$1,any) @loc(any)
@mod(any) does not conform to @mod(x,f$1)
@assign(any) does not conform to @assign(x,any) @assign(f$1,any)
    h(x => {
     ^

Explicit exception type parameters seem to Just Work - add tests

feels like java :)

scala> import annotation.effects._
import annotation.effects._

scala> class E1 extends Exception
defined class E1

scala> trait Fun[A, B, E <: Exception] { def apply(a: A): B @throws[E] }
defined trait Fun

scala> def foo[E <: Exception](fun: Fun[Int, Int, E]): Int @throws[E] = fun(1)
foo: [E <: Exception](fun: Fun[Int,Int,E])Int @scala.annotation.effects.throws[E]

scala> foo(new Fun[Int, Int, Nothing] { def apply(x: Int) = x })
res1: Int @scala.annotation.effects.throws[Nothing] = 1

scala> foo(new Fun[Int, Int, E1] { def apply(x: Int) = x })
res2: Int @scala.annotation.effects.throws[Nothing] = 1

scala> foo(new Fun[Int, Int, Nothing] { def apply(x: Int) = throw new E1 })
<console>:14: error: overriding method apply in trait Fun of type (a: Int)Int @scala.annotation.effects.throws[Nothing];
 method apply has incompatible type
              foo(new Fun[Int, Int, Nothing] { def apply(x: Int) = throw new E1 })
                                                   ^

this one in fact does not seem to work:

scala> def bar = foo(new Fun[Int, Int, E1] { def apply(x: Int): Int @throws[E1] = x })
bar: Int @scala.annotation.effects.throws[Nothing]

subclass of class with constructorEffect makes the plugin loop

this makes the plugin run in a loop, at least when building in eclipse

class C {
  @pure @mod(this) private[this] type constructorEffect = Nothing
  var x = 0
}
class D extends C

Purity effects and pattern matching: define localities of pattern-bound variables

See for example this test:

def f1(a: Any): C @loc(a) = a match {
  case c: C => c
}

fails with

 found   : @mod() @loc(c)
 required: @mod() @loc(a)

Changes to Scala syntax for better effect syntax

Three syntax changes we'd like to push to Scala:

Allow return type (and therefore effect) on constructors

class C(x: Int): C @pure extends D {
}

Same thing for auxiliary constructors

class C extends D {
  def this(x: Int): C @pure = { ... }
}

Allow result type annotations without result type (meaning: infer type, but check effect)

def foo(x: Int): @pure = x + 1

The first two will eliminate the special cases for constructor effect annotations.

Effect annotations print with fully qualified name

It would be nice to omit the ubiquitous scala.annotation.effects:

tsf-444-wpa-2-149:scala-2.10 luc$ ~/scala/scala-2.10.1/bin/scala -cp effects-plugin_2.10-0.1-SNAPSHOT.jar -Xplugin:effects-plugin_2.10-0.1-SNAPSHOT.jar -P:effects:domains:io

Welcome to Scala version 2.10.1 (Java HotSpot(TM) 64-Bit Server VM, Java 1.6.0_45).
Type in expressions to have them evaluated.
Type :help for more information.

scala> def f: Int @io = 1
f: Int @scala.annotation.effects.io

Can This Plugin be Maintained?

This is a great plugin can this be maintained?

Blend @pure and @rel together

Martin suggested to unify @rel and @pure. The simple @pure annotation would keep its meaning, while @pure(f.m()) would describe a relative effect.

In fact, this amounts to removing the current @pure annotation and renaming @rel to @pure. Already now, having an @rel annotation implies purity, and therefore, already now, @rel is equivalent to @pure.

Support external annotations for existing (and Java) libraries

We need a way to get effect annotations for existing libraries.

The checker framework uses stub files, Java source files which contain only declarations, no code. The compiler then reads (effect, other) annotations from those stubs.

Another idea is to provide an API which lets users define effects of existing methods programmatically. Users would write a function of type Symbol => Option[Effect], and the framework would query those user-defined functions for symbols with unknown effect.

This is basically what we do currently in DefaultEffects. We would have to generalize that interface to allow programmers (not effect domain authors, but normal programmers that are using the effects plugin) do plug in their own defaults.

For symbols, this should be covered by the reflection api. However, the Effect type is only defined within the plugin, so it is unclear what representation of effects the user code would have to return.

Effect mismatch error on method invocation: show the latent effect of the function

When a (non-polymorphic, for this case see #6) method invocation triggers an effect mismatch error, it would be helpful to simply display the latent effect of the invoked method.

This example fails because println() does not have effect annotations:

  def foo: Unit @mod() = {
    println()
  }

The error message requires some time to understand:

T.scala:42: error: effect type mismatch;
 found   : @mod(any) @assign(any) @loc(any) @throws[Throwable] @io
 required: @mod() @loc(any) @throws[Throwable] @io
@mod(any) does not conform to @mod()
@assign(any) does not conform to @assign()
    println()
           ^
four errors found