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
type ('a1, 'a2) test0 = 'a1 * 'a2;
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;
(*size between test3 and test4*)
type ('a1, 'a2) test3_4 = (('a1, 'a2) test2, ('a1, 'a2) test2) test3;
(*OK with polyml*)
(* fun foo (x : ('a1, 'a2) test3) : ('a1, 'a2) test3 = x; *)
(*slow with polyml*)
fun foo (x : ('a1, 'a2) test3_4) : ('a1, 'a2) test3_4 = x;
(*too slow with polyml; works with MLton and SML/NJ*)
(* fun foo (x : ('a1, 'a2) test4) : ('a1, 'a2) test4 = x; *)
fun main () = foo;
val _ = main ()
type ('a1, 'a2) test0 = 'a1 * 'a2;
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;
(*size between test3 and test4*)
type ('a1, 'a2) test3_4 = (('a1, 'a2) test2, ('a1, 'a2) test2) test3;
type ('a1, 'a2) copy_test0 = 'a1 * 'a2;
type ('a1, 'a2) copy_test1 = (('a1, 'a2) copy_test0, ('a1, 'a2) copy_test0)
copy_test0;
type ('a1, 'a2) copy_test2 = (('a1, 'a2) copy_test1, ('a1, 'a2) copy_test1)
copy_test1;
type ('a1, 'a2) copy_test3 = (('a1, 'a2) copy_test2, ('a1, 'a2) copy_test2)
copy_test2;
type ('a1, 'a2) copy_test4 = (('a1, 'a2) copy_test3, ('a1, 'a2) copy_test3)
copy_test3;
type ('a1, 'a2) copy_test3_4 = (('a1, 'a2) copy_test2, ('a1, 'a2) copy_test2)
copy_test3;
(*slow with polyml*)
fun foo (x : ('a1, 'a2) test3_4) : ('a1, 'a2) copy_test3_4 = x;
(*too slow with polyml; works with MLton and SML/NJ*)
(* fun foo (x : ('a1, 'a2) test4) : ('a1, 'a2) copy_test4 = x; *)
fun main () = foo;
val _ = main ()
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
