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

[Florian Haftmann]

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

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