Polymorphic+Typeclass Superposition (Submitted to Paar 2014)

Abstract (draft)

Evaluation


Successrate
Monomorphic vs Type Class runtime (16 facts)
  • Monomorphic versus Type Class
  • Timeout was 2h.
  • 16 Facts.
  • 579 Problems.
  • Both settings combined solved 147 problems.
  • Monomorphic took in average: 5.90s on all 147 problems.
  • Monomorphic took in average: 2.99s on 143 proved problems.
  • Monomorphic took in average: 1.98s on 137 problems both proved.
  • Type Class took in average: 8.76s on all 147 problems.
  • Type Class took in average: 4.45s on 141 proved problems.
  • Type Class took in average: 3.67s on 137 problems both proved.

Monomorphic vs Type Class runtime (256 facts)
  • Monomorphic versus Type Class
  • Timeout was 2h.
  • 256 Facts.
  • 579 Problems.
  • Both settings combined solved 222 problems.
  • Monomorphic took in average: 814.88s on all 222 problems.
  • Monomorphic took in average: 383.77s on 208 proved problems.
  • Monomorphic took in average: 197.85s on 193 problems both proved.
  • Type Class took in average: 615.29s on all 222 problems.
  • Type Class took in average: 136.68s on 207 proved problems.
  • Type Class took in average: 85.21s on 193 problems both proved.

Poly Tags vs Type Class runtime (256 facts)
  • Poly Tags versus Type Class
  • Timeout was 2h.
  • 256 Facts.
  • 579 Problems.
  • Both settings combined solved 215 problems.
  • Poly Tags took in average: 1863.83s on all 215 problems.
  • Poly Tags took in average: 114.78s on 162 proved problems.
  • Poly Tags took in average: 119.33s on 154 problems both proved.
  • Type Class took in average: 399.88s on all 215 problems.
  • Type Class took in average: 136.68s on 207 proved problems.
  • Type Class took in average: 20.08s on 154 problems both proved.

Poly Native vs Type Class runtime (256 facts)
  • Poly Native versus Type Class
  • Timeout was 2h.
  • 256 Facts.
  • 579 Problems.
  • Both settings combined solved 215 problems.
  • Poly Native took in average: 889.83s on all 215 problems.
  • Poly Native took in average: 132.73s on 192 proved problems.
  • Poly Native took in average: 78.39s on 184 problems both proved.
  • Type Class took in average: 399.88s on all 215 problems.
  • Type Class took in average: 136.68s on 207 proved problems.
  • Type Class took in average: 122.11s on 184 problems both proved.

Syntax

Simple Example File

Web Service

POST (HTTP) to: http://91.228.53.68:51642/paar14
E.g. by using: curl -F file=@example.dfg "http://91.228.53.68:51642/paar14"
Note this is a slow server. Default timeout is 300 seconds.

Evaluation (continued)

Evaluation Type Class versus other encodings (PDF)