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
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
Thank you for sending the example and cutting it down to a manageable size. It looks as though it is expanding the type-abbreviations before the type checking but I'd have to work through it carefully to see what exactly is going on. I've created an "issue" on GitHub so it won't get forgotten.
Best wishes, David
On 10/04/2025 16:52, Kevin Kappelmann wrote:
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
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
-
David.Matthews＠prolingua.co.uk -
kevin.kappelmann＠tum.de