Effect members and annotations for imported Java code

[maxeonyx]

Summary

This is a PR affecting the Wyvern interpreter. It adds more fine-grained control over effects when importing code from Java. In particular, there are 2 main changes:

1. Automatically generating fresh effect types for imported Java methods.
2. Respecting the use of new @Pure and @Effect annotations in imported Java code

Together these changes improve the interop between Wyvern and Java. However, there are some incomplete parts of the PR (eg. tests) and some minor open questions.

I have a wrapper repository for this project, with Wyvern examples and proof of concepts, and config for using IntelliJ IDEA with Wyvern, located at maxeonyx/summer-research-project.

Motivation

This work address two problems that exist when calling Java code from Wyvern:

• Included code is always annotated with effects, even when it is pure.
• The effect type is always just the system.FFI effect type.

As a result, FFI code cannot be used in a pure context (Unless added to the global whitelist), and the effects of different FFI methods (being all system.FFI) are compatible by default, even when this doesn't make sense (such as read and write effects in some kind of IO module)

Work

Fresh Effect Members

The first change is automatically generating fresh effect types for imported Java methods. These are present as effect members on the type of an imported object. This means that all FFI methods no longer have the effect type system.FFI. Instead, a method obj.doThing on an object obj will be annotated with the effect type corresponding to the effect member obj.doThingEffect.

This presents some incompatibilities with the current approach. It is common for Wyvern modules to define some effect types by abstracting over system.FFI. e.g.

effect print = {system.FFI}
effect flush = {system.FFI}

In the new approach, each FFI method (by default) has a different effect, and so the exported effect types must be defned by abstracting the union of all effect types in the module. e.g.

import java:wyvern.stdlib.support.Stdio.stdio

effect print = {stdio.printEffect, stdio.printLnEffect, ...}
effect flush = {stdio.flushEffect}

Annotations

The second change adds two annotations, @Pure and @Effect, which together means that trusted Java libaries can be written so that when their methods are imported, Wyvern knows how to annotate them with effects.

@Pure means that Wyvern will not annotate the method with any effects.

@Effect allows referencing standard library effect types, instead of using the auto-generated FFI effects from the first change.

There are two limitations of the annotations:

1. The annotations are not checked by a purity analysis. I tried this but it was not useful because of A) The difficulty of writing or converting a library to be compatible with purity analysis. B) It would require Wyvern to compile java code on import in order to verify the purity annotations. The annotations must be trusted and as a result they can be applied incorrectly, and java libraries using them should be exposed to untrusted Wyvern modules with care.
2. Applying the annotations requires access to the source code of the libraries and so they are difficult to apply to third-party libraries such as the Java standard libraries.

What needs to be done to merge this PR

Currently the changes are mostly stable, but there are a few problems.

1. There are still some failing java-import-related tests.
2. There is an unanswered question about what to do about side effects in Java static initializers.
3. In principle, these changes make system.FFI obsolete. However, removing system.FFI breaks significant amount of existing code.

1. Tests

There are currently a number of failing tests. 13 of these I believe are related to my changes.

Failures related to my changes:

• ExampleTests.testIOLibServerClient
• ExampleTests.testTextEditorApplication
• EffectSystemTests.testFileIO1
• EffectSystemTests.testFileIO2
• EffectSystemTests.testFileIO3
• EffectSystemTests.testFileIO5
• EffectSystemTests.testLogger1
• EffectSystemTests.testLogger2
• EffectSystemTests.testLogger3
• EffectSystemTests.testLogger4
• EffectSystemTests.testFileIO
• EffectSystemTests.testLogger
• FileTest.stdlib

All of these failures are related to the first change, which changes the default effect type of FFI methods from system.FFI to a fresh type specific to each method. In code where there are existing annotations, such as with system.FFI or a derived type (eg. fileIOEffects.readF), this causes a type error. To fix this, either use the generated effect members, or add @Effect annotations to the wyvern java platform implementation.

Failures not related to my changes (I think):

• ExampleTests.testPython3Webserver
• ExampleTests.testPython2Webserver
• ExampleTests.testPythonCompilerOnScript
• all OIRTests
• ExampleTests.testBinarySearchTree

2. Static initializers

Java code can perform side effects when classes are loaded and static members are initialized. This currently happens when a java import statement is evaluated in Wyvern, because java imports always refer to a static singleton object for convienience. However, import statements can't have side effects in Wyvern.

This kind of side effect is admittedly rare, but an approach to managing it correctly would be to import classes instead of static instances eg.

// instead of 
import java:com.thing.Thing.instance

// do
import java:com.thing.Thing

This could be imported as a wyvern module object without initializing the class, and then the class could be initialized when the module is instantiated.

This would also be useful for another reason, which is that using an @Effect annotation adds module dependencies which are currently hidden from the user. These could be explicitly provided as in ordinary wvern modules.

However, this is a relatively big change, as it would affect all uses of java imports.

3. Removing or renaming system.FFI

With these changes, FFI methods have one of three kinds of effects:

1. Generated fresh effect (e.g. obj.doThingEffect)
2. No effects using @Pure
3. Referencing a standard library effect using @Effect (e.g. @Effect("stdout.print"))

system.FFI is now only used to define standard library effects, and actually has nothing to do with FFI. However, there is no mechanism in pure Wyvern for creating a fresh effect type, except for a hack with self-referencing dependent types. The ability to reference a fresh effect is neccesary for creating pure modules which export effect types. (eg. "wyvern/stdlib/platform/java/io/networkEffects.wyv") Currently system.FFI fills this role.

One simple approach could simply be renaming system.FFI, to make it match its new role.

How does this relate to the global whitelist (Global.java)

The global whitelist still exists, and still fills a role, which is eliminating the requirements for the java capability object when importing java code. However, objects/methods in the global whitelist are also marked as pure (this is the existing behavior). This now overlaps with the @Pure annotation, and this aspect of the global whitelist could in principle be removed.