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