[racket] non-terminating type check for typed racket

From: Danny Yoo (dyoo at cs.wpi.edu)
Date: Mon Apr 18 11:40:52 EDT 2011

> Also, if the part that's slow may well be inferring the type
> parameters to a polymorphic function application, in which case it
> should be easy to work around by explicitly using `inst'.


One hot spot identified: the use of remove-duplicates in the
definition of -and within typed-scheme/types/filter-ops.rkt is taking
a significant amount of time.  I modified the loop to display timing
information, with the following (in Racket 5.0.1):



diff --git a/collects/typed-scheme/types/filter-ops.rkt
b/collects/typed-scheme/types/filter-ops.rkt
index 2d24753..d336ef3 100644
--- a/collects/typed-scheme/types/filter-ops.rkt
+++ b/collects/typed-scheme/types/filter-ops.rkt
@@ -132,7 +132,8 @@
     (case-lambda [() -top]
                  [(f) f]
                  [fs (make-AndFilter fs)]))
-  (let loop ([fs (remove-duplicates args filter-equal?)] [result null])
+  (let loop ([fs (time (begin (displayln (length args))
+                             (remove-duplicates args
filter-equal?)))] [result null])
     (if (null? fs)
         (match result
           [(list) -top]



Here's the time data I'm seeing during type-checking:

##########################################################
cpu time: 0 real time: 0 gc time: 0
3
cpu time: 0 real time: 0 gc time: 0
3
cpu time: 0 real time: 0 gc time: 0
4096
cpu time: 496 real time: 496 gc time: 0
4096
cpu time: 492 real time: 500 gc time: 0
2
cpu time: 0 real time: 0 gc time: 0
3
cpu time: 0 real time: 0 gc time: 0
3
cpu time: 0 real time: 0 gc time: 0
4096
cpu time: 496 real time: 512 gc time: 0
4096
cpu time: 496 real time: 497 gc time: 0
2
cpu time: 0 real time: 0 gc time: 0
3
cpu time: 0 real time: 0 gc time: 0
3
cpu time: 0 real time: 0 gc time: 0
8192
cpu time: 1996 real time: 2011 gc time: 0
8192
cpu time: 1984 real time: 1996 gc time: 0
##########################################################


This is a partial listing, but you can see that this is eating at
least two seconds here and there throughout the typechecking phase.
There is something funny in the performance of remove-duplicates: it's
exhibiting very bad n^2 performance here.  I've made the following
change to improve the performance in that hotspot:


diff --git a/collects/typed-scheme/types/filter-ops.rkt
b/collects/typed-scheme/types/filter-ops.rkt
index 2d24753..3786840 100644
--- a/collects/typed-scheme/types/filter-ops.rkt
+++ b/collects/typed-scheme/types/filter-ops.rkt
@@ -132,7 +132,11 @@
     (case-lambda [() -top]
                  [(f) f]
                  [fs (make-AndFilter fs)]))
-  (let loop ([fs (remove-duplicates args filter-equal?)] [result null])
+  (let loop ([fs (time (begin (displayln (length args))
+                             ;; Subtle: remove-duplicates appears not to use
+                             ;; a fast hashtable unless #:key is defined and
+                             ;; the comparator is either eq? or equal?.
+                             (remove-duplicates args equal? #:key
Rep-seq)))] [result null])
     (if (null? fs)
         (match result
           [(list) -top]


Something is still really expensive in -and: when I time the whole
thing, I can still see it taking seconds in there.  I'll continue to
investigate.


Posted on the users mailing list.