[isabelle-dev] A note on composition in src/Pure/library.ML

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Sun Jan 22 09:18:15 CET 2017

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

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.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170122/930bfc98/attachment.asc>

More information about the isabelle-dev mailing list