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 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 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
