Skip to content

Commit 365807c

Browse files
AlexKnauthAlexKnauth
committed
start opaque-positive-predicate RFC
1 parent e90a2b9 commit 365807c

File tree

1 file changed

+192
-0
lines changed

1 file changed

+192
-0
lines changed

‎rfcs/text/0003-opaque-positive-predicate.md

Lines changed: 192 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,192 @@
1+
- Feature Name: opaque-positive-predicate
2+
- Start Date: 2019-11-30
3+
- RFC PR: (leave this empty)
4+
- Feature Commit(s): (leave this empty)
5+
6+
# Summary
7+
8+
The predicate in an `Opaque` type does not correspond to an exact decision yes/no, only a positive yes/unknown. This RFC defines the meaning of `Opaque` as the set of values the predicate has returned true for _at any point_ without excluding values the predicate has returned false for. It also provides `define-positive-predicate`, which defines positive yes/unknown predicates for types.
9+
10+
# Motivation
11+
12+
Currently `Opaque` and `#:opaque` are unsound because the result of the predicate on a value can change due to mutation (https://github.com/racket/typed-racket/issues/457). The unsoundness comes from a combination of two things:
13+
1. The predicate `foo?` is treated as an exact decision yes/no,
14+
in other words `foo? : (-> Any Boolean : Foo)`.
15+
2. The result of `(foo? x)` can change due to mutable state from `x`
16+
or even `foo?`.
17+
18+
This RFC fixes this unsoundness by changing (1) to a positive predicate, with type `(-> Any Boolean : #:+ Foo)`.
19+
20+
With a positive predicate, the type system still supports cases like:
21+
```racket
22+
; x : Any
23+
(cond [(foo? x) (use-foo x)]
24+
[else #f])
25+
```
26+
27+
However it no longer supports cases like:
28+
```racket
29+
; x : (U Foo String)
30+
(cond [(foo? x) #f]
31+
[else (use-string x)])
32+
```
33+
Because `(foo? x)` returning false no longer rules out the type `Foo`. A program like this would need `(string?x)` determine `String`.
34+
35+
# Guide-level explanation
36+
37+
## `require/typed` `#:opaque`
38+
39+
```racket
40+
(require/typed m rt-clause ...)
41+
42+
rt-clause = ...other-rt-clause...
43+
| [#:opaque t pred]
44+
```
45+
The `[#:opaque t pred]` case defines a new type `t` and imports `pred` from module `m`. `pred` is a predicate for the type `t`. The type is defined as those values for which `pred` has produced `#t`. `pred` must have type `(Any -> Boolean : #:+ t)`. Opaque types must be required lexically before they are used.
46+
47+
Examples:
48+
```racket
49+
> (require/typed racket/base
50+
[#:opaque Evt evt?]
51+
[alarm-evt (Real -> Evt)]
52+
[sync (Evt -> Any)])
53+
> evt?
54+
- : (-> Any Boolean : #:+ Evt)
55+
#<procedure:evt?>
56+
> (sync (alarm-evt (+ 100 (current-inexact-milliseconds))))
57+
- : Any
58+
#<alarm-evt>
59+
```
60+
61+
## `Opaque`
62+
63+
```racket
64+
(Opaque pred)
65+
```
66+
A type constructed using the `#:opaque` clause of `require/typed`. Defined as those values for which `pred` has produced `#t`.
67+
68+
Examples:
69+
```racket
70+
> (require/typed racket/base
71+
[#:opaque Evt evt?])
72+
> (:type Evt)
73+
(Opaque evt?)
74+
```
75+
76+
## `define-positive-predicate`
77+
78+
```racket
79+
(make-positive-predicate t)
80+
```
81+
Evaluates to a predicate for the type `t`, with the type `(Any -> Boolean : #:+ t)`. When the predicate returns true on a value, that value is known to have type `t`. However, when the predicate returns false, the type is unchanged.
82+
83+
`t` may not contain function types, or types that may refer to mutable data such as `(Vectorof Integer)`. `make-positive-predicate` works with `Opaque` types such that `(make-positive-predicate (Opaque pred))` has the same runtime behavior as `pred`.
84+
85+
```racket
86+
> (make-positive-predicate Integer)
87+
- : (-> Any Boolean : #:+ Integer)
88+
#<procedure:exact-integer?>
89+
> ((make-positive-predicate Integer) 12)
90+
- : Boolean
91+
#t
92+
```
93+
94+
```racket
95+
(define-positive-predicate name t)
96+
```
97+
Equivalent to `(define name (make-positive-predicate t))`, defining `name` with the type `(Any -> Boolean : #:+ t)`. When `name` returns true on a value, that value is known to have type `t`. However, when `name` returns false, the type is unchanged.
98+
99+
```racket
100+
> (define-positive-predicate listof-integer? (Listof Integer))
101+
> listof-integer?
102+
- : (-> Any Boolean : #:+ (Listof Integer))
103+
#<procedure:listof-integer?>
104+
> (listof-integer? (list 3 5 8))
105+
- : Boolean
106+
#t
107+
```
108+
109+
# Reference-level explanation
110+
111+
## `require/typed` `#:opaque`
112+
113+
```racket
114+
(require/typed m rt-clause ...)
115+
116+
rt-clause = ...other-rt-clause...
117+
| [#:opaque t pred]
118+
```
119+
An `#:opaque` clause within `require/typed` expands to `require/opaque-type` from `typed-racket/base-env/prims-contract.rkt`:
120+
```racket
121+
(require/opaque-type t pred m maybe-unsafe maybe-name-exists)
122+
123+
maybe-unsafe =
124+
| unsafe-kw
125+
126+
maybe-name-exists =
127+
| #:name-exists
128+
```
129+
It imports `pred` from `m`, guarded with contract `(any-wrap-warning/c . c-> . boolean?)` unless `unsafe-kw` is provided. It defines `t` as a type alias for `(Opaque pred)`, and gives `pred` the type `(-> Any Boolean : #:+ (Opaque pred))`.
130+
131+
## `Opaque`
132+
133+
```racket
134+
(Opaque pred)
135+
```
136+
A type constructed using the `#:opaque` clause of `require/typed`. Defined as those values for which `pred` has produced `#t`. Note that `pred` returning `#f` on a value does _not_ exclude the value from having type `(Opaque pred)`, since `pred` might return `#t` at a different time.
137+
138+
## `define-positive-predicate`
139+
140+
```racket
141+
(make-positive-predicate t)
142+
```
143+
Evaluates to a predicate for the type `t`, with the type `(Any -> Boolean : #:+ t)`. When the predicate returns true on a value, that value is known to have type `t`. However, when the predicate returns false, the type is unchanged.
144+
145+
`t` may not contain function types, or types that may refer to mutable data such as `(Vectorof Integer)`. `make-positive-predicate` works with `Opaque` types such that `(make-positive-predicate (Opaque pred))` has the same runtime behavior as `pred`.
146+
147+
```racket
148+
(define-positive-predicate name t)
149+
```
150+
Equivalent to `(define name (make-positive-predicate t))`, defining `name` with the type `(Any -> Boolean : #:+ t)`. When `name` returns true on a value, that value is known to have type `t`. However, when `name` returns false, the type is unchanged.
151+
152+
## Interaction with define-predicate
153+
154+
Using `make-predicate` or `define-predicate` on types with `Opaque` in them produces a _warning_ for now. Later this warning should be changed to an error to fully close the unsoundness shown in Motivation and https://github.com/racket/typed-racket/issues/457. For example:
155+
```racket
156+
(require/typed racket/base
157+
[#:opaque Evt evt?])
158+
(define-predicate evt?-v2 Evt)
159+
```
160+
produces a warning, while using `define-positive-predicate` is safe.
161+
162+
To implement this warning on types with `Opaque` without triggering the warning on other normal first-order types, `define-predicate` passes an `exact?` argument as true when generating the contract. If `type->static-contract` finds an `Opaque` type when `exact?` is true, it triggers the warning.
163+
164+
# Drawbacks and Alternatives
165+
[drawbacks]: #drawbacks
166+
167+
The main reason *not* to do this is backwards compatibility for programs that use the negative proposition in the predicates for opaque types. Programs like this:
168+
```racket
169+
(require/typed m [#:opaque Foo foo?])
170+
(: f (-> (U Foo String) String))
171+
(define (f x)
172+
(cond [(foo? x) ""]
173+
[else x]))
174+
```
175+
which typechecked before, will no longer typecheck since in the else case `x` still has type `(U Foo String)` rather than being refined to `String`.
176+
177+
There are alternative ways to close the unsoundness shown in Motivation and https://github.com/racket/typed-racket/issues/457. The unsoundness is caused by two things together: (1) exact decisions yes/no from predicates, and (2) mutation changing predicate answers. This RFC addresses it by changing (1), so an alternative is to leave (1) alone and fix (2) instead. This could be done by enforcing purity, although it would have to enforce purity in untyped code as well, which is impractical. An less-restrictive property to enforce is "no take-backs", which could be done with contract wrappers that memoize every input-output pair, raising an error if an output is different from the previous outputs for the same inputs.
178+
179+
# Prior art
180+
[prior-art]: #prior-art
181+
182+
Prior versions of types based on predicates usually use the predicate as an exact decision yes/no, and rely on the assumption that the results of the predicate don't change. In pure languages such as Haskell, ACL2, or Coq, this is a valid assumption. Other languages such as Dafny constrain predicates to a subset of the language that restricts reading or writing state unless specifically annotated. This allows the compiler to use the predicate as an exact decision only for the region in which no state changes occur.
183+
184+
However, Typed Racket cannot enforce those restrictions on all opaque prediactes because they often come from untyped code which the typechecker has no control over.
185+
186+
# Unresolved questions
187+
[unresolved]: #unresolved-questions
188+
189+
I have three unresolved questions:
190+
1. Design: is changing the existing `Opaque` and `#:opaque` for soundness preferable even if it's not strictly backwards compatible, or would it better to adding entirely new sound versions?
191+
2. Implementation: to distinguish types that provide exact decision yes/no predicates (`define-predicate` works with no warning) from types that provide only positive yes/unknown predicates (`define-positive-predicate` works, but `define-predicate` produces a warning), is passing a new `exact?` argument to contract-generation good, or is there a better way to implement it?
192+
3. Timing: after the warning is put in place on uses of `define-predicate` with `Opaque` types, how long should we wait until making it an error to fully close the unsoundness? 1 release cycle, 2 release cycles, or more?

0 commit comments

Comments
 (0)