WIP: Add Type/Predicate and make-positive-predicate

[AlexKnauth]

Addresses #457 by adding Type/Predicate and #:type/predicate as sound versions of what's most useful about Opaque and #:opaque.

• 1. A type constructor Type/Predicate that takes a predicate id and produces a type. If foo? is a predicate, then (Type/Predicate foo?) produces a type for values that have passed foo? even just once. So if (foo? x) returns #true and then returns #false, x still has type Foo after that.

• 2. A required/typed keyword [#:type/predicate Foo foo?] that imports the predicate foo? and defines the type Foo as (Type/Predicate foo?). The foo? predicate is imported with type (-> Any Boolean : #:+ Foo). It can not have type (-> Any Boolean : Foo).

• 3. A new expression form make-positive-predicate that takes a type and produces a predicate with only the positive #:+ proposition. So (make-positive-predicate X) will produce a predicate with the type (-> Any Boolean : #:+ X).

  • (make-positive-predicate (Type/Predicate foo?)) produces a predicate equivalent to foo? with type (-> Any Boolean : #:+ (Type/Predicate foo?))
  • (make-positive-predicate (Opaque foo?)) also produces a predicate equivalent to foo? with type (-> Any Boolean : #:+ (Opaque foo?))

• 4. Make sure make-predicate errors on Type/Predicate types, with an error message that suggests using make-positive-predicate instead. It should give a warning on Opaque types, similarly suggesting make-positive-predicate instead.

[samth]

What happens if we just change #:opaque to only have a positive predicate? How much breaks?

I'd really prefer not to add a lot more mechanism here.

[AlexKnauth]

If we did that then make-predicate could no longer soundly work on types containing Opaque types. Only make-positive-predicate could.

[samth]

That's also true of your proposal, I believe.

[AlexKnauth]

Yes, with my proposal make-predicate would be a warning on Opaque types, which would guide programmers toward the sound version. But it wouldn't be an error, so still unsound

[samth]

I should also say that this change will definitely require an RFC, and I encourage you to first write that and go through the process before working too much more on the implementation.

[AlexKnauth]

Closed to be replaced by #882