Managing `cast` performance penalty

Questions & Answers
,
1

Hi,

After putting cast here and there in my Typed Racket code, I got curious to know how much it cost me in terms of runtime performance:

#lang typed/racket

(time (for ([i (in-range 10000)])
        (+ 1 i)))

(time (for ([i (in-range 10000)])
        (+ 1 (cast i Integer))))

cpu time: 0 real time: 0 gc time: 0
cpu time: 18 real time: 18 gc time: 2

Oh. It actually tends to get somewhat worse when I reload the same code multiple times (tested mainly in Racket Mode, but also in DrRacket):

cpu time: 0 real time: 0 gc time: 0
cpu time: 18 real time: 18 gc time: 2
> 
cpu time: 0 real time: 0 gc time: 0
cpu time: 20 real time: 20 gc time: 3
> 
cpu time: 0 real time: 0 gc time: 0
cpu time: 35 real time: 35 gc time: 18
> 
cpu time: 0 real time: 0 gc time: 0
cpu time: 39 real time: 39 gc time: 22
> 
cpu time: 0 real time: 0 gc time: 0
cpu time: 69 real time: 69 gc time: 51
> 
cpu time: 0 real time: 0 gc time: 0
cpu time: 28 real time: 28 gc time: 12
> 
cpu time: 0 real time: 0 gc time: 0
cpu time: 20 real time: 20 gc time: 3
> 
cpu time: 0 real time: 0 gc time: 0
cpu time: 26 real time: 26 gc time: 8

Well, the docs did tell me that:

The value is actually protected with two contracts. The second contract checks the new type, but the first contract is put there to enforce the old type, to protect higher-order uses of the value.

As I understand it, the performance penalty is therefore the effect of the contracts cast imposes.

Is there a way to manage the performance penalty of cast?

I find myself doing lots of conversions between Integer and Positive-Integer or Nonnegative-Integer, and I am getting vaguely worried.

1 Like
2

Maybe waiting for Shallow typed racket?

2 Likes
3

Woow, I watched Racket Con 2020 : Shallow Typed Racket - YouTube and it got me really interested!

Quite excited to see that @ben_greenman has done some recent and huge work on the related PR. I realize that shallow types do not fit all situations, but I'll be watching this work closely.

Thank you @dannypsnl for the pointer!

2 Likes
4

if you wanted downcasting, I would recommend type predicates.

(time (for ([i (in-range 10000)])
        (+ 1 i)))

