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

isVolatile incorrect for intersection types #50

Closed
samuelgruetter opened this Issue Mar 7, 2014 · 57 comments

Comments

Projects
None yet
8 participants
@samuelgruetter
Copy link
Member

samuelgruetter commented Mar 7, 2014

@namin and me had a look at the isVolatile method in Types/TypeOps.

If we try the following example:

object Test {
  trait A {
    type X = String
  }
  trait B {
    type X = Int
  }
  lazy val o: A & B = ???

  def xToString(x: o.X): String = x

  def intToString(i: Int): String = xToString(i)
}

It's accepted by dotty, which means that we can cast Int to String...

I added debug output for the results of isVolatile, and it prints

isVolatile(AndType(TypeRef(ThisType(module class Test$),A),TypeRef(ThisType(module class Test$),B)))=false

But as we understood isVolatile, it should return true for all types which are possibly uninhabited.

The and-case in needsChecking looks bad:

case AndType(l, r) =>
  needsChecking(l, true) || needsChecking(r, true)

because we cannot just look seperately at l and r, but we should check if there are conflicting members in l and r.

In Scala, this is not a problem, because we only have with, which is asymmetric, so the members of r override those of l and in our example, o.X is only Int.

From a theoretical point of view, we are bothered by the fact that !isVolatile is not preserved by weakening, i.e.

A <: B and !isVolatile(B) does not imply !isVolatile(A)

so we doubt if a !isVolatile judgment would be useful in a typesafety proof (needs more thinking...).

Additionally, if we replace the implementation of needsChecking (which seems to be just an optimization) by this

def needsChecking(tp: Type, isPart: Boolean): Boolean = true

we get a java.util.NoSuchElementException: head of empty list, so it's not just an optimization...

@samuelgruetter

This comment has been minimized.

Copy link
Member Author

samuelgruetter commented Mar 7, 2014

I just checked with the changes from #47 , but this problem remains (which is not surprising because #47 does not change isVolatile...)

odersky added a commit to odersky/dotty that referenced this issue Mar 9, 2014

Fix of lampepfl#50 - volatile
Volatile checking needs to take all intersections into account; previously these
could be discarded through needsChecking.

Plus several refactorings and additions.

1) Module vals now have Final and Stable flags set
2) All logic around isVolatile is now in TypeOps; some of it was moved from Types.
3) Added stability checking to Select and SelectFromType typings.

Todo: We should find a better name for isVolatile. Maybe define the negation instead under the name
"isRealizable"?.

@odersky odersky closed this Mar 9, 2014

samuelgruetter added a commit to samuelgruetter/dotty that referenced this issue Mar 9, 2014

@odersky odersky reopened this Mar 12, 2014

@odersky

This comment has been minimized.

Copy link
Contributor

odersky commented Mar 12, 2014

Reopening to keep the test case around for the time we have refchecks written.

odersky added a commit that referenced this issue Mar 12, 2014

@samuelgruetter

This comment has been minimized.

Copy link
Member Author

samuelgruetter commented Nov 24, 2014

@smarter In this example, if we remove lazy, the program will crash when evaluating ???, so if we can cast Int to String afterwards, no one cares. However, if o is lazy (but never forced), we can cast Int to String, which is a typesafety breach.

@smarter

This comment has been minimized.

Copy link
Member

smarter commented Nov 18, 2015

@odersky : does this still need to be kept open?

@odersky

This comment has been minimized.

Copy link
Contributor

odersky commented Nov 19, 2015

Yes, the error is not detected. I'll put a test in pending/neg.

@namin

This comment has been minimized.

Copy link
Member

namin commented Jan 29, 2016

Note that instead of an unimplemented lazy val, we could also have a null val.
We can also interchange with and &.

@RossTate and I found a similar issue that also affects scalac:
https://issues.scala-lang.org/browse/SI-9633

@odersky

This comment has been minimized.

Copy link
Contributor

odersky commented Jan 29, 2016

Good point. I think this would have a fix analogous to lazy vals: We need a
predicate that a type is guaranteed
to have good bounds under all possible refinements (i.e. the opposite of
the isVolatile, after that is fixed). It can be a conservative
approximation. Let's call it "alwaysGoodBounds" (agp).

Then for

lazy val x: T = ...
val x: T = null
T # A

T must in each case be agp.

Wdyt?

On Fri, Jan 29, 2016 at 7:12 AM, Nada Amin notifications@github.com wrote:

