Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP

Loading…

Tr letrec values #372

Closed
wants to merge 2 commits into from

3 participants

@takikawa

This pull request is for code review.

This fixes PR 13124 by allowing letrec-values clauses that don't refer to the bound variables in the RHS to type-check with synthesized types no matter the order in which they appear.

Sam was concerned about interaction with control operators, but I think it's not an issue here. In order for a control operator to observe the mutation in the letrec, it would need to use a reference in the RHS to a letrec-bound variable. Since the first pass ignores such clauses, it should be fine.

Note: all the tests pass, except for the 6 unit tests that are still broken from the pkg reorganization.

@endobson

Why is this the right fix? Doesn't this just make the problematic code path not get triggered? I.e. the undefined getting added to the type still happens in the complicated cases.

@takikawa

This PR doesn't intend to reduce the conservative-ness of the typechecker with regard to #<undefined> (that's also a futile thing to do anyway; at some point in the future TR won't need to deal with #<undefined>s).

The bug that it's addressing is that the typechecker already looks for clauses where the RHS doesn't refer to a bound variable and checks those even without an annotation. This only works for certain orderings of clauses, however, and the attached commit makes annotations unnecessary no matter the order.

@endobson

I agree that you are fixing a bug, I'm just not sure that it is fixing the bug reported as pr 13124. I believe that the following program

#lang typed/racket

(: foo (-> Integer))
(define (foo)
  (: bn (Integer -> Integer))
  (define (bn n) (if (= n 0) 1 (bn (- n 1))))
  (define v (bn 0))
  0)

Is the same bug as PR 13124, and your change doesn't fix this program. I also think that a fix to that will obsolete the change that you are introducing here.

@takikawa

I agree that the typechecker could be even smarter. In particular, it can use Tarjan's algorithm to see which variables don't create cycles and type-check those in reverse topological order (that would make your example typecheck). This PR just solves a subset of the more general problem because I don't have more time to spend on it ATM, but I could add a TODO comment outlining how to do better.

@samth
Collaborator

How much of this would go away if we didn't have undefined?

@takikawa

This particular code is still relevant after removing #<undefined>. The point of this first pass is to find clauses that aren't recursive or mutually recursive for sure. Recursive clauses require a type annotation in order to close the loop (type synthesis doesn't work). The non-recursive clauses can be type-checked without an annotation.

@endobson
@samth samth was assigned
@samth
Collaborator

Coming back to this after a while, I'd like to get this merged, but I'd also like to understand @shekari's last suggestion better. Can you explain it further?

@endobson

My point was that the algorithim as currently written is fairly complicated and I saw a way of cleaning it up.

@takikawa is not changing the actual checking code, just the order in which bindings are being looked at, and I had shown an example where the new order is still not sufficient. I'm suggesting we have two parts one to determine the order and one to check in that order. That makes it so that changing to tarjan's algorithm or something doesn't need to touch the checking code.

takikawa added some commits
@takikawa takikawa Improve letrec-values type-checking
Split into two passes in order to be able to find
more cases where the RHS doesn't refer to the bindings
in the letrec.

Closes PR 13124
818d566
@takikawa takikawa [fixup] split up the implementation into several pieces
This follows the PR feedback from Eric
d914e48
@takikawa

I finally got around to addressing @shekari's comments for this PR. The latest commit separates the code that generates the list of non-recursive clauses to check, the actual checking code, and the 2nd pass that remains the same as before.

To replace the algorithm with a better one that uses Tarjan's algorithm, only one function should need modification if I set things up correctly. (and once the other PR that has an implementation of Tarjan's algorithm is merged, we could do this)

@samth
Collaborator

@takikawa, do you plan to use the Tarjan's algorithm implementation here from #570?

@takikawa

@samth yes, that's the plan. I'll extract out the algorithm into a utility module and generalize it a bit.

@takikawa

Now merged, with cycle detection. Thanks for the feedback.

@takikawa takikawa closed this
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Commits on Mar 4, 2014
  1. @takikawa

    Improve letrec-values type-checking

    takikawa authored
    Split into two passes in order to be able to find
    more cases where the RHS doesn't refer to the bindings
    in the letrec.
    
    Closes PR 13124
  2. @takikawa

    [fixup] split up the implementation into several pieces

    takikawa authored
    This follows the PR feedback from Eric
