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
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
type ('a1, 'a2) test0 = unit * unit;
type ('a1, 'a2) test1 = (('a1, 'a2) test0, ('a1, 'a2) test0) test0;
type ('a1, 'a2) test2 = (('a1, 'a2) test1, ('a1, 'a2) test1) test1;
type ('a1, 'a2) test3 = (('a1, 'a2) test2, ('a1, 'a2) test2) test2;
type ('a1, 'a2) test4 = (('a1, 'a2) test3, ('a1, 'a2) test3) test3;
type ('a1, 'a2) test5 = (('a1, 'a2) test4, ('a1, 'a2) test4) test4;
type ('a1, 'a2) test6 = (('a1, 'a2) test5, ('a1, 'a2) test5) test5;
(*too slow with polyml; works with MLton and SML/NJ*)
fun foo (x : ('a1, 'a2) test6) : ('a1, 'a2) test6 = x;
fun main () = foo;
val _ = main ()
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
