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

typed-racket-doc/typed-racket/scribblings/reference/libraries.scrbl

@@ -287,7 +287,7 @@ following steps are required:
   @item{Determine the data manipulated by the library, and how it will
   be represented in Typed Racket.}
   @item{Specify that data in Typed Racket, using @racket[require/typed]
-  and @racket[#:opaque] and/or @racket[#:struct].}
+  and @racket[#:type/predicate] and/or @racket[#:struct].}
   @item{Use the data types to import the various functions and constants
   of the library.}
   @item{Provide all the relevant identifiers from the new adapter module.}

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

@@ -487,11 +487,26 @@ the type:
 @defform[(make-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[(Any -> Boolean : t)]. @racket[t] may not contain function types,
+@racket[Type/Predicate] types, or types that may refer to mutable data
+such as @racket[(Vectorof Integer)].
+
+If the type @racket[t] includes @racket[Type/Predicate] types,
+@racket[make-positive-predicate] should be used 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[Type/Predicate] types.}
+
+@defform[(define-positive-predicate name t)]{
+Equivalent to @racket[(define name (make-positive-predicate t))].}
 
 @section{Type Annotation and Instantiation}
 
@@ -611,6 +626,7 @@ optionally-renamed identifier.
             [#:struct maybe-tvars (name-id parent) ([f : t] ...)
                  struct-option ...]
             [#:opaque t pred]
+            [#:type/predicate t pred]
 	    [#:signature name ([id : t] ...)]]
  [maybe-renamed id
                 (orig-id new-id)]
@@ -664,6 +680,11 @@ Opaque types must be required lexically before they are used.
     evt?
     (sync (alarm-evt (+ 100 (current-inexact-milliseconds))))]
 
+@index["type/predicate"]{The fifth case} defines a new type @racket[t]
+to represent values which have passed @racket[pred] at any point.
+@racket[pred] is imported from module @racket[m] with type
+@racket[(Any -> Boolean : #:+ t)].
+
 @index["signature"]{The @racket[#:signature] keyword} registers the required
 signature in the signature environment. For more information on the use of
 signatures in Typed Racket see the documentation for

typed-racket-doc/typed-racket/scribblings/reference/typed-units.scrbl

@@ -255,6 +255,7 @@ The primary use of is for the reflective operation @racket[unit?]}
             [#:struct (name parent) ([f : t] ...)
                  struct-option ...]
             [#:opaque t pred]
+            [#:type/predicate t pred]
 	    [#:signature name ([id : t] ...)]]
  [maybe-renamed id
                 (orig-id new-id)]

typed-racket-doc/typed-racket/scribblings/reference/types.scrbl

@@ -1020,4 +1020,9 @@ prefab types with the (implicitly quoted) prefab-key
 @defform[(Opaque t)]{A type constructed using the @racket[#:opaque]
 clause of @racket[require/typed].}
 
+@defform[(Type/Predicate pred-id)]{
+  A type constructed using the @racket[#:type/predicate] clause of
+  @racket[require/typed].
+}
+
 @(close-eval the-eval)

typed-racket-lib/typed-racket/base-env/base-types-extra.rkt

@@ -20,7 +20,7 @@
 ;; special type names that are not bound to particular types
 (define-other-types
   -> ->* case-> U Union ∩ Intersection Rec All Opaque Immutable-Vector Mutable-Vector Vector
-  Parameterof List List* Class Object Row Unit Values AnyValues Instance Refinement
+  Parameterof List List* Class Object Row Unit Values AnyValues Instance Refinement Type/Predicate
   pred Struct Struct-Type Prefab PrefabTop Distinction Sequenceof Refine Self Imp)
 
 (define-other-props

typed-racket-lib/typed-racket/base-env/extra-env-lang.rkt

@@ -31,6 +31,7 @@
     #:attributes (form outer-form)
     (pattern :simple-clause)
     (pattern :opaque-clause)
+    (pattern :type/predicate-clause)
     (pattern :struct-clause))
 
   (define-syntax-class simple-clause
@@ -52,6 +53,19 @@
                                    (define-syntax type type-name-error)
                                    (provide type pred))))
 
+  (define-syntax-class type/predicate-clause
+    #:description "[#:type/predicate type pred]"
+    (pattern [#:type/predicate type:id pred:id]
+             #:with form
+             #'(begin
+                 (register-type (quote-syntax id)
+                                (asym-pred Univ B (-PS (-is-type 0 (make-Type/Predicate #'pred)) -tt)))
+                 (register-type-name (quote-syntax type)
+                                     (make-Type/Predicate #'pred)))
+             #:with outer-form #'(begin
+                                   (define-syntax type type-name-error)
+                                   (provide type pred))))
+
   (define-syntax-class struct-clause
     #:description "[#:struct name ([field : type] ...)]"
     ;; FIXME: support other struct options
@@ -100,7 +114,8 @@
                              typed-racket/env/global-env typed-racket/env/type-alias-env
                              typed-racket/types/struct-table typed-racket/types/abbrev
                              typed-racket/typecheck/tc-structs
-                             (only-in typed-racket/rep/type-rep make-Name make-Opaque)
+                             (only-in typed-racket/rep/type-rep make-Name make-Opaque
+                                      make-Type/Predicate)
                              (rename-in racket/private/sort [sort raw-sort]))
                     ;; FIXME: add a switch to turn contracts on for testing
                     binding.form ...)))

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

@@ -12,38 +12,44 @@
 ;;
 ;; - 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/predicate-type
          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/predicate-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 ...)
        (with-syntax ([(names ...) (generate-temporaries #'(id ...))])
          #'(begin (provide (rename-out [names id] ...))
                   (define-syntax (names stx) (id stx)) ...))]))
   (def require/opaque-type
+        require/predicate-type
         require-typed-signature
         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
@@ -166,10 +172,17 @@
     (pattern [(~or (~datum opaque) #:opaque) opaque ty:id pred:id #:name-exists]
              #:with opt #'(#:name-exists)))
 
+  (define-syntax-class type/predicate-clause
+    #:attributes (ty pred opt)
+    (pattern [#:type/predicate ty:id pred:id]
+             #:with opt #'()))
+
   (define-syntax-class (clause legacy unsafe? lib)
    #:attributes (spec)
    (pattern oc:opaque-clause #:attr spec
      #`(require/opaque-type oc.ty oc.pred #,lib #,@(if unsafe? #'(unsafe-kw) #'()) . oc.opt))
+   (pattern tpc:type/predicate-clause #:attr spec
+     #`(require/predicate-type tpc.ty tpc.pred #,lib #,@(if unsafe? #'(unsafe-kw) #'()) . tpc.opt))
    (pattern (~var strc (struct-clause legacy)) #:attr spec
      #`(require-typed-struct strc.nm (strc.tvar ...)
                              (strc.body ...) strc.constructor-parts ...
@@ -204,7 +217,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)
@@ -251,6 +264,11 @@
               (require/typed/provide lib other-clause ...))]
     [(_ lib (~and clause [#:opaque t:id pred:id])
         other-clause ...)
+     #'(begin (require/typed lib clause)
+              (provide t pred)
+              (require/typed/provide lib other-clause ...))]
+    [(_ lib (~and clause [#:type/predicate t:id pred:id])
+        other-clause ...)
      #'(begin (require/typed lib clause)
               (provide t pred)
               (require/typed/provide lib other-clause ...))]))
@@ -269,16 +287,22 @@
 ;; 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
-(define (make-contract-def-rhs/from-typed id flat? maker?)
+;; make-contract-def-rhs/from-typed : Id Boolean Boolean Boolean -> Syntax
+(define (make-contract-def-rhs/from-typed id flat? exact? maker?)
   (contract-def-property
    #'#f
    ;; This function should only be called after the type-checking pass has finished.
@@ -291,7 +315,7 @@
          (if types
              #`(U #,@types)
              #f)))
-     `#s(contract-def ,type-stx ,flat? ,maker? typed))))
+     `#s(contract-def ,type-stx ,flat? ,exact? ,maker? typed))))
 
 
 (define (define-predicate stx)
@@ -312,8 +336,9 @@
 (define (make-predicate stx)
   (syntax-parse stx
     [(_ ty:expr)
+     ; passing #t for exact? makes it error on Type/Predicate 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 +350,40 @@
      #`(#,(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 Type/Predicate types
+     (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,10 +408,10 @@
             #'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)))
+                                     (make-contract-def-rhs/from-typed existing-ty-id #f #f #f)))
             (define (store-existing-type existing-type)
               (check-no-free-vars existing-type #'v)
               (cast-table-add! existing-ty-id (datum->syntax #f existing-type #'v)))
@@ -408,6 +467,33 @@
                                    (any-wrap-warning/c . c-> . boolean?)))))
            #,(ignore #'(require/contract pred hidden pred-cnt lib)))))]))
 
+(define (require/predicate-type stx)
+  (define-syntax-class unsafe-id
+    (pattern (~literal unsafe-kw)))
+  (syntax-parse stx
+    [_ #:when (eq? 'module-begin (syntax-local-context))
+       ;; it would be inconvenient to find the correct #%module-begin here, so we rely on splicing
+       #`(begin #,stx (begin))]
+    [(_ ty:id pred:id lib (~optional unsafe:unsafe-id))
+     (with-syntax ([hidden (generate-temporary #'pred)])
+       ;; this is needed because this expands to the contract directly without
+       ;; going through the normal `make-contract-def-rhs` function.
+       (set-box! include-extra-requires? #t)
+       (quasisyntax/loc stx
+         (begin
+           ;; register the identifier for the top-level (see require/typed)
+           #,@(if (eq? (syntax-local-context) 'top-level)
+                  (list #'(define-syntaxes (hidden) (values)))
+                  null)
+           #,(internal #'(require/typed-internal hidden (Any -> Boolean : #:+ (Type/Predicate pred))))
+           #,(syntax/loc stx (define-type-alias ty (Type/Predicate pred)))
+           #,(if (attribute unsafe)
+                 (ignore #'(define pred-cnt any/c)) ; unsafe- shouldn't generate contracts
+                 (ignore #'(define pred-cnt
+                             (or/c struct-predicate-procedure?/c
+                                   (any-wrap-warning/c . c-> . boolean?)))))
+           #,(ignore #'(require/contract pred hidden pred-cnt lib)))))]))
+
 
 
 (module self-ctor racket/base

typed-racket-lib/typed-racket/env/init-envs.rkt

@@ -275,6 +275,8 @@
                 (list ,@(map type->sexp rands)))]
     [(Opaque: pred)
      `(make-Opaque (quote-syntax ,pred))]
+    [(Type/Predicate: pred)
+     `(make-Type/Predicate (quote-syntax ,pred))]
     [(Refinement: parent pred)
      `(make-Refinement ,(type->sexp parent) (quote-syntax ,pred))]
     [(Mu-maybe-name: n (? Type? b))

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

@@ -139,6 +139,7 @@
 (define-literal-syntax-class #:for-label Union)
 (define-literal-syntax-class #:for-label All)
 (define-literal-syntax-class #:for-label Opaque)
+(define-literal-syntax-class #:for-label Type/Predicate)
 (define-literal-syntax-class #:for-label Parameter)
 (define-literal-syntax-class #:for-label Immutable-Vector)
 (define-literal-syntax-class #:for-label Mutable-Vector)
@@ -789,6 +790,8 @@
        (parse-all-type stx)]
       [(:Opaque^ p?:id)
        (make-Opaque #'p?)]
+      [(:Type/Predicate^ p?:id)
+       (make-Type/Predicate #'p?)]
       [(:Distinction^ name:id unique-id:id rep-ty:expr)
        (-Distinction (syntax-e #'name) (syntax-e #'unique-id) (parse-type #'rep-ty))]
       [(:Parameter^ t)
@@ -1106,6 +1109,8 @@
           Err])]
       [(:Opaque^ . rest)
        (parse-error "bad syntax in Opaque")]
+      [(:Type/Predicate^ . rest)
+       (parse-error "bad syntax in Type/Predicate")]
       [(:U^ . rest)
        (parse-error "bad syntax in Union")]
       [(:Rec^ . rest)