wyvernlang/wyvern

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

I believe it was fixed in 259a153 instead.