I didn’t see mention of the verification being added to Racket, but even if it hasn’t been, I think that it could be added, via a library.

No, the compiler is currently not able to remove contract checks

Does the compiler only recognize runtime type tests that have been explicitly told to the compiler, perhaps in the form of a list of predicate functions provided by the core language? There is no way for the compiler to recognize a type predicate that myself write and use in my code?

Consider this program: #lang racket/base (struct p (x y)) (define (f p) (if (p? p) (p-x p) 1)) (if (even? (random 10)) (f (p 2 2)) (f (p 3 1))) That gets compiled to (if (even? (random 10)) 2 3). Is that what you mean?

@samth after CP0, there could be two variants of primitives: those prefixed with #2% and those prefixed with #3%. Do I understand correctly that #3% are the unsafe variant?

yes mostly. Here’s another scenario I’m thinking of (struct p (x y)) (define (f1 p) (if (p? p) (process (f2 p)) ; where process is a bunch of code surrounding (f2 p) 1)) (define (f2 p) (if (p? p) (p-x p) 'not-a-p)) (f1 p) does this get compiled to something like (process (p-x p))?

Is the compiler capable of looking through multiple function invocations and recognize that same predicate being used in the outermost function is also being used in inner functions and avoid those additional redundant predicate checks?

I think you meant (f1 (p ... ...)), right?

Otherwise, that just evaluates to 1

yes I meant to say (f1 (p 4 5))

so this means (process (f2 p)) gets compiled to (process 4) or (process (p-x p)) depending on how sophisticated it is

For a program:

#lang racket/base (struct p (x y)) (define (f1 p) (if (p? p) (println (f2 p)) 1)) (define (f2 p) (if (p? p) (p-x p) 'not-a-p)) (f1 (p 4 5)) Here’s the compilation result:

(call-with-module-prompt (letrec ([procz1 (lambda () (println3 4))]) (lambda () (#%call-with-values procz1 print-values4))))

nice!

here’s another slightly modified scenario which really accurately captures what I’m actually thinking about

``````

(struct p (x y)) (define (my-p? p) (and (equals? (p-x p) 'x-value) (equals (p-y p) 'y-value))) (define (f1 p) (if (my-p? p) (process (f2 p)) ; where process is a bunch of code surrounding (f2 p) 1)) (define (f2 p) (if (my-p? p) (p-x p) 'not-a-valid-p)) (f1 (p 'x-value 'y-value))

does this get compiled to (process 'x-value)

Yes

cool

I think there are two separate things though

what is that?

For concrete inputs, it’s not surprising that the partial evaluator could optimize the program like that. That’s just inlining.

The original topic of this thread is about symbolic inputs. Like, if you have:

(define (f x) (car x) (cdr x)) and there’s no call to f at all. In this case, x is not concrete.

The question is, will there be redundant check that x is a pair when it calls cdr.

For that program, the redundant check is eliminated.

For a more complicated program, consider: #lang racket/base (struct p (x y) ) (define (f p) (if (p? p) (+ (p-x p) (p-y p) ) (void)))

In that program, the redundant p? checks are not eliminated, because of the possibility of impersonators. If you add #:authentic to the struct, then the redundant checks go away.

gotcha, often I write functions which process datatypes and turns out it’s convenient to reuse some functions within other functions which also check for and process the same datatype so there end up being layers of redundant checks being performed by the functions. I often wondered whether the compiler and the runtime system were smart enough to eliminate those checks. My takeaway is yes in certain cases but as things get complicated that isn’t necessarily true.

But this isn’t something I worry about, it’s not a performance issue for me, more of an intellectual itch I’ve been meaning to scratch

decided to make good use of the new and shiny github discussions feature by opening a can of typed racket worms https://github.com/racket/typed-racket/discussions/1004