[Python-ideas] Re: Syntax for loop invariants

On Wed, Mar 18, 2020 at 09:26:52PM -0700, Andrew Barnert via Python-ideas wrote:

...

On Mar 18, 2020, at 04:22, haael wrote:

What is bugging me is the assymetry: there is a nice way to hint functions, but there is none to hint loops.

Then Steve’s suggestion of a context manager seems perfect. It allows you to hint any statement, including a loop statement, by adding whatever code you want that gets run before and after the statement.

Wasn't me, it was the other Stephen who spells his name with a "ph" :-) Context managers are great when the CM has its own standard behaviour that gets reused over and over again, like open files. You need to write the the context manager once, and you can use it over and over again. The only standard part of a loop invariant is, as far as I can tell, to save a copy of the loop variable at the start of the loop. Everything else is likely to be unique. So each loop will need its own context manager, meaning its own class. The *actual* invariant will be buried far away, in a CM class, rather than right there next to the loop. You might be able to reuse some invariant CMs by generalising the invariants into a meta-invariant, but I expect that to lead to over- abstract code that is unclear and hard to follow. But in general, each loop will need its own CM class. Because the actual invariant is far away, buried in a class rather than there next to the loop, we will rely on a unique, descriptive name for every loop that has an invariant. Naming is hard: that's not going to work well, and we'll end up with multiple context managers with generic names like "invariant1", "invariant2" etc. Worse: the condition will likely need to be written as a string, or a lambda, in order to delay evaluation. In Eiffel, invariants are a block. Forcing invariants into a context manager would have all the disadvantages of forcing every for loop into a call to map() with a named function. I don't think the context manager idea will be practical unless you have only a very small number of very similar, simple, invariants. -- Steve