order-of-evaluation props

rfcs/0003-app-order.md

@@ -0,0 +1,100 @@
+- Feature Name: Use left-to-right application order with occurrence typing
+- Start Date: 2018-05-02
+- RFC PR: (leave this empty)
+- Feature Commit(s): (leave this empty)
+
+# Summary
+
+When typechecking a function application `(f e_0 ... e_n)`:
+
+- use the unconditional props from `f` to type-check `e_0`
+- use the unconditional props from `e_0` to type-check `e_1`
+- ... and so on
+
+# Motivation
+
+The Typed Racket type checker is flow-sensitive in some ways.
+
+- for an if-statement `(if e_0 e_1 e_2)`, the result of type-checking `e_0`
+  is used to type check `e_1` and `e_2` with refined type environments
+- for a sequence `(begin e_0 e_1)`, the result of type-checking `e_0`
+  is used to refine the environment for type-checking `e_1`
+
+This flow sensitivity is sound because it matches Racket's order of evaluation.
+For example in `(begin e_0 e_1)`, the expression `e_1` is only evaluated after
+the expression `e_0`.
+
+Typed Racket is not currently flow-sensitive for function applications, even
+though Racket guarantees left-to-right evaluation (Racket Reference, Sec 3.7).
+For example:
+
+```
+#lang typed/racket
+
+;; This expression type-checks, because TR is flow-sensitive for `begin`
+(lambda ((x : Any))
+  (begin
+    (assert x integer?)
+    (+ x x)))
+
+;; This similar expression does NOT type-check, because TR doesn't know the
+;;  second `x` has type `integer?`
+(lambda ((x : Any))
+  (+ (begin (assert x integer?) x)
+     x))
+```
+
+
+# Guide-level explanation
+
+The Typed Racket type checker includes some basic flow sensitivity:
+
+- when type-checking a sequence of expressions, e.g. `(begin e_0 e_n)`, TR
+  uses the result of checking `e_0` to type-check `e_1`
+- when type-checking a function application, e.g. `(e_0 e_1)`, TR uses the result
+  of type-checking the function expression `e_0` to type-check the argument
+  expression `e_1`
+
+<!-- Explain the proposal as if it was already included in the language and you were -->
+<!-- teaching it to another Typed Racket programmer. That generally means: -->
+<!--  -->
+<!-- - Introducing new named concepts. -->
+<!-- - Explaining the feature largely in terms of examples. -->
+<!-- - Explaining how Typed Racket programmers should *think* about the feature. -->
+<!--  -->
+<!-- For implementation-oriented RFCs (e.g. for type checker internals), focus on how -->
+<!-- type system contributors should think about the change, and give examples of its -->
+<!-- concrete impact. -->
+<!--  -->
+<!-- # Reference-level explanation -->
+<!--  -->
+<!-- Explain the design in sufficient detail that: -->
+<!--  -->
+<!-- - Its interaction with other features is clear. -->
+<!-- - It is reasonably clear how the feature would be implemented. -->
+<!-- - Corner cases are dissected by example. -->
+<!--  -->
+<!-- Return to the examples given in the previous section, and explain more fully how -->
+<!-- the detailed proposal makes those examples work. -->
+<!--  -->
+<!-- # Drawbacks and Alternatives -->
+<!-- [drawbacks]: #drawbacks -->
+<!--  -->
+<!-- Why should we *not* do this? Could we do something else instead? -->
+<!--  -->
+<!-- # Prior art -->
+<!-- [prior-art]: #prior-art -->
+<!--  -->
+<!-- Discuss prior art, both the good and the bad, in relation to this proposal. -->
+<!-- A few examples of what this can include are: -->
+<!--  -->
+<!-- - Does this feature exist in other programming languages and what experience have their community had? -->
+<!-- - Papers: Are there published papers, books, great blog posts, etc that discuss this? Be _specific_! -->
+<!--  -->
+<!--  -->
+<!-- # Unresolved questions -->
+<!-- [unresolved]: #unresolved-questions -->
+<!--  -->
+<!-- - What parts of the design do you expect to resolve through the RFC process before this gets merged? -->
+<!-- - What parts of the design do you expect to resolve through the implementation of this feature before stabilization? -->
+<!-- - What related issues do you consider out of scope for this RFC that could be addressed in the future independently of the solution that comes out of this RFC? -->

typed-racket-lib/typed-racket/typecheck/signatures.rkt

