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