Mutable strings are unsound with (make-predicate "abc")

[SuzanneSoy]

What version of Racket are you using?

6.7.0.4

What program did you run?

#lang typed/racket
(define s (string #\a #\b #\c))
(if ((make-predicate "abc") s)
      (begin
        (string-set! s 1 #\x)
        (ann s "abc"))
      #f)

What should have happened?

make-predicate should refuse to generate the predicate, as it needs a non-flat contract.

I think it's best to wait until immutable data structures are implemented in TR before fixing this, as this may otherwise break programs which rely on make-predicate (and string mutations are exceedingly rare). Then it will be possible to write (make-predicate (∩ Immutable "abc")) or something similar.

The type of the generated predicate can also be changed to (-> Any Boolean : #:+ "abc" #:- (or (not "abc") Mutable)), although that goes against the general pattern for make-predicate which always generates (-> Any Boolean : T). Maybe it would be interesting in the future to have weaker versions (make-pos-predicate T) which returns a predicate with the type (-> Any Boolean : #:+ T) and (make-neg-predicate T) which returns a predicate with the type (-> Any Boolean : #:- T) ?

[AlexKnauth]

Subtyping for strings needs to keep mutability into account. In other words if the type "abc" is meant to include mutable strings, then it can't be a subtype of String if String allows it to be mutated to contain different characters. However I'm guessing the intention was for "abc" to not include mutable strings. That seems like the simplest fix; the generated predicate would just have an extra immutable? condition. String literals are already immutable.

[SuzanneSoy]

@AlexKnauth True, If I understand you correctly, "abc" should be interpreted as (∩ Immutable "abc") by default?

Also, my type above (-> Any Boolean : #:+ "abc" #:- (or (not "abc") Mutable)) was wrong I think, it should be (-> Any Boolean : #:+ "abc" #:- (or (not String) Mutable)).

[AlexKnauth]

There are two possibilities, based on different interpretations of what "abc" means:

1. The type "abc" includes mutable strings. The contract would have to be a chaperone contract so that mutable strings can be checked at every access or mutation. In this case make-predicate should fail because it cannot be checked with a flat contract. This would potentially break programs that use make-predicate with string literal types.

2. The type "abc" only includes immutable strings. The contract can be flat, and it will include an immutable? check. This could potentially break programs that use mutable strings at these types, probably through contracts, with cast or required/typed.

[LiberalArtist]

This seems somewhat related to racket/racket#2179.