Skip to content
New issue

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

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

Already on GitHub? # 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

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

No branches or pull requests

1 participant