Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Port more benchmarks from Racket #5

Open
bennn opened this issue Mar 20, 2017 · 5 comments
Open

Port more benchmarks from Racket #5

bennn opened this issue Mar 20, 2017 · 5 comments
Assignees

Comments

@bennn
Copy link
Member

bennn commented Mar 20, 2017

Try porting more benchmarks from Racket.

Two options for this:

  • type a small chunk of each benchmark
  • fully type, randomly sample
@bennn bennn added this to the gradschool milestone Mar 20, 2017
@bennn bennn self-assigned this Mar 20, 2017
@bennn
Copy link
Member Author

bennn commented Apr 21, 2017

I started porting suffixtree, its taking longer than expected but this might work.

Will try to fnish tonight, then try to port another

@bennn
Copy link
Member Author

bennn commented Apr 22, 2017

Failure for now. The writing is a higher priority.

@bennn
Copy link
Member Author

bennn commented Apr 26, 2017

FWIW, here is a suffixtree function that Reticulated cannot type. All the code is below; key points:

  • the comment at the top is from the original author (Danny Yoo, src)
  • the problematic type signature starts at the first non-comment line below
;; node-follow/k: node label (node -> A)
;;                           (node number -> B)
;;                           (node label number -> C)
;;                           (node number label number -> D)
;;                    -> (union A B C D)
;; 
;; Traverses the node's edges along the elements of the input label.
;; Written in continuation-passing-style for leakage containment.
;; One of the four continuation arguments will be executed.
(: node-follow/k (All (A B C D)
                      (-> Node
                          Label
                          (-> Node A)
                          (-> Node Index B)
                          (-> Node Label Index C)
                          (-> Node Index Label Index D)
                          (U A B C D))))
(define (node-follow/k node
                       original-label
                       matched-at-node/k
                       matched-in-edge/k
                       mismatched-at-node/k
                       mismatched-in-edge/k)
  (: EDGE/k (-> Node Label Index (U A B C D)))
  (define (EDGE/k node label label-offset)
    (: up-label Label)
    (define up-label (node-up-label node))
    (let loop ((k 0))
      (define k+label-offset (+ k label-offset))
      (cond
       ((= k (label-length up-label))
        (unless (index? k+label-offset) (error "node/folllowd"))
        (NODE/k node label k+label-offset))
       ((= k+label-offset (label-length label))
        (unless (index? k) (error "node/followk"))
        (matched-in-edge/k node k))
       ((label-element-equal? (label-ref up-label k)
                              (label-ref label k+label-offset))
        (loop (add1 k)))
       (else
        (unless (and (index? k)
                     (index? k+label-offset)) (error "node-follow/k mismatched fail"))
        (mismatched-in-edge/k node k label
                              k+label-offset)))))
  (: NODE/k (-> Node Label Index (U A B C D)))
  (define (NODE/k node label label-offset)
    (if (= (label-length label) label-offset)
        (matched-at-node/k node)
        (let ([child (node-find-child node (label-ref label label-offset))])
          (if child
              (EDGE/k child label label-offset)
              (mismatched-at-node/k node label label-offset)))))
  (NODE/k node (label-copy original-label) 0))

@bennn
Copy link
Member Author

bennn commented Apr 26, 2017

More data, here's a table of racket benchmarks from the GTP repo and whether they use "All" types:

benchmark at least one All-type ?
acquire X
dungeon X
forth
fsm X
fsmoo
gregor
kcfa X
lnm
mbta X
morsecode X
quadBG X
quadMB X
snake
suffixtree X
synth X
take5
tetris
zombie
zordoz X

Time-permitting it would be good to explore the "small" benchmarks that don't use All-types.

(Comparing across languages is apples to oranges, so give these thoughts little/no weight: morsecode was fast in TR, will it be fast in Retic? snake and tetris had very high overhead in TR, I think because the types implied extra traversals of lists)

@bennn bennn removed this from the gradschool milestone May 9, 2017
@bennn
Copy link
Member Author

bennn commented Aug 8, 2017

Alternatively ... put tag soundness in Typed Racket

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant