Hi all, in http://isabelle.in.tum.de/repos/isabelle/rev/18a6b96f8b00 you see the result of a struggle ongoing for years now to get static vs. dynamic scoping of code generator conversions etc. right.
Finally I realized that composition is to blame for. See the following example: ML_val ‹ fun foo k = error (string_of_int (k + 1)); val bar = I oo foo; val _ = bar 41; › Surprisingly (?), there is no error here. The reason is obvious when inspecting src/Pure/library.ML: ML ‹ fun (f oo g) x y = f (g x y); fun (f ooo g) x y z = f (g x y z); fun (f oooo g) x y z w = f (g x y z w); › The composition operators always wait for all arguments to be applied! Alternative definitions would be ML ‹ fun (f oo g) x = f o g x; fun (f ooo g) x = f oo g x; fun (f oooo g) x = f ooo g x; › ML_val ‹ fun foo k = error (string_of_int (k + 1)); val bar = I oo foo; val _ = bar 41; › Yielding the expected error. I am not sure whether this is a striking argument to change such long-standing definitions dating back to c755dfd02509 in 1998. But it is at least worth noting that these are not apt for partial application. Cheers, Florian -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev