stainless

stainless copied to clipboard

The following code works in Scala and is an explicit way of representing closures as objects that capture their environment as a trait parameter. It does not work in Stainless because trait parameters are not supported. However, the syntactic sugar capturing could be perhaps supported and directly translated in imperative phase elimination.

//import stainless.annotation.*
object Capture:

  trait FunEff[A, E, B](val e: E):
    def apply(a: A): B
  end FunEff

  case class Ref[T](var content: T)

  def capturing[A, E, B](e1: E)(f: E => A => B): FunEff[A,E,B] =
    new FunEff[A, E, B](e1) {
      override def apply(a: A) = f(e)(a)
    }

  val adder = capturing(Ref[Int](0))((e: Ref[Int]) =>
    (a: Int) => 
      e.content = e.content + a
      e.content      
  )

  val incrementer = capturing(Ref(()))((_:Ref[Unit]) => 
    (a: Int) => a + 1
  )

end Capture

What do you think @mario-bucev @samarion ?

The most important thing is in fact to have something like FunEff that has a method that depends on a mutable trait parameter. How we construct instances of FunEff is less important.

When f : FunEff then f is an object with apply and a field storing a mutable object. So, a call

val b = f(a)

becomes something like

val (b,f1) = f.apply(f, a)

We can represent traits with mutable constructor fields by having each of the trait methods take that field as an extra argument, then applying the usual imperative transformation.

Regis wrote up an example with an SFun case class which does something similar: https://github.com/epfl-lara/stainless/blob/a041c9790d24411f45c4329526adec334bc71337/frontends/benchmarks/imperative/valid/Tutorial.scala#L192-L194

@samarion : thanks, that's it! I remembered, but could not find it in the benchmarks.

The question is if we want to make this more seamless, or just document it as a pattern.

On another note, the S in SFun or E in my example must be immutable. If you want to allow hierarchical state, then you would like to allow S/E to be mutable, but then perhaps no need to wrap it.

In case it's not obvious, this question was partly inspired by the bug https://github.com/epfl-lara/stainless/issues/1365