Issue with substituting `this` in effect annotations
Darya- opened this issue · 5 comments
In the text-editor application, define and use a logging effect. Namely, declare an effect in the Logger
type and use it to annotated the updateLog
method:
resource type Logger
effect WriteToLog
def updateLog(msg: String): {this.WriteToLog} Unit
Then, change the logger
module to be:
module def logger(logFile: fileSystem.File): Logger
effect WriteToLog = {logFile.Write}
def updateLog(msg: String): {WriteToLog} Unit
val logAppender = logFile.makeAppender()
logAppender.write(msg)
logAppender.close()
Run the text-editor application.
Expected behavior: No error is thrown
Actual behavior: The following error is thrown:
Effect "logAppender.Write" not found in scope at location file wyvern/stdlib/platform/java/fileSystem/Writer.wyt on line 3 column 9
The error message is not very good. It should read:
method "updateLog" has effect "logAppender.Write", which is not included in the declared effect "this.WriteToLog"
The problem is that in the current implementation of the fileSystem
library, File.makeAppender()
returns an object that has a Write
effect, and it does not specify that the Write
effect in the returned object is the same as the Write
effect of the original File
.
So the fix is actually a bit more complicated. First of all, the error message should be improved, as the current one is quite misleading. Second, the fileSystem
library should allow more precise reasoning about effects, so they can be accurately tracked in examples such as this one.
The signature of makeAppender
is:
def makeAppender() : Writer
but it should be:
def makeAppender() : {} Writer[this.Write]
(and maybe makeAppender
should also have an effect itself, e.g. if it opens a file that is not already open).
The point of this is to specify that writes on the Appender
are essentially writes to the underlying File
The error message was improved (though it's still not completely ideal) in commit ad591d5
The commit also improved general handling of effects based on a variable that goes out of scope.
Fully fixed in commit ad591d5