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

[Makarius]

On 23/01/17 12:25, Lawrence Paulson wrote:
> 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.

>> On 22 Jan 2017, at 08:18, Florian Haftmann
>> <florian.haftmann at informatik.tu-muenchen.de
>> <mailto: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);
>> ›

Such a subtle change of semantics would also require a change of the
name, otherwise we get into a mire of unclear meaning of Isabelle/ML
sources over a long history.

In this case there is not even a clear indication to go this way or that
way with partial application: making it more strict can cause other
surprises.


Also note that oo, ooo, oooo are relatively old-fashioned and rarely
used these days.


	Makarius