Note that instead of an unimplemented lazy val, we could also have a null
val.
We can also interchange with and &.

@RossTate https://github.com/RossTate and I found a similar issue that
also affects scalac:
https://issues.scala-lang.org/browse/SI-9633


Reply to this email directly or view it on GitHub
#50 (comment).

Martin Odersky
EPFL

@namin

This comment has been minimized.

Copy link
Member

namin commented Jan 29, 2016

Not sure I understand how the proposal would work.

  1. For val x: T = null, how would you enforce T agp for val x: T = <arbitrary expression that evaluates to null>?
  2. Also, how would you handle the case below? It seems like you'd need to consider every parameter type as well?
  trait A { type L <: Nothing }
  trait B { type L >: Any}
  def id1(b: B, x: Any): b.L = x
  def id2(p: B with A)(x: Any): Nothing = id1(p, x)
  def id3(x: Any): Nothing =  id2(null)(x)
  println(id3("oh"))
@odersky

This comment has been minimized.

Copy link
Contributor

odersky commented Jan 29, 2016

One option would be to make Null a subtype only of (agp) types?

On Fri, Jan 29, 2016 at 9:41 AM, Nada Amin notifications@github.com wrote:

Not sure I understand how the proposal would work.

For val x: T = null, how would you enforce T agp for val x: T =
?
2.

Also, how would you handle the case below? It seems like you'd need to
consider every parameter type as well?

trait A { type L <: Nothing }
trait B { type L >: Any}
def id1(b: B, x: Any): b.L = x
def id2(p: B with A)(x: Any): Nothing = id1(p, x)
def id3(x: Any): Nothing = id2(null)(x)
println(id3("oh"))


Reply to this email directly or view it on GitHub
#50 (comment).

Martin Odersky
EPFL

@DarkDimius

This comment has been minimized.

Copy link
Member

DarkDimius commented Jan 30, 2016

Note that you can also have expression evaluate to null due to initialization order:

class C {
  val a: T = method
  def method = b
  val b: T = a
}

(new C).a#A

This code is type correct for any T, a and b are always initialized to null, there is no particular place to issue a warning(method could be implemented in a subclass).

@odersky

This comment has been minimized.

Copy link
Contributor

odersky commented Jan 30, 2016

@DarkDimius Yes, I know. We need to fix initialization separately. One thing after another. Right now, we need to classify programs that access uninitialized data as potentially unsound.

@namin

This comment has been minimized.

Copy link
Member

namin commented Jan 30, 2016

@odersky -- to enforce Null <: agp, you'd also have to enforce agp <: non-agp, otherwise you could circumvent the check through a chain of casts? I don't see how you'd get agp <: non-agp, e.g. Any <: x.L, but then I don't know what exactly you have in mind for agp.

@odersky

This comment has been minimized.

Copy link
Contributor

odersky commented Jan 30, 2016

@namin I think if you have Null <: agp <: non-agp then non-agp cannot constitute a soundness hole, because the bounds are known to be good through the agp <: non-agp relationship.

But on second thought we should wait until we address the problem at the root with the null-safe type system we planned. Then null would be its own type, anything nullable would be represented as T | Null , and we can decree that if x: T | Null then x is not a path.

odersky added a commit to dotty-staging/dotty that referenced this issue Jan 30, 2016

@namin

This comment has been minimized.

Copy link
Member

namin commented Jan 30, 2016

@odersky -- maybe you're right about agp <: non-agp

The second proposal feels right long-term...

@namin

This comment has been minimized.

Copy link
Member

namin commented Jan 30, 2016

Yet another variation (relevant to agp proposal), showing interaction with polymorphism and subtyping constraints.

  trait A { type L <: Nothing }
  trait B { type L >: Any}
  def id1(b: B, x: Any): b.L = x
  def id2[C, A1 >: C <: A, B1 >: C <: B](c: C, x: Any): Nothing = {
    val c1: B1 with A1 = c
    id1(c1, x)
  }
  def id3(x: Any): Nothing = id2[Null, A, B](null, x)
  println(id3("oh"))
@TiarkRompf

This comment has been minimized.

Copy link

TiarkRompf commented Jan 31, 2016

@odersky what is the proposed definition of 'always good bounds'? We know that previous definitions of realizability are not preserved through narrowing, which (I believe) is the problem we're observing here.

