[Python-ideas] quantifications, and tuple patterns

[Annie Liu]

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