-
Notifications
You must be signed in to change notification settings - Fork 65
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Effect members and annotations for imported Java code #390
Open
maxeonyx
wants to merge
17
commits into
master
Choose a base branch
from
java-purity
base: master
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
… longer necessary.
…ng the purity of static initialization.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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:
@Pure
and@Effect
annotations in imported Java codeTogether 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:
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 asread
andwrite
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 methodobj.doThing
on an objectobj
will be annotated with the effect type corresponding to the effect memberobj.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.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.
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:
What needs to be done to merge this PR
Currently the changes are mostly stable, but there are a few problems.
system.FFI
obsolete. However, removingsystem.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:
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 withsystem.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):
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.
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:
obj.doThingEffect
)@Pure
@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.