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

[Lawrence Paulson]

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.

Larry

> 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...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20170123/46a620a2/attachment-0002.html>