Tracking issue for verifying the benchmarks in gradual-typing-performance

[rosekunkel]

Progress for verifying the benchmarks in https://github.com/nuprl/gradual-typing-performance/tree/master/benchmarks

• [ ] acquire
  • [ ] Write contracts.
• [ ] dungeon
  • [ ] Write contracts.
• [ ] forth
  • [ ] Write contracts.
  • [ ] Deal with object-oriented Racket: #77
• [ ] fsm (verified except for tricky invariants maintained by helper accumulated-%s)
  • [x] Write contracts.
  • [ ] Handle keyword arguments: #78
  • [x] Handle apply: #74
• [ ] fsmoo
  • [ ] Write contracts.
• [ ] gregor
  • [ ] Write contracts.
• [ ] kcfa
  • [ ] Write contracts.
• [ ] lnm
  • [ ] Write contracts.
  • [ ] Handle keyword arguments: #78
• [ ] mbta
  • [ ] Write contracts.
• [x] morsecode
  • [x] Write contracts.
  • [x] Handle apply: #74
• [ ] quadBG
  • [ ] Write contracts.
• [ ] quadMB
  • [ ] Write contracts.
• [x] sieve
  • [x] Write contracts.
  • [x] Handle multiple return values: #61
  • [x] Handle printf: #81
• [x] snake
• [x] stack
  • [x] Write contracts.
• [ ] suffixtree
  • [ ] Write contracts.
• [ ] synth
  • [ ] Write contracts.
• [x] tetris
• [x] zombie
• [ ] zordoz.6.2
  • [ ] Write contracts.
• [ ] zordoz.6.3
  • [ ] Write contracts.
• [ ] zordoz.6.5
  • [ ] Write contracts.

[bennn]

Question: why is "write contracts" a task? I mean, why not use the types from the benchmarks?

I've looked at your sieve and morsecode but I'm not sure if you're inferring contracts yourself or using the types. For example:

• for morsecode's char-table, why hash? instead of (hash/c char? symbol?) (original type)
• for sieve, why use exact-integer? instead of natural numbers? (original types)

[bennn]

Also, FYI, I'm hoping to run these benchmarks "as-is" through soft contracts and I started a mapping from contracts to Typed Racket syntax here.

[philnguyen]

We'll figure out getting the contracts from TR programs eventually. But for a while we just added the contracts manually, which somewhat mismatched with the types.