[isabelle-dev] A note on composition in src/Pure/library.ML
lp15 at cam.ac.uk
Mon Jan 23 12:25:14 CET 2017
I’m not sure what to conclude from this. It’s about non-functional behaviour, so not quite something people ought to rely upon.
I’m guessing one could make the change and nothing would happen. I’m still not convinced that the case for a change has been made however.
For what it’s worth, there are no such operators in HOL Light.
> On 22 Jan 2017, at 08:18, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> 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.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the isabelle-dev