Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

PEP-484 "numeric tower" approach makes it hard/impossible to specify contracts in documentation #91390

Closed
tfish2 mannequin opened this issue Apr 5, 2022 · 9 comments
Closed

Comments

@tfish2
Copy link
Mannequin

tfish2 mannequin commented Apr 5, 2022

BPO 47234
Nosy @rhettinger, @stevendaprano, @JelleZijlstra, @AlexWaygood

Note: these values reflect the state of the issue at the time it was migrated and might not reflect the current state.

Show more details

GitHub fields:

assignee = None
closed_at = None
created_at = <Date 2022-04-05.20:26:08.691>
labels = []
title = 'PEP-484 "numeric tower" approach makes it hard/impossible to specify contracts in documentation'
updated_at = <Date 2022-04-08.12:54:15.235>
user = 'https://bugs.python.org/tfish2'

bugs.python.org fields:

activity = <Date 2022-04-08.12:54:15.235>
actor = 'tfish2'
assignee = 'none'
closed = False
closed_date = None
closer = None
components = []
creation = <Date 2022-04-05.20:26:08.691>
creator = 'tfish2'
dependencies = []
files = []
hgrepos = []
issue_num = 47234
keywords = []
message_count = 6.0
messages = ['416814', '416817', '416818', '416967', '416981', '416982']
nosy_count = 5.0
nosy_names = ['rhettinger', 'steven.daprano', 'JelleZijlstra', 'AlexWaygood', 'tfish2']
pr_nums = []
priority = 'normal'
resolution = None
stage = None
status = 'open'
superseder = None
type = None
url = 'https://bugs.python.org/issue47234'
versions = []

@tfish2
Copy link
Mannequin Author

tfish2 mannequin commented Apr 5, 2022

Here is a major general problem with python-static-typing as it is
described by PEP-484: The approach described in
https://peps.python.org/pep-0484/#the-numeric-tower negatively impacts
our ability to reason about the behavior of code with stringency.

I would like to clarify one thing in advance: this is a real problem
if we subscribe to some of the important ideas that Dijkstra
articulated in his classic article "On the role of scientific thought"
(e.g.: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/EWD447.html).
Specifically, this part:

"""
Let me try to explain to you, what to my taste is characteristic
for all intelligent thinking. It is, that one is willing to study in
depth an aspect of one's subject matter in isolation for the sake of
its own consistency, all the time knowing that one is occupying
oneself only with one of the aspects. We know that a program must be
correct and we can study it from that viewpoint only; we also know
that it should be efficient and we can study its efficiency on another
day, so to speak. In another mood we may ask ourselves whether, and if
so: why, the program is desirable. But nothing is gained —on the
contrary!— by tackling these various aspects simultaneously. It is
what I sometimes have called "the separation of concerns", which, even
if not perfectly possible, is yet the only available technique for
effective ordering of one's thoughts, that I know of. This is what I
mean by "focussing one's attention upon some aspect": it does not mean
ignoring the other aspects, it is just doing justice to the fact that
from this aspect's point of view, the other is irrelevant. It is being
one- and multiple-track minded simultaneously.
"""

So, "code should be easy to reason about".