Another variation (with either null or lazy, both of which are not supported by the theory):

    trait A { type L <: Nothing }
    trait B { type L >: Any}
    trait U { 
      val p: B
      // or: lazy val p: B
      def brand(x: Any): p.L = x 
    }
    trait V extends U { 
      val p: A & B = null
      // or: lazy val p: A & B = ???
    }
    val v = new V {}
    v.brand("boom!")
@namin

This comment has been minimized.

Copy link
Member

namin commented Jan 31, 2016

@TiarkRompf -- cool example. In scalac (with B with A instead of A & B), it's a compile time error because any refined val p is checked for incompatible bounds.

@TiarkRompf

This comment has been minimized.

Copy link

TiarkRompf commented Jan 31, 2016

@namin Well, slight variations break in scalac as well:

    trait A { type L <: Nothing }
    trait B { type L >: Any}
    trait U { 
      type X <: B
      val p: X
      def brand(x: Any): p.L = x 
    }
    trait V extends U { 
      type X = B with A
      val p: X = null
      // or: lazy val p: X = ???
    }
    val v = new V {}
    v.brand("boom!"): Nothing
@odersky

This comment has been minimized.

Copy link
Contributor

odersky commented Jan 31, 2016

@namin Does scalacs checking also work if the bad bounds arise from an intersection somewhere deeper?

It looks to me we also have to enforce that val's used in paths are final.

@odersky

This comment has been minimized.

Copy link
Contributor

odersky commented Feb 2, 2016

@RossTate I tried to convert your example to Scala but it does not pass:

object unsound {
  trait Bound[A, B <: A]
  trait Bind[A] {
    def bad[B <: A](bound: Bound[A, B], b: B) = b
  }
  def coerce[T, U](t: T): U = {
    lazy val bound: Bound[U, _ >: T] = ???
    def bind = new Bind[U] {}
    bind.bad(bound, t)
  }
}

Compiling this gives:

error: Type argument  >: T does not conform to upper bound U 
    lazy val bound: Bound[U, _ >: T] = ???
                             ^

one error found

@odersky odersky closed this Feb 2, 2016

@odersky odersky reopened this Feb 2, 2016

@RossTate

This comment has been minimized.

Copy link

RossTate commented Feb 2, 2016

It wouldn't translate to Scala. Java's wildcards generate implicit constraints, whereas Scala's do not. Here's a simpler example:

class Numbers<N extends Number> extends List<N> {...}
Numbers<? extends Number> foo(Numbers<?> n) { return n; }

This type checks in Java because Java infers that the wildcard in Numbers<?> must be a subtyping of Number because whatever type it is abstracting must be a valid type argument for Numbers. Scala, on the other hand, is unable to recognize that every Numbers[_] is also a Numbers[_<:Number].

But the high-level strategy of this example is that same as what @namin and I came up with for Scala: rather than writing the inconsistent bounds directly, where the compiler would check for consistency, instead figure out some way to have inconsistent bounds be generated, where the compiler would not check for consistency. In my Java example, I do this using implicit constraints (and use the Bind class to get around some hack in the compiler). In @namin's and my Scala example, we do this using trait intersection. Both compilers have ad-hoc methods for preventing these, but adding enough layers of indirection seems to always eventually get around those hacks.

@TiarkRompf

This comment has been minimized.

Copy link

TiarkRompf commented Feb 2, 2016

Good observations, @RossTate, and interesting to see how this plays out in Java.

I think one important bit we've learnt from the DOT proofs is that most static predicates (like realizability of types) are not preserved by narrowing. So whenever we want to use realizability as a safeguard (instead of knowing that a type must be inhabited through evaluation) we're on thin ice, and we have to be very careful that narrowing (through function calls or inheritance) is ruled out.

For top-level lazy vals the restrictions we have now look reasonable to me (non-overridable definition of the lazy val, non-overridable definition of its type).

But for the other bits I don't the fix is quite there yet (cc @odersky). The length > 1 path example seems to be unchanged (?), and the by-name one blows up with a little more indirection:

    trait A { type L <: Nothing }
    trait B { type L >: Any }
    def f(x: => B)(y: Any):x.L = y
    def f1(x: => A & B)(y: Any):Nothing = f(x)(y)
    f1(???)("boom!"): Nothing

