order-of-evaluation props

[bennn]

Use props from checking a function to check its first argument, use props from checking the first argument to check the second, and so on.

Makes things like this type check: (lambda: ((x : (Un Symbol Natural))) (+ (assert x integer?) x))

---

TODO:

• [ ] add test where some arguments are unreachable
• [ ] accumulate props in tc-app-main on L91 L97 L98
• [ ] add test to show its a good idea to accumulate props even when the arguments have expected types
• [ ] stop extracting props from argument twice
• [ ] finish the RFC
• [ ] measure performance (using the pnwamk/tr-performance repo)
• [ ] see about accumulating props in the special tc-app cases (for values, vector-ref, etc.)

[pnwamk]

Questions:

1. Are there any downsides to doing this? The only possible conflict I can think of is that dependent function types allow arguments to depend on each other in any order (not in a fixed left to right order) and you may want to check those in that particular order... I'm not sure if/how these features would interact. Maybe we should add a check that the function is not a dependent function to be safe?

2. Does this affect performance at all? It seems like it probably wouldn't for most programs (most arguments don't have interesting propositions, right?) but it would be nice to double check w/ some numbers just so we know.

[pnwamk]

I like this PR -- I'm a little nervous because we could clearly never "undo" it so we need to make sure we feel like we've considered all the possible repercussions.

[samth]

I think this is something that would benefit from writing down the RFC as part of this process.

[bennn]

@pnwamk re 1. I don't think these changes affect dependent functions; looks like tc-app-main.rkt handles those (DepFun?) in a separate branch. BUT I think it would be safe to apply "this change" to applications of dependent functions as long as those still evaluate their arguments left-to-right

[pnwamk]

I think it might be useful to have the RFC be it's own pull request. That way we can agree on the idea itself separate from the work to implement, merge the RFC when it's ready, and then we can focus on working together to get this PR done and in sync with the RFC.

[bennn]

This program came up last year (on Discord?) and has exactly the same problem: ((get-foo a1) a1) is checking and using a1 is the same expression.

#lang typed/racket

(provide num/foo foo-get num Num)



(: prop:foo (Struct-Property (-> Self Number)))

(: foo-pred (-> Any Boolean : (Has-Struct-Property prop:foo)))

(: foo-get (-> (Has-Struct-Property prop:foo)

               (Some (X)

                     (-> X Number)

                     : #:+ X)))

(define-values (prop:foo foo-pred foo-get)

  (make-struct-type-property 'foo))



(struct num ([n : Number])

  #:type-name Num

  #:property prop:foo

  (lambda ([me : Num])

          : Number

    (num-n me)))



(: num/foo Number)

(define num/foo

  (let ([a1 : Num

            (num 42)])

    ((foo-get a1) a1)))



(module+ test

  (require typed/rackunit)

  ;; succeeds

  (check-equal? num/foo 42))



;; However adding the following inline test for the body of num/foo as follows:

;; 
;; 
;; (module+ test
;; 
;;   (check-equal?
;; 
;;    (ann
;; 
;;     (let ([a1 : Num
;; 
;;               (num 42)])
;; 
;;       ((foo-get a1) a1))
;; 
;;     Number)
;; 
;;    42))
;; 
;; 
;; 
;; Results in the following type error
;; 
;; 
;; 
;; Type Checker: type mismatch
;; 
;;   expected: (B 0)
;; 
;;   given: Num
;; 
;;   in: a1