Now, let us look at this function - I am here (mostly) following the
Google Python style guide (https://google.github.io/styleguide/pyguide.html) for now:

=== Example 1, original form ===

def middle_mean(xs):
  """Compute the average of the nonterminal elements of `xs`.

Args:
xs: a list of floating point numbers.

Returns:
A float, the mean of the elements in xs[1:-1].

Raises:
ValueError: If len(xs) < 3.
"""
if len(xs) < 3:
raise ValueError('Need at least 3 elements to compute middle mean.')
return sum(xs[1:-1]) / (len(xs) - 2)
======

Let's not discuss performance, or whether it makes sense to readily
generalize this to operate on other sequences than lists, but focus,
following Dijkstra, on one specific concern here: Guaranteed properties.

Given the function as it is above, I can make statements that are
found to be correct when reasoning with mathematical rigor, such as
this specific one that we will come back to:

=== Theorem 1 ===
If we have an object X that satisfies these properties...:

  1. type(X) is list
  2. len(X) == 4
  3. all(type(x) is float for x in X)

...then we are guaranteed that middle_mean(X) evaluates to a value Y
which satisfies:

  • type(Y) is float
  • Y == (X[1] + X[2]) * 0.5 or math.isnan(Y)
    ===

Now, following PEP-484, we would want to re-write our function, adding type annotations.
Doing this mechanically would give us:

=== Example 1, with mechanically added type information ===

def middle_mean(xs: List[float]) -> float:
  """Compute the average of the nonterminal elements of `xs`.

Args:
xs: a list of floating point numbers.

Returns:
A float, the mean of the elements in xs[1:-1].

Raises:
ValueError: If len(xs) < 3.
"""
if len(xs) < 3:
raise ValueError('Need at least 3 elements to compute middle mean.')
return sum(xs[1:-1]) / (len(xs) - 2)
======

(We are also deliberately not discussing another question here: given
this documentation and type annotation, should the callee be
considered to be permitted to mutate the input list?)

So, given the above form, we now find that there seems to be quite a
bit of redundancy here. After all, we have the type annotation but
also repeat some typing information in the docstring. Hence, the
obvious proposal here is to re-write the above definition again, obtaining:

=== Example 1, "cleaned up" ===

def middle_mean(xs: List[float]) -> float:
  """Compute the average of the nonterminal elements of `xs`.

Args:
xs: numbers to average, with terminals ignored.

Returns:
The mean of the elements in xs[1:-1].

Raises:
ValueError: If len(xs) < 3.
"""
if len(xs) < 3:
raise ValueError('Need at least 3 elements to compute middle mean.')
return sum(xs[1:-1]) / (len(xs) - 2)
======

But now, what does this change mean for the contract? Part of the "If
arguments have these properties, then these are the guarantees"
contract now is no longer spelled out by the docstring, but via type
annotations. We naturally would expect this to be straightforward,
so, we would like to have:

=== Theorem 1b ===
If we have an object X that satisfies these properties...:

  1. Static type analysis tells us that X has the appropriate type for
    being passed into middle_mean().
  2. len(X) == 4

...then we are guaranteed that middle_mean(X) evaluates to a value Y
which satisfies:

  • Static type analysis can tell us that this value is a float
  • Y == (X[1] + X[2]) * 0.5 or math.isnan(Y)
    ===

...but the actual situation is:

a) This is not guaranteed.
b) PEP-484 does not seem to leave us any option to amend
the type annotation so that we can obtain a corresponding guarantee.

Specifically, this Python3+ example breaks it - note that PEP-484
states that: "when an argument is annotated as having type float, an
argument of type int is acceptable".

 >>> middle_mean([0.0, 1.25, 10**1000, 0.0])
 Traceback (most recent call last):
   File "<stdin>", line 1, in <module>
   File "<stdin>", line 15, in middle_mean
 OverflowError: int too large to convert to float

So, even the "this function call evaluates to..." is violated here -
it does not evaluate to anything, but raises an exception instead.

One option to address this would be to stick with the code as in
[Example 1, with mechanically added type information], but I would
argue that it is highly confusing that float in the static type
annotation and float in the docstring then refer to two very
different concepts. This is certainly not desirable (and we should not
expect Python practitioners to do it that way)!

Now, while this may superficially look like a weird edge case, that is
actually not so - the problem is that such mismatches in some
situations "allow us to drive in a wedge" and create conditions where
there is a deviation between actual and expected program
behavior. This is a common starting point for writing exploits, as for
example these classic articles nicely illustrate:

"Smashing The Stack For Fun And Profit" (aleph1@underground.org, Phrack #49)
(E.g.: https://inst.eecs.berkeley.edu/~cs161/fa08/papers/stack_smashing.pdf)

"Delivering Signals for Fun and Profit" (Michal Zalewski)
(E.g.: https://lcamtuf.coredump.cx/signals.txt)

CAPEC-71: Using Unicode Encoding to Bypass Validation Logic
https://capec.mitre.org/data/definitions/71.html

So, clearly, we want to not only maintain the ability to reason about
the behavior of Python code with mathematical stringency, but also
make this reasonably simple and straightforward. I would also argue
that, given the popularity of Python as a CS education language, it
matters that professors have a viable substrate for teaching the skill
to stringently reason about the behavior of code.

@JelleZijlstra
Copy link
Member

Thanks for your report, but I would appreciate a more concise explanation. Let me try to rephrase the problem.

Given this function:

def mean(x: list[float]) -> float:
    return sum(x) / len(x)

We want to provide a guarantee that if x is a nonempty list containing only floats, the function returns successfully and returns a float.

But the type system currently doesn't give this guarantee, because PEP-484 specifies that ints are compatible with floats, and mean([0.0, 1.25, 10**1000, 0.0]) will throw OverflowError.

---

We generally discuss issues with the general type system over at https://github.com/python/typing/issues, but here are a few thoughts:

  • The type system doesn't generally try to cover exceptions. Your function could also raise MemoryError, or KeyboardInterrupt, and the type system can't tell you.
  • The concrete proposal here would be to make int no longer implicitly compatible with float. That might be nice, but at this point it would be a big break in backwards compatibility, so I'm not sure we can do it.

@rhettinger
Copy link
Contributor

This is a partial duplicate of an issue you already filed: https://bugs.python.org/issue47121 where math.isfinite(10**1000) raises an OverflowError even though it type checks.

Here was one of the comments:
"""
Types relationships are useful for verifying which methods are available, but they don't make promises about the range of valid values. For example math.sqrt(float) -> float promises which types are acceptable but doesn't promise that negative inputs won't raise an exception. Likewise, "n: int=10; len(range(n))" is type correct but will raise an OverflowError for "n = 10**100".
"""

@tfish2
Copy link
Mannequin Author

tfish2 mannequin commented Apr 8, 2022

This is not a partial duplicate of https://bugs.python.org/issue47121 about math.isfinite().
The problem there is about a specific function on which the documentation may be off -
I'll comment separately on that.

The problem here is: There is a semantic discrepancy between what the
term 'float' means "at run time", such as in a check like:

issubclass(type(x), float)

(I am deliberately writing it that way, given that isinstance() can, in general [but actually not for float], lie.)

and what the term 'float' means in a statically-checkable type annotation like:

def f(x: float) -> ... : ...

...and this causes headaches.

The specific example ('middle_mean') illustrates the sort of weird
situations that arise due to this. (I discovered this recently when
updating some of our company's Python onboarding material, where the
aspiration naturally is to be extremely accurate with all claims.)

So, basically, there is a choice to make between these options:

Option A: Give up on the idea that "we want to be able to reason with
stringency about the behavior of code" / "we accept that there will be
gaps between what code does and what we can reason about". (Not
really an option, especially with an eye on "writing secure code
requires being able to reason out everything with stringency".)

Option B: Accept the discrepancy and tell people that they have to be
mindful about float-the-dynamic-type being a different concept from
float-the-static-type.

Option C: Realizing that having "float" mean different things for
dynamic and static typing was not a great idea to begin with, and get
everybody who wants to state things such as "this function parameter
can be any instance of a real number type" to use the type
numbers.Real instead (which may well need better support by
tooling), respectively express "can be int or float" as Union[int, float].

Also, there is Option D: PEP-484 has quite a lot of other problems
where the design does not meet rather natural requirements, such as:
"I cannot introduce a newtype for 'a mapping where I know the key to
be a particular enum-type, but the value is type-parametric'
(so the new type would also be 1-parameter type-parametric)", and
this float-mess is merely one symptom of "maybe PEP-484 was approved
too hastily and should have been also scrutinized by people
from a community with more static typing experience".

Basically, Option B would spell out as: 'We expect users who use
static type annotations to write code like this, and expect them to be
aware of the fact that the four places where the term "float" occurs
refer to two different concepts':

def foo(x: float) -> float:
  """Returns the foo of the number `x`.

Args:
x: float, the number to foo.

Returns:
float, the value of the foo-function at x.
"""
...

...which actually is shorthand for...:

def foo(x: float  # Note: means float-or-int
  ) -> float  # Note: means float-or-int
  :
  """Returns the foo of the number `x`.

Args:
x: the number to foo, an instance of the float type.

Returns:
The value of the foo-function at x,
as an instance of the float type.
"""
...

Option C (and perhaps D) appear - to me - to be the only viable
choices here. The pain with Option C is that it invalidates/changes
the meaning of already-written code that claims to follow PEP-484,
and the main point of Option D is all about: "If we have to cause
a new wound and open up the patient again, let's try to minimize
the number of times we have to do this."

Option C would amount to changing the meaning of...:

def foo(x: float) -> float:
  """Returns the foo of the number `x`.

Args:
x: float, the number to foo.

Returns:
float, the value of the foo-function at x.
"""
...

to "static type annotation float really means instance-of-float here"
(I do note that issubclass(numpy.float64, float), so passing a
numpy-float64 is expected to work here, which is good), and ask people
who would want to have functions that can process more generic real
numbers to announce this properly. So, we would end up with basically
a list of different things that a function-sketch like the one above
could turn into - depending on the author's intentions for
the function, some major cases being perhaps:

(a) ("this is supposed to strictly operate on float")
def foo(x: float) -> float:
"""Returns the foo of the number x.

Args:
x: the number to foo.

Returns:
the value of the foo-function at x.
"""

(b) ("this will eat any kind of real number")

def foo(x: numbers.Real) -> numbers.Real:
  """Returns the foo of the number `x`.

Args:
x: the number to foo.

Returns:
the value of the foo-function at x.
"""

(c) ("this will eat any kind of real number, but the result will always be float")

def foo(x: numbers.Real) -> float:
  """Returns the foo of the number `x`.

Args:
x: the number to foo.

Returns:
the value of the foo-function at x.
"""

(d) ("this will eat int or float, but the result will always be float")

def foo(x: Union[int, float]) -> float:
  """Returns the foo of the number `x`.

Args:
x: the number to foo.

Returns:
the value of the foo-function at x.
"""

(e) ("this will eat int or float, and the result will also be of that type")

def foo(x: Union[int, float]) -> Union[int, float]:
  """Returns the foo of the number `x`.

Args:
x: the number to foo.

Returns:
the value of the foo-function at x.
"""

(f) ("this method maps a float to a real number, but subclasses can
generalize this to accept more than float, and return something that
gives more guarantees than being a real number.")

def myfoo(self, x: float) -> numbers.Real:
  """Returns the foo of the number `x`.

Args:
x: the number to foo.

Returns:
the value of the foo-function at x.
"""

@AlexWaygood
Copy link
Member

Please try to make your messages more concise.

@tfish2
Copy link
Mannequin Author

tfish2 mannequin commented Apr 8, 2022

Re AlexWaygood:

If these PEP-484 related things were so obvious that they would admit a compact description of the problem in 2-3 lines, these issues would likely have been identified much earlier. We would not be seeing them now, given that Python by and large is a somewhat mature language.

@ezio-melotti ezio-melotti transferred this issue from another repository Apr 10, 2022
@rhettinger
Copy link
Contributor

Closing this as being unspecific and unactionable.

To develop the ideas further consider launching a discussion on python-ideas or the typing-sig. If something matures, it would likely require a PEP because it changes changes decisions made in earlier typing PEPs.

One cannot just wish away the differences between reals in mathematics, Real in numbers.py, floats as used in typing, and the concrete float type implemented in the core language. There are practical limits on how much they can be harmonized without breaking existing code and tools.

@fischbacher
Copy link

(I would like to comment on this claim:

"One cannot just wish away the differences between reals in mathematics, Real in numbers.py, floats as used in typing, and the concrete float type implemented in the core language. There are practical limits on how much they can be harmonized without breaking existing code and tools."

Right now, we are in a situation where this function...:

def float_identity(x: float) -> float:
return float(x)

...fails to give two important guarantees:

  1. If x is a value recognized as being a float by static type checking, we could deduce:
    (x == x) <= (float_identity(x) == x). (I.e.: if x is equal to itself, then float_identity(x) must also be equal to x.)

  2. If x is a value recognized as being a float by static type checking, float_identity will actually return a value.

Note that this Python-specific problem that float currently means two observably-different things is not(!) shared by any other major programming language: All of C, C++, C#, Java, R[n]RS Scheme, Common Lisp, Haskell, all ML dialects, and quite a few more have one notion of "float". So, this is very much not about "wish[ing] away the differences between reals in mathematics ... and the concrete float type implemented in the core language"! Every other major language has come up with a satisfactory solution here - in the sense that authors have some authoritative reference documentation available that explains what a "float" is and how it works. (It might have a different name, such as "double", but the general contract always is: You can rely on these floating point numbers to behave as specified in the IEEE-754 floating point standard).

Python actually also has a notion of IEEE-754-1985 binary64 compliant floating point numbers - these are objects satisfying isinstance(type(x), float), which includes instances of subclasses such as numpy.float64.

Python is special - and indeed unique - in that it has a second notion of float, which is something entirely different.
Even worse, the way this second notion of float was introduced makes it currently impossible to express the claim
"this function is guaranteed to return an instance of the class float" as a static type annotation.

Ad: "To develop the ideas further consider launching a discussion on python-ideas or the typing-sig" - such procedural detail changes nothing about the observation that this quite clearly is a relevant open bug.

Python is a popular programming language in higher education. One important aspect of teaching computing is teaching the skill to reason about the behavior of code. With discrepancies such as this that convey a message along the lines of "reasoning about code is difficult, so let's just forget about that", Python unnecessarily positions itself as unsuitable for teaching computing.

@stevendaprano
Copy link
Member

stevendaprano commented May 2, 2022 via email

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

5 participants