Discussion: Stainless support for Co- and Contra-Variance

[saraswat]

(I am not yet sure this will end up being a Feature Request or a Bug Report and/or Documentation. But hopefully discussion of this will make its way into a Stainless primer on converting code...)

Background: Crucial to using a sophisticated language like Scala is understanding the type system and what you can get it to do for you idiomatically.

I am beginning to get a sense for how the Stainless design deals with Scala's type system (see various issues related to recursive types, existential types, type variable declarations .. note again that the issues are being driven from practical consdierations in trying to port a significant Java code base to Stainless, not from a language-level analysis).

Q: Is Stainless designed to support Scala's co- and contra-variance declarations?

Turns out that the following code "works" (i.e. Stainless compiles and terminates, without throwing a traceback or any other sign of discomfort).

object CheckCoVariance {
  trait A
  case class B() extends A
  case class CoBox[+X][(x:X)
  def m(a:CoBox[A]):A = a.x

  def use: Unit = {
     m(CoBox[B](B())
  }
}

This is great! Plan to use it. Are there any cautionary tales around co/contravariance that the designers / implementers of Stainless can think of that should be kept in mind by the programmer?

This brings up a related point: Is contra variance actually usable meaningfully in Stainless (for user-defined classes). My attempt at using it (schematically -- this is not motivated from real code I am working on) resulted in a surprising (new)) error.

Code:

object CheckContraVariance {
  trait A
  trait AA extends A
  case class B() extends AA
  case class ContraBox[-X](x:(X)=>A)
  def n(x:ContraBox[AA]):(AA)=>A = x.x
  def mn = {
    val  x : (A)=> A = (A)=> B()
    n(ContraBox[A](x))
  }
}

Error:

Compiling 31 Scala sources to /Users/savija/IdeaProjects/cake/stainless_test/verified/target/scala-2.12/classes ...
[warn] The Z3 native interface is not available. Falling back onto smt-z3.
[info] Generating VCs for those functions: 
[info] Checking Verification Conditions...
[info] Generating VCs for those functions: n$0
[error] Run has failed with error: stainless.verification.TypeCheckerUtils$TypeCheckingException: ADT Object must appear only in strictly positive positions of Object
[error] 
[error] stainless.verification.TypeChecker.$anonfun$$init$$25(TypeChecker.scala:270)
[error] stainless.verification.TypeChecker.$anonfun$$init$$25$adapted(TypeChecker.scala:268)
[error] scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:877)
[error] scala.collection.Iterator.foreach(Iterator.scala:941)
[error] scala.collection.Iterator.foreach$(Iterator.scala:941)
[error] scala.collection.AbstractIterator.foreach(Iterator.scala:1429)
[error] scala.collection.MapLike$DefaultKeySet.foreach(MapLike.scala:181)
[error] scala.collection.TraversableLike$WithFilter.foreach(TraversableLike.scala:876)
[error] stainless.verification.TypeChecker.$anonfun$$init$$23(TypeChecker.scala:268)
[error] stainless.verification.TypeChecker.$anonfun$$init$$23$adapted(TypeChecker.scala:266)
[error] scala.collection.TraversableLike$WithFilter.$anonfun$foreach$1(TraversableLike.scala:877)
[error] scala.collection.immutable.Map$Map2.foreach(Map.scala:159)

So a few questions:

• Is Stainless designed to work for contra?
• What is the error actually saying. What does ADT Object and Object mean?

Thanks!!

[jad-hamza]

Object is a special ADT which is introduced in one of the phases (I think TypeEncoding) to encode the hierarchy of types.

We have two ways of generating verification conditions, one with --type-checker (default) which for now disallows non strictly positive datatypes (see for instance : http://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/). The older verification condition generation with --type-checker=false allows those, but may suffer from soundness issues.

For now the "complex" types introduced by the TypeEncoding phase are not well supported by the default --type-checker option.