(time (for ([i (in-range 10000)])
        (+ 1 (if (integer? i) i
                   (error 'hi)))))

output:

cpu time: 0 real time: 0 gc time: 0
cpu time: 0 real time: 0 gc time: 0
2 Likes
5

I would say that cast in Typed Racket is very rarely the right construct. I would take a look at assert, which encapsulates the pattern @capfredf suggested. In some cases ann and the #{e :: t} reader syntax have also been useful for people who thought they needed cast.

I can think of two main cases when cast is a good choice:

  1. When you are dealing with a higher-order or mutable type that can't be fully verified by a flat predicate; and
  2. When you are receiving some structured data with a type like Any and the contract system's good error messages are worth the cost of a one-time cast at the boundary crossing.

By far the main way I use cast in practice is to promote the result of read or fasl->sexp. Even then, though, I'll more often use require/typed to import the function in question with a type-specific name and contract.

3 Likes
6

I am not a heavy typed racket user, so I don't really know.
But your solution looks to me, what I would call an assert and looking at the docs I saw there is an assert in typed racket.

So my question is, is that assert the idiomatic way to do something similar in typed racket?
I guess @LiberalArtist answered my question. (yes)

7

I ... don't suppose there's an existing categorization that would allow certain uses of cast to be automatically replaced with asserts, is there? I can see that just providing a special list for this one optimization would be fragile, but if there's an existing lists somewhere of flat-checkable-types, would it not make sense to rewrite casts as asserts? There must be something wrong with this proposal, but I don't know what it is.

1 Like
8

(assert v p) roughly expands to (if (p v) v (error ...)

3 Likes
9

Mostly I recommend using cast only as a last resort. Typically you can add a dynamic check using occurrence typing and then specify your own error behavior. If you don't want that control the assert function is the next best choice. Only if those don't work would I use cast.

5 Likes
10

It might be worth elaborating on this in the docs for cast: it looks like they don't even link to assert, which is (reasonably) relegated to the "Utilities" section. I know this has come up before, perhaps for people familiar with languages where cast is a more frequently useful operation.

3 Likes
11

I don’t know this stuff enough to do my own pull request to update the docs, but I’ve done the odd one before and would be happy to help if you know what you want to write?

1 Like
12

Thanks a lot for your answers everyone! I have been looking at the 5 Occurrence Typing section in the Typed Racket reference for a couple years now, and have been wondering how on earth I managed to go around without using this feature, which is "One of Typed Racket’s distinguishing type system features." Well, I have my answer now :smiley: The best news is that I totally understand your examples and the usefulness of occurrence typing, for the first time ever!

I managed to completely convert all casts in my code to asserts, and it works like a charm. I have also just submitted a PR to Typed Racket (thanks @spdegabrielle for pointing the location!) to mention assert, occurrence typing, and ann in the docs of cast: Mention assert and ann in the docs of cast. by scolobb · Pull Request #1231 · racket/typed-racket · GitHub .

While converting casts to asserts, I found myself quite often using assert in conjuction with make-predicate, like so:

(assert (modulo (+ x y) 2) (make-predicate (U Zero One)))

So I made myself a little macro:

(define-syntax-parse-rule (assert-type e:expr type:expr)
  (assert e (make-predicate type)))

which is used like this

(assert-type (modulo (+ x y) 2) (U Zero One))

Does that ring any bells? Like, do I miss an existing pattern already captured by a definition in Typed Racket, or is my macro somehow bad?

In what concerns ann and the #{ e :: t } reader extension, I frankly haven't yet found a use for them. I always write type annotations for top-level definitions, and Typed Racket is clever enough to figure out the types of the values in the definitions from that. Sometimes I need to incorporate some additional knowledge which is not directly derivable from the top-level types, and in these cases assert and cast do a good job, but ann is too weak, e.g.:

> (define x : Any 1)
> (cast x Integer)
- : Integer
1
> (assert x (make-predicate Integer))
- : Integer
1
> (ann x Integer)
; tmp.rkt/cast-example:42:5: Type Checker: type mismatch
;   expected: Integer
;   given: Any
;   in: x

Actually, I have even been wondering out of curiosity as to why there is a reader extension for ann specifically, but not for cast or assert.

4 Likes
13

Well, I usually use ann to annotate the type of lambda, and use reader extension to declare the type matched by match.

For example:

> (map (ann (lambda (x) (symbol->string x)) (-> Symbol String)) '(a b c d))
- : (Pairof String (Listof String))
'("a" "b" "c" "d")

and here is an example from guide 3.1.4:

(: assert-symbols! ((Listof Any) -> (Listof Symbol)))
(define (assert-symbols! lst)
  (match lst
    [(list (? symbol? #{s : (Listof Symbol)}) ...) s]
    [_ (error "expected only symbols, given" lst)]))
2 Likes
14

Thank you @NoahStoryM, these examples are illustrative and useful to me.

15

I keep trying to adopt this path, and then I find parts of it that just don't seem to work. Consider this example:

#lang typed/racket

(: parse-let (Sexp -> (List (Listof Symbol)
                            (Listof Sexp)
                            Sexp)))
(define (parse-let lst)
  (match lst
    [(list 'let
           (list (? symbol? #{s : (Listof Symbol)})
                 '=
                 #{val : (Listof Sexp)})
           ...
           'in
           body)
     (list s val body)]
    [_ (error "expected only symbols, given" lst)]))

in 8.4.900, this signals the errors

Type Checker: type mismatch
  expected: (Listof Symbol)
  given: (Listof Any) in: (match lst ((list (quote let) (list (? symbol? s) (quote =) val) ... (quote in) body) (list s val body)) (_ (error "expected only symbols, given" lst)))
. Type Checker: type mismatch
  expected: (Listof Sexp)
  given: (Listof Any) in: (match lst ((list (quote let) (list (? symbol? s) (quote =) val) ... (quote in) body) (list s val body)) (_ (error "expected only symbols, given" lst)))

... even though mousing over the identifier 's' shows it to have type (Listof Symbol). My impression is that TR just gives up when the match becomes of sufficient complexity, which makes it hard to recommend this for students.

Am I missing something?

1 Like
16

Yes, I'm also impressed that match is so complicated that it becomes very difficult to directly annotate the type of the matched variable. This is why I basically only use #:when style now (as we discussed in Is it good style to use `#:when` instead of `?` in match expression?).

And in TR, match seems not to design a syntax for declaring types, types can only be declared through reader extension (although I rarely do this, but I think this is at least an example to illustrate the use of reader extension)

2 Likes
17

The short answer is that using ... in match when it is not the end of the list generates much more complex code, which TR doesn't understand. There is not a "give-up" threshold in any of these systems, just sometimes the output of macros is too hard to automatically infer the types.

Note that if you change this to more like Racket's syntax, with the bindings in a list, it typechecks fine.

1 Like
18

Oh! Interesting. I should add "dots-not-at-the-end" to my list of things that substantially complicate the process of matching; that makes perfect sense.

19

Many thanks for reminding me of this. This is so close to working in my classroom... but now I have a teeny tiny different problem. Consider this code:

#lang typed/racket

(: sexp? (Any -> Boolean : #:+ Sexp))
(define (sexp? s)
  (symbol? s))


(define (only-sexps [f : Any]) : Sexp
  (cond [(sexp? f) f]
        [else '(oops)]))

(: parse-let (Sexp -> (List (Listof Symbol)
                            (Listof Sexp)
                            Sexp)))


(define (parse-let lst)
  (match lst
    [(list 'let
           (list s '= val)
           ...
           'in
           body)
     #:when (and (andmap symbol? s)
                 (andmap sexp? val)) 
     (list s val body)]
    [_ (error "whatever")]))

Now, the type of s works perfectly, and it seems that TR can assign it the type Symbol. Unfortunately, Sexp is not a simple type, it requires a chaperone (apologies if I'm saying that incorrectly), so there's no flat sexp? check. 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?, but as 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?'. Again, I'd love to be wrong....

1 Like
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.