implement opaque-positive-predicate

Author: AlexKnauth

typed-racket-doc/typed-racket/scribblings/reference/special-forms.scrbl

@@ -496,10 +496,25 @@ the type:
 
 Evaluates to a predicate for the type @racket[t], with the type
 @racket[(Any -> Boolean : t)]. @racket[t] may not contain function types, or
-types that may refer to mutable data such as @racket[(Vectorof Integer)].}
+types that may refer to mutable data such as @racket[(Vectorof Integer)].
+
+If @racket[t] contains any @racket[Opaque] types, @racket[make-predicate] will
+produce a warning. You should use @racket[make-positive-predicate] instead.}
 
 @defform[(define-predicate name t)]{
-Equivalent to @racket[(define name (make-predicate t))].
+Equivalent to @racket[(define name (make-predicate t))].}
+
+@defform[(make-positive-predicate t)]{
+
+Evaluates to a predicate for the type @racket[t], with the type
+@racket[(Any -> Boolean : #:+ t)]. @racket[t] may not contain function types, or
+types that may refer to mutable data such as @racket[(Vectorof Integer)].
+
+@racket[make-positive-predicate] does work with @racket[Opaque] types
+without any warnings.}
+
+@defform[(define-positive-predicate name t)]{
+Equivalent to @racket[(define name (make-positive-predicate t))].}
 
 @section{Type Annotation and Instantiation}
 

typed-racket-lib/typed-racket/base-env/prims-contract.rkt

@@ -12,26 +12,28 @@
 ;;
 ;; - their implementations (under the same names) are defined at phase
 ;;   0 using `define` in the main module
-;; 
+;;
 ;; - the `forms` submodule uses `lazy-require` to load the
 ;;   implementations of the forms
 
 
 (provide require/opaque-type require-typed-struct-legacy require-typed-struct
          require/typed-legacy require/typed require/typed/provide
          require-typed-struct/provide core-cast make-predicate define-predicate
+         make-positive-predicate define-positive-predicate
          require-typed-signature)
 
 (module forms racket/base
   (require (for-syntax racket/lazy-require racket/base))
-  (begin-for-syntax 
+  (begin-for-syntax
     (lazy-require [(submod "..")
                    (require/opaque-type
                     require-typed-signature
                     require-typed-struct-legacy
                     require-typed-struct
                     require/typed-legacy require/typed require/typed/provide
-                    require-typed-struct/provide core-cast make-predicate define-predicate)]))
+                    require-typed-struct/provide core-cast make-predicate define-predicate
+                    make-positive-predicate define-positive-predicate)]))
   (define-syntax (def stx)
     (syntax-case stx ()
       [(_ id ...)
@@ -43,7 +45,8 @@
         require-typed-struct-legacy
         require-typed-struct
         require/typed-legacy require/typed require/typed/provide
-        require-typed-struct/provide make-predicate define-predicate)
+        require-typed-struct/provide make-predicate define-predicate
+        make-positive-predicate define-positive-predicate)
 
   ;; Expand `cast` to a `core-cast` with an extra `#%expression` in order
   ;; to prevent the contract generation pass from executing too early
@@ -204,7 +207,7 @@
               ;; define `cnt*` to be fixed up later by the module type-checking
               (define cnt*
                 (syntax-local-lift-expression
-                 (make-contract-def-rhs #'ty #f (attribute parent))))
+                 (make-contract-def-rhs #'ty #f #f (attribute parent))))
               (quasisyntax/loc stx
                 (begin
                   ;; register the identifier so that it has a binding (for top-level)
@@ -269,12 +272,18 @@
 ;; Conversion of types to contracts
 ;;  define-predicate
 ;;  make-predicate
+;;  define-positive-predicate
+;;  make-positive-predicate
 ;;  cast
 
 ;; Helpers to construct syntax for contract definitions
-;; make-contract-def-rhs : Type-Stx Boolean Boolean -> Syntax
-(define (make-contract-def-rhs type flat? maker?)
-  (define contract-def `#s(contract-def ,type ,flat? ,maker? untyped))
+;; make-contract-def-rhs : Type-Stx Boolean Boolean Boolean -> Syntax
+;; The exact? argument determines whether the contract must decide
+;; exactly whether the value has the type.
+;;  - flat? true and exact? true must generate (-> Any Boolean : type)
+;;  - flat? true and exact? false can generate (-> Any Boolean : #:+ type)
+(define (make-contract-def-rhs type flat? exact? maker?)
+  (define contract-def `#s(contract-def ,type ,flat? ,exact? ,maker? untyped))
   (contract-def-property #'#f (λ () contract-def)))
 
 ;; make-contract-def-rhs/from-typed : Id Boolean Boolean -> Syntax
@@ -291,7 +300,7 @@
          (if types
              #`(U #,@types)
              #f)))
-     `#s(contract-def ,type-stx ,flat? ,maker? typed))))
+     `#s(contract-def ,type-stx ,flat? #f ,maker? typed))))
 
 
 (define (define-predicate stx)
@@ -312,8 +321,9 @@
 (define (make-predicate stx)
   (syntax-parse stx
     [(_ ty:expr)
+     ; passing #t for exact? makes it produce a warning on Opaque types
      (define name (syntax-local-lift-expression
-                   (make-contract-def-rhs #'ty #t #f)))
+                   (make-contract-def-rhs #'ty #t #t #f)))
      (define (check-valid-type _)
        (define type (parse-type #'ty))
        (define vars (fv type))
@@ -325,6 +335,41 @@
      #`(#,(external-check-property #'#%expression check-valid-type)
         #,(ignore-some/expr #`(flat-contract-predicate #,name) #'(Any -> Boolean : ty)))]))
 
+
+(define (define-positive-predicate stx)
+  (syntax-parse stx
+    [(_ name:id ty:expr)
+     #`(begin
+         ;; We want the value bound to name to have a nice object name. Using the built in mechanism
+         ;; of define has better performance than procedure-rename.
+         #,(ignore
+            (syntax/loc stx
+              (define name
+                (let ([pred (make-positive-predicate ty)])
+                  (lambda (x) (pred x))))))
+         ;; not a require, this is just the unchecked declaration syntax
+         #,(internal (syntax/loc stx (require/typed-internal name (Any -> Boolean : #:+ ty)))))]))
+
+
+(define (make-positive-predicate stx)
+  (syntax-parse stx
+    [(_ ty:expr)
+     ; passing #f for exact? makes it work with Opaque types without warning
+     (define name (syntax-local-lift-expression
+                   (make-contract-def-rhs #'ty #t #f #f)))
+     (define (check-valid-type _)
+       (define type (parse-type #'ty))
+       (define vars (fv type))
+       ;; If there was an error don't create another one
+       (unless (or (Error? type) (null? vars))
+         (tc-error/delayed
+          "Type ~a could not be converted to a predicate because it contains free variables."
+          type)))
+     #`(#,(external-check-property #'#%expression check-valid-type)
+        #,(ignore-some/expr #`(flat-contract-predicate #,name) #'(Any -> Boolean : #:+ ty)))]))
+
+
+
 ;; wrapped above in the `forms` submodule
 (define (core-cast stx)
   (syntax-parse stx
@@ -349,7 +394,7 @@
             #'v]
            [else
             (define new-ty-ctc (syntax-local-lift-expression
-                                (make-contract-def-rhs #'ty #f #f)))
+                                (make-contract-def-rhs #'ty #f #f #f)))
             (define existing-ty-id new-ty-ctc)
             (define existing-ty-ctc (syntax-local-lift-expression
                                      (make-contract-def-rhs/from-typed existing-ty-id #f #f)))
@@ -397,7 +442,7 @@
            #,@(if (eq? (syntax-local-context) 'top-level)
                   (list #'(define-syntaxes (hidden) (values)))
                   null)
-           #,(internal #'(require/typed-internal hidden (Any -> Boolean : (Opaque pred))))
+           #,(internal #'(require/typed-internal hidden (Any -> Boolean : #:+ (Opaque pred))))
            #,(if (attribute ne)
                  (internal (syntax/loc stx (define-type-alias-internal ty (Opaque pred))))
                  (syntax/loc stx (define-type-alias ty (Opaque pred))))

typed-racket-lib/typed-racket/private/type-contract.rkt

@@ -30,7 +30,9 @@
   (c:contract-out
     [type->static-contract
       (c:parametric->/c (a) ((Type? (c:-> #:reason (c:or/c #f string?) a))
-                             (#:typed-side boolean?) . c:->* . (c:or/c a static-contract?)))]))
+                             (#:typed-side boolean? #:exact? boolean?)
+                             . c:->* .
+                             (c:or/c a static-contract?)))]))
 
 (provide change-contract-fixups
          change-provide-fixups
@@ -50,7 +52,11 @@
           #t)]
     [_ #f]))
 
-(struct contract-def (type flat? maker? typed-side) #:prefab)
+;; The exact? field determines whether the contract must decide
+;; exactly whether the value has the type.
+;;  - flat? true and exact? true must generate (-> Any Boolean : type)
+;;  - flat? true and exact? false can generate (-> Any Boolean : #:+ type)
+(struct contract-def (type flat? exact? maker? typed-side) #:prefab)
 
 ;; get-contract-def-property : Syntax -> (U False Contract-Def)
 ;; Checks if the given syntax needs to be fixed up for contract generation
@@ -83,7 +89,7 @@
 ;; (such as mutually recursive class types).
 (define (generate-contract-def stx cache sc-cache)
   (define prop (get-contract-def-property stx))
-  (match-define (contract-def type-stx flat? maker? typed-side) prop)
+  (match-define (contract-def type-stx flat? exact? maker? typed-side) prop)
   (define *typ (if type-stx (parse-type type-stx) t:-Dead-Code))
   (define kind (if (and type-stx flat?) 'flat 'impersonator))
   (syntax-parse stx #:literals (define-values)
@@ -104,6 +110,7 @@
         ;; unless it's used for with-type
         #:typed-side (from-typed? typed-side)
         #:kind kind
+        #:exact? exact?
         #:cache cache
         #:sc-cache sc-cache
         (type->contract-fail
@@ -124,6 +131,7 @@
     (type->contract type
                     #:typed-side #t
                     #:kind 'impersonator
+                    #:exact? #f
                     #:cache cache
                     #:sc-cache sc-cache
                     ;; FIXME: get rid of this interface, make it functional
@@ -281,17 +289,18 @@
    [(both) 'both]))
 
 ;; type->contract : Type Procedure
-;;                  #:typed-side Boolean #:kind Symbol #:cache Hash
+;;                  #:typed-side Boolean #:kind Symbol #:exact? Boolean #:cache Hash
 ;;                  -> (U Any (List (Listof Syntax) Syntax))
 (define (type->contract ty init-fail
                         #:typed-side [typed-side #t]
                         #:kind [kind 'impersonator]
+                        #:exact? [exact? #t]
                         #:cache [cache (make-hash)]
                         #:sc-cache [sc-cache (make-hash)])
   (let/ec escape
     (define (fail #:reason [reason #f]) (escape (init-fail #:reason reason)))
     (instantiate/optimize
-     (type->static-contract ty #:typed-side typed-side fail
+     (type->static-contract ty #:typed-side typed-side #:exact? exact? fail
                             #:cache sc-cache)
      fail
      kind
@@ -338,6 +347,7 @@
 
 (define (type->static-contract type init-fail
                                #:typed-side [typed-side #t]
+                               #:exact? [exact? #t]
                                #:cache [sc-cache (make-hash)])
   (let/ec return
     (define (fail #:reason reason) (return (init-fail #:reason reason)))
@@ -535,6 +545,10 @@
        [(Promise: t)
         (promise/sc (t->sc t))]
        [(Opaque: p?)
+        (when exact?
+          (eprintf
+           "warning: Opaque predicates cannot be used as exact decisions yes/no:\n  predicate: ~s\n"
+           (syntax-e p?)))
         (flat/sc #`(flat-named-contract (quote #,(syntax-e p?)) #,p?))]
        [(Continuation-Mark-Keyof: t)
         (continuation-mark-key/sc (t->sc t))]

typed-racket-lib/typed-racket/private/with-types.rkt

@@ -73,7 +73,7 @@
                  ;; this is a parameter to avoid dependency issues
                  [current-type-names
                   (lazy
-                    (append 
+                    (append
                      (type-name-env-map (lambda (id ty)
                                           (cons (syntax-e id) ty)))
                      (type-alias-env-map (lambda (id ty)
@@ -154,7 +154,7 @@
 (define (type-stxs->ids+defs type-stxs typed-side)
   (for/lists (_1 _2) ([t (in-list type-stxs)])
     (define ctc-id (generate-temporary))
-    (define contract-def `#s(contract-def ,t #f #f ,typed-side))
+    (define contract-def `#s(contract-def ,t #f #f #f ,typed-side))
     (values ctc-id
             #`(define-values (#,ctc-id)
                 #,(contract-def-property

typed-racket-test/fail/opaque-positive-predicate.rkt

@@ -0,0 +1,19 @@
+#lang typed/racket
+
+(module foo racket/base
+  (provide foo?)
+  (define x #false)
+  (define (foo? v) (set! x (not x)) x))
+
+(require/typed 'foo [#:opaque Foo foo?])
+;; foo? is a positive predicate: (-> Any Boolean : #:+ Foo)
+
+(: no+ (∀ (T) (-> Any Boolean : #:+ T)))
+(define (no+ v) #false)
+
+(: transmute (∀ (T) (-> Any T)))
+(define (transmute v)
+  (if (and (or (foo? v) ((inst no+ T) v)) (not (foo? v)))
+      v
+      (error 'absurd)))
+