Evaluation order rfc

[bennn]

RFC for #707

Goals:

• identify all kinds of function applications in Typed Racket (applying a normal function, applying a dependent function, the special cases in typecheck/tc-app/*)
• have a complete RFC

[MichaelBurge]

Should evaluation order affect typechecking?

In the expression

(+ x (begin (assert x integer?) x))

the right-hand x is known to be an integer. But the left-hand x is the same x: Since all arguments are evaluated before the function is invoked, it shouldn't be unsound if earlier arguments are accepted on the basis of later arguments passing their runtime checks.

Do we want the union of all propositions to apply to each argument?

Probably not - if the left-hand x is changed to (f x) for some f expecting an integer?, then it would be unsound. So it would only help in the cases where a variable is passed unmodified to the function application. Although that does make me wonder if asserts should be pushed to the beginning of the scope.

[bennn]

Do we want the union of all propositions to apply to each argument?

No, because that could be unsound. In this application, we don't want to check the 1st argument to + assuming that x is an integer:

(+ (add1 x) (begin (assert x integer?) x))

I think we need to conservatively reject your example.

[pnwamk]

Would it be helpful to describe this as checking function application in terms of its equivalent expansion into A-normal form to help with intuition as for why it works and is correct?

i.e. we're basically leveraging the fact that checking this program:

(fun arg1 arg2 ...)

is equivalent to checking this one:

(let* ([x1 arg1]
       [x2 arg2]
       ...)
  (fun x1 x2 ...))

(where the x's are fresh) because of how function application is defined in Racket. (I know that the let* could have been a let but perhaps the * helps emphasize the necessary ordering of argument evaluation for people who haven't realized let also guarantees in-order evaluation in Racket)