www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | README

speed-many-poly.rkt (614B)

      1 #lang type-expander
      2 
      3 (require (for-syntax racket))
      4 
      5 ;; This seems to be a slow-starting exponential, with a factor of ×2.5
      6 ;; each time n is increased by 100.
      7 ;; n=500 takes nearly 3 minutes, n=1000 should, by projection, take 4.5 hours.
      8 (define-for-syntax n 200)
      9 
     10 (: f ((Λ (_)
     11         (with-syntax ([(T ...)
     12                        (map (λ (i) (gensym 'τ)) (range n))])
     13           #'(∀ (A B T ...)
     14                (→ (List A T ...) B (List B T ...)))))))
     15 (define (f l v)
     16   (cons v (cdr l)))
     17 
     18 (define-syntax (callf stx)
     19   (with-syntax ([(v ...) (range n)])
     20     #'(f (list "a" v ...) 'x)))
     21 
     22 (define cf (callf))