[polyml] Very slow type checking with largish/nested type abbreviations

Addendum: the type check remains slow even in case the instantiated variables are ultimately unused. An example can be found in attached test_check_unused.sml

Again, the file does not compile in reasonable time in Poly/ML and compiles in <0.2 seconds in SML/NJ and about 1 second in MLton.

Best wishes,

Kevin

On 10.04.25 14:35, Kevin Kappelmann wrote:

Dear list,

I am facing very slow type checking in a development of mine (in Isabelle), possibly due to largish types created by nested type abbreviations. The type checking of these types is significantly faster in MLton and SML/NJ. I hence wanted to ask if there is any hope that type checking performance for such cases could be improved in Poly/ML (with reasonable effort)?

Attached, you can find 2 short files that demonstrate this. Both files create nested type abbreviations and a function "foo" that uses these types.

In test_check.sml, one of the types has to be checked against itself. In test_compare.sml, two equal types have to be compared to each other.

Times on an Apple M3 machine:

• test_check.sml:

  • polyml-5.9.1/arm64_32-darwin: 13.043 seconds (command: "poly < test_check.sml")
  • SML/NJ Version 110.99.7; 64-bit: 0.161 seconds (command: "sml < test_check.sml")
  • MLton Version 20241230: 1.201 seconds (command: "mlton test_check.sml")

• test_check.sml when changing "foo" to use type "test4" instead of

"test3_4" (cf. source file)

• polyml-5.9.1/arm64_32-darwin: TIMEOUT after 10 minutes

• SML/NJ Version 110.99.7; 64-bit: 0.398 seconds

• MLton Version 20241230: 1.249 seconds

• test_compare.sml:

  • polyml-5.9.1/arm64_32-darwin: 13.369 seconds
  • SML/NJ Version 110.99.7; 64-bit: 0.178 seconds
  • MLton Version 20241230: 1.221 seconds

Best wishes,

Kevin

---

polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml