[Python-ideas] quantifications, and tuple patterns
Annie Liu
liu at cs.stonybrook.edu
Sat Jan 14 06:25:19 CET 2012
Hi!
I'd like to propose adding quantifications to python. It'd be very
helpful to have tuple patterns as well.
I found extensive use of quantifications while learning and teaching
distributed algorithms in the last few years, and I saw more and more
places where they can help make programming easier and make programs
clearer and less error-prone. They didn't show up this much until I
started to pay attention, since my students (even the best ones) and
myself too just coded them away too quickly.
For example, even the simplest "some x in s has pred", when a witness
for x is not needed, could end up like "{x for x in s if pred}",
"any(pred for x in s)", "len(...)!=0", "len...>0", len...>=1", ... not
to mention the many more kinds of loops and tests written by the
majority of students not used to writing queries/comprehensions. Even
more kinds of loops and bigger hassles are involved when a witness for
x is needed.
For another example, a simple "each x in s has x > y" tends to end up
like "min(s)>y", which is incorrect, since s could be empty, so one
has to either add this condition or invent some boundary value for
min, which is error-prone since it is sensitive to the possible values
of elements of s and the uses of these values.
For an example distributed algorithm, one may look at Robbert von
Renesse's "Paxos made moderately complex", at
http://www.cs.cornell.edu/courses/CS7412/2011sp/paxos.pdf (he has
newer versions but the pseudo code didn't change). It has 8 uses of
quantifications. His algorithm can be coded almost exactly like that
in our language DistAlgo (python with small extensions for distributed
programming) if we have quantifications and tuple patterns. For
example (using "!" to indicate a bound variable in tuple patterns),
while some (!slot_num,p1) in decisions:
if some (!slot_num,p2) in proposals has p2 != p1:
is currently written as follows (it happens to be correct here to use
"for" for "if" but generally requires more code to be correct):
while {p1 for (s0,p1) in decisions if s0==slot_num}:
p1 = {p1 for (s0,p1) in decisions if s0==slot_num}.pop()
for p2 in {p2 for (s0,p2) in proposals if s0==slot_num if p2 != p1}:
Both a witness for p1 and a witness for p2 are needed here. (BTW a
best student working on this, after given advanced warnings and hints,
wrote a 4-line nested "for"s and "if"s that were actually incorrect)
So we started to think about adding quantifications and tuple patterns
to DistAlgo too (other extensions are all distributed programming
features).
In general, "some x in s has pred" should return true/false AND bind x
to a witness if true is returned. One might object to the side effect
of the binding, but it is most natural here for ease of programming
and clarity of programs, and it helps program efficiency too. Witness
in existential quantification is also standard in logic.
Of course, there is the obvious problem of new keywords: "some",
"each", "has" (perhaps one may use ":" for "has") or some others. The
"!" syntax would be ok for tuple patterns but only if there are no
"equal cards", i.e., multiple occurrences of a same variable (though
such occurrences don't seem to be useful in current python semantics
for "for". A special symbol for wildcard would be more useful). So
we are looking for good syntax.
Thanks,
Annie Liu
More information about the Python-ideas
mailing list