Managing `cast` performance penalty

Questions & Answers
,
20

this example shows (with a very very restrictive "sexp?" that actually only greenlights symbols), user-defined predicates don't seem to work in the same way as built-in ones like 'symbol?'.

I think the problem that your sexp? can't work like symbol? may be related to andmap.

Welcome to Racket v8.4 [cs].
> (: sexp? (Any -> Boolean : #:+ Sexp))
> (define (sexp? s) (symbol? s))
> (: sexps? ((Listof Any) -> Boolean : #:+ (Listof Sexp)))
> (define (sexps? s) ((inst andmap Any Boolean Sexp) sexp? s))
string:1:19: Type Checker: type mismatch;
 mismatch in proposition
  expected: ((: s (Listof Sexp)) | Top)
  given: (Top | Top)
  in: ((inst andmap Any Boolean Sexp) sexp? s)
 [,bt for context]
>

TR seems to have special handling for the type of andmap, for example, we can define listof? directly through andmap:

Welcome to Racket v8.4 [cs].
> (: listof? (All (A) (case-> [-> (pred A) (pred (Listof A))]
                              [-> [-> Any Boolean] [-> Any Boolean]])))
> (define listof?
    (λ (pred)
      (λ (arg)
        (and (list? arg)
             (andmap pred arg)))))
> (:print-type listof?)
(All (A)
  (case->
   (-> (-> Any Boolean : A) (-> Any Boolean : (Listof A)))
   (-> (-> Any Boolean) (-> Any Boolean))))
> (:print-type andmap)
(All (a c d b ...)
  (case->
   (-> (-> a c : d) (Listof a) c)
   (-> (-> a b ... b c) (Listof a) (Listof b) ... b (U True c))))
>

But if we manually retype andmap, this code will throw an error:

Welcome to Racket v8.4 [cs].
> (require typed/racket/unsafe)
> (unsafe-require/typed racket/base
    [andmap
     (All (a c d b ...)
          (case->
           (-> (-> a c : d) (Listof a) c)
           (-> (-> a b ... b c) (Listof a) (Listof b) ... b (U True c))))])
> (: listof? (All (A) (case-> [-> (pred A) (pred (Listof A))]
                              [-> [-> Any Boolean] [-> Any Boolean]])))
> (define listof?
    (λ (pred)
      (λ (arg)
        (and (list? arg)
             (andmap pred arg)))))
string:5:11: Type Checker: Polymorphic function `andmap2' could not be applied to arguments:
Types: (-> a c : d) (Listof a)  -> c
       (-> a b ... b c) (Listof a) (Listof b) ... b -> (U True c)
Arguments: (-> Any Boolean : A) (Listof Any)
Expected result: Boolean
  in: (andmap pred arg)
 [,bt for context]
> (:print-type andmap)
(All (a c d b ...)
  (case->
   (-> (-> a c : d) (Listof a) c)
   (-> (-> a b ... b c) (Listof a) (Listof b) ... b (U True c))))
>

In my case, I don't care about fancy things, I only want (what I believe to be) some pretty simple things, so I can possibly "roll my own" sexp?

I don't think there's a safe way to implement sexp? in TR (and I'm not sure why you want only greenlights symbols predicates), I wonder if this weaker sexp? can solve the problem you met?

(define-type S-Exp (U Boolean Real Char String Bytes
                      Keyword Symbol (Listof S-Exp)))
(define-predicate sexp? S-Exp)

it requires a chaperone (apologies if I'm saying that incorrectly), so there's no flat sexp? check.

When I want to deal with mutable types, I'm always frustrated that I can't refine their types through predicates. But I thought before that maybe we could tag these non-flat values through contract and then get their original type information (see [Feature Request] Tag Contract and Tag Type - #3 by NoahStoryM).

I don't know much about the specific implementation of contract and type, so I'm not sure whether tag type is feasible or not, hope this idea can help you.