@@ -14,6 +14,7 @@
    [cond-contracted tc-body/check (syntax? (or/c tc-results/c #f) . -> . full-tc-results/c)]
    [cond-contracted tc-expr/t (syntax? . -> . Type?)]
    [cond-contracted single-value ((syntax?) ((or/c tc-results/c #f)) . ->* . full-tc-results/c)]
+   [cond-contracted map-single-value/unconditional-prop (((listof syntax?)) ((listof Prop?)) . ->* . (listof full-tc-results/c))]
    [cond-contracted tc-dep-fun-arg ((syntax?) ((or/c tc-results/c #f)) . ->* . full-tc-results/c)]))
 
 (define-signature check-subforms^

typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-main.rkt

@@ -9,7 +9,7 @@
          "../signatures.rkt" "../tc-funapp.rkt"
          (types abbrev utils prop-ops)
          (env lexical-env)
-         (typecheck tc-subst tc-envops check-below)
+         (typecheck tc-subst tc-envops check-below tc-metafunctions)
          (rep type-rep prop-rep object-rep values-rep))
 
 (import tc-expr^ tc-app-keywords^
@@ -75,8 +75,10 @@
 (define (tc/app-regular form expected)
   (syntax-case form ()
     [(f . args)
-     (let ([f-ty (tc-expr/t #'f)]
-           [args* (syntax->list #'args)])
+     (let* ([f-res (single-value #'f)]
+            [f-ty (match f-res [(tc-result1: t _ _) t])]
+            [f-prop (unconditional-prop f-res)]
+            [args* (syntax->list #'args)])
        (define (matching-arities arrs)
          (for/list ([arr (in-list arrs)] #:when (arrow-matches? arr args*)) arr))
        (define (has-drest/props? arrs)
@@ -89,7 +91,8 @@
             (cond
               [(with-refinements?)
                (map tc-dep-fun-arg args*)]
-              [else (map single-value args*)]))
+              [else
+               (map-single-value/unconditional-prop args* f-prop)]))
           (tc/funapp #'f #'args f-ty arg-types expected)]
          [(or (? DepFun?)
               (Poly-unsafe: _ (? DepFun?)))
@@ -111,5 +114,5 @@
                  (single-value arg-stx (ret dom-ty))]
                 [else (single-value arg-stx)])))
           (tc/funapp #'f #'args f-ty arg-types expected)]
-         [_ (tc/funapp #'f #'args f-ty (map single-value args*) expected)]))]))
+         [_ (tc/funapp #'f #'args f-ty (map-single-value/unconditional-prop args* f-prop) expected)]))]))
 

typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt

@@ -16,7 +16,7 @@
          racket/list
          racket/private/class-internal
          syntax/parse
-         (typecheck internal-forms tc-envops)
+         (typecheck internal-forms tc-envops tc-metafunctions)
          racket/sequence
          racket/extflonum
          ;; Needed for current implementation of typechecking letrec-syntax+values
@@ -355,6 +355,25 @@
           #:stx form
           "expected single value, got multiple (or zero) values")]))
 
+;; Apply `single-value` to a list of forms in order, accumulate the prop info
+(define (map-single-value/unconditional-prop forms [prop -tt])
+  (define any-res (-tc-any-results #f))
+  (let loop ((forms forms)
+             (prop prop))
+    (match forms
+     ['()
+      '()]
+     [(cons e rst)
+      (define tcr
+        (with-lexical-env+props
+          (list prop)
+          #:expected any-res
+          #:unreachable (for-each register-ignored! rst)
+          (single-value e)))
+      (define prop+
+        (-and (unconditional-prop tcr) prop))
+      (cons tcr (loop rst prop+))])))
+
 (define (tc-dep-fun-arg form [expected #f])
   (define t (tc-expr/check form expected #t))
   (match t

typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt

@@ -13,7 +13,8 @@
          combine-props
          merge-tc-results
          tc-results->values
-         erase-existentials)
+         erase-existentials
+         unconditional-prop)
 
 ;; Objects representing the rest argument are currently not supported
 (define/cond-contract (abstract-results results arg-names #:rest-id [rest-id #f])

typed-racket-test/unit-tests/typecheck-tests.rkt

@@ -4712,6 +4712,14 @@
           (void))
         #:ret (ret -Void #f #f)
         #:msg #rx"Bad arguments to function"]
+
+       ;; props + evaluation order
+       [tc-e ((lambda: ((x : (Un Symbol Natural))) (+ (assert x integer?) x)) 1) -Nat]
+       [tc-e ((lambda: ((x : (Un Symbol Natural))) ((begin (assert x integer?) +) x x)) 1) -Nat]
+       [tc-e ((lambda: ((x : (Un Symbol Natural)) (y : (Un Symbol Natural)))
+                (+ (assert x integer?) (assert y integer?) (+ x y))) 1 2) -Nat]
+       ;; TODO
+       ;;[tc-e ((lambda: ((x : Symbol)) (void (assert x string?) (+ x 1))) 'A) -Nat]
        )
 
   (test-suite