This page is out of date. Refresh to see the latest.
View
93 pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
@@ -116,31 +116,39 @@
[(var) (add-scoped-tvars b (lookup-scoped-tvars #'var))]
[_ (void)]))
- (let loop ([names names] [exprs exprs] [flat-names orig-flat-names] [clauses clauses])
+ ;; First look at the clauses that do not bind the letrec names
+ (define all-clauses
+ (for/list ([name-lst names] [expr exprs] [clause clauses])
+ (lr-clause name-lst expr clause)))
+
+ (define-values (ordered-clauses remaining)
+ (get-non-recursive-clauses all-clauses orig-flat-names))
+
+ (define-values (remaining-names remaining-exprs remaining-clauses)
+ (for/lists (_1 _2 _3) ([remaining-clause remaining])
+ (match-define (lr-clause name expr clause) remaining-clause)
+ (values name expr clause)))
+
+ ;; Check those and gather an environment for use below
+ (define-values (env-names env-types)
+ (check-non-recursive-clauses ordered-clauses))
+
+ (with-lexical-env/extend env-names env-types
(cond
;; after everything, check the body expressions
- [(null? names)
+ [(null? remaining-names)
(do-check void null null null form null body null expected #:abstract orig-flat-names)]
- ;; if none of the names bound in the letrec are free vars of this rhs
- [(not (ormap (lambda (n) (member n flat-names bound-identifier=?))
- (free-vars (car exprs))))
- ;; then check this expression separately
- (with-lexical-env/extend
- (list (car names))
- (list (match (get-type/infer (car names) (car exprs) (lambda (e) (tc-expr/maybe-expected/t e (car names)))
- tc-expr/check)
- [(tc-results: ts) ts]))
- (loop (cdr names) (cdr exprs) (apply append (cdr names)) (cdr clauses)))]
[else
+ (define flat-names (apply append remaining-names))
(do-check (lambda (stx e t) (tc-expr/check e t))
- names
+ remaining-names
;; compute set of variables that can't be undefined. see below.
(let-values
([(safe-bindings _)
(for/fold ([safe-bindings '()] ; includes transitively-safe
[transitively-safe-bindings '()])
- ([names (in-list names)]
- [clause (in-list clauses)])
+ ([names (in-list remaining-names)]
+ [clause (in-list remaining-clauses)])
(case (safe-letrec-values-clause? clause transitively-safe-bindings flat-names)
;; transitively safe -> safe to mention in a subsequent rhs
[(transitively-safe) (values (append names safe-bindings)
@@ -156,10 +164,59 @@
l)
types-from-user
(map (λ (x) (Un x -Undefined)) types-from-user)))))
- names))
+ remaining-names))
;; types the user gave. check against that to error if we could get undefined
- (map (λ (l) (ret (map get-type l))) names)
- form exprs body clauses expected)]))))
+ (map (λ (l) (ret (map get-type l))) remaining-names)
+ form remaining-exprs body remaining-clauses expected)]))))
+
+;; An lr-clause is a
+;; (lr-clause (Listof Identifier) Syntax Syntax)
+;;
+;; interp. represents a letrec binding
+(struct lr-clause (names expr clause) #:transparent)
+
+;; get-non-recursive-clauses : (Listof lr-clause) (Listof Identifier) ->
+;; (Listof lr-clause) (Listof )
+;; Find an approximation of letrec clauses that do not create variable cycles
+;;
+;; Note: this is currently approximate, but using Tarjan's algorithm would yield
+;; an optimal ordering for checking these clauses.
+(define (get-non-recursive-clauses clauses flat-names)
+ (define-values (non-recursive remaining _ignore)
+ (for/fold ([non-recursive '()]
+ [remaining '()]
+ [flat-names flat-names])
+ ([clause clauses])
+ (match-define (lr-clause names expr _) clause)
+ (cond [(not (ormap (lambda (n) (member n flat-names bound-identifier=?))
+ (free-vars expr)))
+ (values (cons clause non-recursive)
+ remaining
+ (remove* names flat-names bound-identifier=?))]
+ [else
+ (values non-recursive
+ (cons clause remaining)
+ flat-names)])))
+ (values (reverse non-recursive) remaining))
+
+;; check-non-recursive-clauses : (Listof lr-clause) ->
+;; (Listof Identifier) (Listof Type)
+;; Given a list of non-recursive clauses, check the clauses in order and
+;; build up a type environment for use in the second pass.
+(define (check-non-recursive-clauses clauses)
+ (let loop ([clauses clauses] [env-ids '()] [env-types '()])
+ (cond [(null? clauses) (values env-ids env-types)]
+ [else
+ (match-define (lr-clause names expr _) (car clauses))
+ (define results
+ (get-type/infer names expr
+ (lambda (e) (tc-expr/maybe-expected/t e names))
+ tc-expr/check))
+ (match-define (tc-results: types) results)
+ (with-lexical-env/extend names types
+ (loop (cdr clauses)
+ (cons names env-ids)
+ (cons types env-types)))])))
;; determines whether any of the variables bound in the given clause can have an undefined value
;; in this case, we cannot trust the type the user gave us and must union it with undefined
View
29 pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/succeed/pr13124.rkt
@@ -0,0 +1,29 @@
+#lang typed/racket/base
+
+;; Test for PR 13124
+
+(: foo (-> Flonum))
+(define (foo)
+ (: bn (Flonum -> Flonum))
+ (define (bn n)
+ (cond [(= n 0.0)
+ 1.0]
+ [else (let loop ([s 0.0] [i 0.0])
+ (cond [(i . < . n)
+ (loop (+ s (bn i))
+ (+ i 1.0))]
+ [else s]))]))
+ ;; we want this `v` to type-check without extra annotation
+ (define v 0.0)
+ v)
+
+;; simpler version
+(: foo2 (-> Integer))
+(define (foo2)
+ (: bn (Integer -> Integer))
+ (define (bn n)
+ (if (= n 0)
+ 1 (bn (- n 1))))
+ (define v 1)
+ 0)
+
Something went wrong with that request. Please try again.