When I said these issues were easy to fix I thought of a more conservative solution, i.e. of disallowing by-name values in paths, and restricting lazy vals to be endpoints in paths (but of course this doesn't rule out solutions based on more elaborate checks).

@RossTate

This comment has been minimized.

Copy link

RossTate commented Feb 2, 2016

I agree. I think it's safe to say that you can't soundly have bounded virtual types, intersection types, and a (lazily) inhabitable bottom type.

@odersky

This comment has been minimized.

Copy link
Contributor

odersky commented Feb 2, 2016

@TiarkRompf You need to compile with -strict. We check fields for
realizability only under strict mode.
Because fields currently could be null (and therefore in the new typesystem
not eligible as paths),
we risk get false negatives if we make every unrealizable field as an
error.

Cheers

  • Martin

On Tue, Feb 2, 2016 at 7:33 PM, Ross Tate notifications@github.com wrote:

I agree. I think it's safe to say that you can't soundly have bounded
virtual types, intersection types, and a (lazily) inhabitable bottom type.


Reply to this email directly or view it on GitHub
#50 (comment).

Martin Odersky
EPFL

@TiarkRompf

This comment has been minimized.

Copy link

TiarkRompf commented Feb 2, 2016

@odersky ok, got it now. The nested path fails with -strict, but the second by-name example still goes through.

@odersky

This comment has been minimized.

Copy link
Contributor

odersky commented Feb 2, 2016

@TiarkRompf Which example did you mean?

On Tue, Feb 2, 2016 at 8:41 PM, Tiark Rompf notifications@github.com
wrote:

@odersky https://github.com/odersky ok, got it now. The nested path
fails with -strict, but the second by-name example still goes through.


Reply to this email directly or view it on GitHub
#50 (comment).

Martin Odersky
EPFL

@TiarkRompf

This comment has been minimized.

Copy link

TiarkRompf commented Feb 2, 2016

This one:

    trait A { type L <: Nothing }
    trait B { type L >: Any }
    def f(x: => B)(y: Any):x.L = y
    def f1(x: => A & B)(y: Any):Nothing = f(x)(y)
    f1(???)("boom!"): Nothing
@odersky

This comment has been minimized.

Copy link
Contributor

odersky commented Feb 2, 2016

@TiarkRompf Ah I overlooked that. But it seems anyway we should reject all cbn parameters as paths because they can have different values on each call. Do you agree?

@TiarkRompf

This comment has been minimized.

Copy link

TiarkRompf commented Feb 2, 2016

Yes, agreed.

@namin

This comment has been minimized.

Copy link
Member

namin commented Jun 9, 2016

I just thought I'd mention this here. I tried running the unsound null example in earlier versions of Scala (<=2.9.3) but interestingly, it doesn't compile due to restrictions on dependent method types. Does that suggest a static null containment strategy only for arguments of dependent methods, or am I missing something?

When I try to convert to OO in order to avoid dependent methods, I get the usual checks for good bounds in objects.

@namin

This comment has been minimized.

Copy link
Member

namin commented Jun 10, 2016

Ah, nevermind. As @odersky hinted, the dependent method type is just one more restriction rather than essential. @TiarkRompf already had some earlier examples with no dependent methods: #50 (comment)

Here's an example that compiles with all major Scala releases listed in the download page, including 2.5 to 2.9.

object unsound_legacy {
  trait LowerBound[T] {
    type M >: T;
  }
  trait UpperBound[U] {
    type M <: U;
  }
  trait Upcast[T] {
    type X <: LowerBound[T]
    def compute: X
    final val ub: X = compute
    def upcast(t: T): ub.M = t
  }
  class Coerce[T,U] extends Upcast[T] {
    type X = LowerBound[T] with UpperBound[U]
    override def compute = null
    def coerce(t: T): U = upcast(t)
  }
  def main(args : Array[String]) : Unit = {
    val zero : String = (new Coerce[Int,String]).coerce(0)
    println("...")
  }
}
@olhotak

This comment has been minimized.

Copy link
Contributor

olhotak commented Oct 31, 2016

Current dotty master (9f3005c) still fails to reject the example from SI-9633.

@namin

This comment has been minimized.

Copy link
Member

namin commented Oct 31, 2016

Yes, @olhotak -- Scala and Dotty have deferred any fixes for null paths. In Dotty, the fixes have focused on lazy paths.

@smarter

This comment has been minimized.

Copy link
Member

smarter commented Oct 31, 2016

@olhotak I think you need -strict
EDIT: ah nevermind, this example uses null which we don't deal with yet as Nada said (waiting on non-nullable types)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment