Unsoundness from stateful #:opaque predicates

[AlexKnauth]

What version of Racket are you using?

I'm using version 6.7.0.1

If you got an error message, please include it here.

I didn't get an error message. I added the number 16 to the byte string #"abcdefg" and got a box pointing to the number 3136 as the answer.

What should have happened?

I'm not sure. Maybe occurrence typing has to work differently for #:opaque predicates?

What program did you run?

#lang typed/racket

(module untyped racket
  (provide x? reset!)
  (define b (make-parameter #true))
  (define (x? x)
    (cond [(b) (b #false) #true]
          [else #false]))
  (define (reset!) (b #true)))

(require/typed 'untyped
               [#:opaque X x?]
               [reset! (-> Void)])

(: ->false : (All (T) [Any -> Boolean : #:+ T]))
(define (->false v) #false)

(: transmute : (All (T) Any -> T))
;; This ends up always returning v
(define (transmute v)
  (reset!)
  ;; (x? v) returns #true the first time
  (if (or (x? v) ((inst ->false T) v))
      (if (not (x? v)) ; but #false the second time
          v
          (error "this never happens"))
      (error "this never happens")))

(+
           #b00000000000000000000000000010000
           (transmute ;(inst transmute Positive-Index)
            (string->bytes/utf-8 "abcdefg")))

[AlexKnauth]

What should happen?

It depends on the definition of (Opaque x?). Defining it as the set of values for which x? returns (present tense) true is not specific enough. There are four options that I see for defining it more precisely:

1. The set of values for which x? has ever returned true.
2. The set of values for which x? has always and will always return true.
3. The set of values for which x? has returned true and has not returned false (yet).
4. The set of values for which x? has ever or will ever return true but has not and will never return false.

Under definition 1, x? could have the type [Any -> Boolean : #:+ X], but not [Any -> Boolean : X] (where X is (Opaque x?)). Under definition 2, x? could have the type [Any -> Boolean : #:- (! X)]. With definitions 3 and 4, I'm not sure.

The current system assumes that x? is not stateful, so it ends up looking a little bit like definition 3, and when state is involved it causes this unsoundness. The combination of definition 3 with the current way of dealing with occurrence typing using intersections causes this unsoundness.

@pnwamk Do you have any ideas?

[samth]

It's important that people be able to select X's out a union (or out of Any) with x?, otherwise opaque types won't be useful (plus everyone's code will break). So definition 2 seems bad.

Note that we also use x? in the contract, which means that returning #t has to be a sufficient condition for membership in X.

[AlexKnauth]

Ok, so that rules out 2, but it also rules out 3 and 4, because if x? returns false the first time and then true the next time, it would not be a member of X. Does that mean it has to be definition 1? Does it mean that the negative side of the filter needs to be removed?

[samth]

If that's all we need to do, then it seems like less pain than I would expect from this problem (which I've known about for a long time).

[AlexKnauth]

The make-predicate form just came up in #456. If we change the type of the predicate to only include the positive filter, how would make-predicate need to change? Would we need a make-positive-predicate form so that we can produce a type without the negative filter?

[pnwamk]

Sorry for coming late to this.

I haven't thought about this a lot, but changes such as dropping propositions from the predicate seem to me like they would break programs that currently type check today with no win for those users if they're using the feature safely...

Ideally/in hind sight should Opaque types be declared with something that bears the prefix unsafe- since they provide a way for the user to add axioms to the type system which we cannot verify (at least I don't see how we could reasonably do so).

[samth]

1. I think breaking programs that currently use #:opaque isn't something we can do.
2. I don't see why make-predicate is a problem. The discussion in require/typed #opaque -> contract violation #456 is about opaque types. make-predicate is very different because we control the predicate created.

[pnwamk]

Perhaps we should do the following:

1. Deprecate the current form for declaring Opaque types and add a warning that it can lead to unsoundness.

2. Introduce a replacement interface for declaring Opaque types that uses the unsafe- prefix (and does not warn, since the behavior is warned by the prefix).

3. Come up a/ a sound version of Opaque that is free to not be 100% backwards compatible w/ the previous iteration.

[AlexKnauth]

There are two possible sound versions I can think of, and neither would work with make-predicate in the normal way.

1. Making it actually opaque, just like #:exists contracts, where it wraps the value in an opaque struct at the boundary.

2. Defining it as the set of values that have passed the predicate, but without excluding the ones that have failed it.

I was thinking of make-positive-predicate for both of these definitions. Both of them would be unsound if both the negative and the positive filters were there.

(make-positive-predicate X) would produce a predicate of the type [Any -> Boolean : #:+ X]. Once Unsafe-Opaque is there we could start making Opaque display a warning when used within make-predicate, and suggest using make-positive-predicate instead. That still leaves the predicate generated by #:opaque, so we would have to provide a safe renamed version to replace that.

[samth]

@AlexKnauth, is the problem you're thinking of wrt make-predicate just the use of it on opaque types?

[AlexKnauth]

Yes, that and types that contain opaque types, since the predicates for those could also be contradictory otherwise.

[pnwamk]

I think make-predicate is doing the right thing currently -- it would be unreasonable for it to try and right any and all potential wrongs users may have introduced by leveraging an unsound feature (which is what the current interface to Opaque types is).

edit: Ah, I just saw the suggestion that it could warn. That could be helpful... but I could also see it being a huge pain if I knowingly use unsafe-Opaque and then all sorts of Typed Racket features are constantly warning me about it. edit edit: Okay, the suggestion was only warning with Opaque - maybe that would be a nice middle ground.

[pnwamk]

I think option (2) sounds promising (and less invasive).

Here's my mental model for why the positive-predicate option I think is the best approach (sorry for the verbosity!):

Our Opaque types are simply types we know nothing about (and this is consistent with how we treat them in subtyping, etc). This is relatively harmless... it's just like having a variable ψ floating around in logical equations where we can't know anything about the contents of ψ while working with it (which we do all the time in math/logic/etc).

However, our current method for introducing an Opaque type τ also has the user axiomatically declare that some identifier pred? is a predicate for them. In other words, we assume this function pred? can tell us, for any value x, whether x ∈ τ or x ∉ τ. The former statement (x ∈ τ) is completely harmless since we have already decided it is impossible to know anything about τ, but the second statement is scary! Because x ∉ τ is equivalent to (x ∈ τ) → ⊥, we are putting quite a lot of trust in the declaration of pred?, since it can now be used to derive ⊥!

So... yah, at least as far as I've thought about it, I'm sold on excluding the negative proposition from an axiomatized, Opaque predicate as the sensible approach for getting rid of potential unsoundness while allowing the user to still declare and work with Opaque types.