[Python-ideas] Statically checking purity of functions

[Christoph Groth]

Cory Benfield wrote:

> Here’s where this falls down (NB, the print is just a simple 
> example of non-purity, but you can imagine that you can just do 
> arbitrary code).
>
> class SideEffectyInt(int):
>     def __add__(self, other):
>         if other == 3:
>             print(“YAY")
>         return super().__add__(other)

Of course, an instance of SideEffectInt is also an instance of int 
and as such mypy will not complain when it is passed to the "add" 
function.

However, using the above technique any type checking by mypy can 
be circumvented.  Mypy will happily nod through the following 
program:

class FloatingInt(int):
    def __add__(self, other):
        return float(super().__add__(other))

def add(a: int, b: int) -> int:
    return a + b

print(add(FloatingInt(1), 2))

However, if we change the above class definition to

class FloatingInt(int):
    def __add__(self, other) -> float:
        return float(super().__add__(other))

mypy will start to complain with the following error:

test.py:2: error: Return type of "__add__" incompatible with 
supertype "int"

Now, mypy could be probably more strict and flag already the first 
definition of FloatingInt.__add__() as an error, because it knows 
(as the above error message shows) what its return type should be 
From inheritance.  It also knows that float()  produces a float, 
since it does not accept

def foo() -> int:
    return float(5)

I guess it's a choice of mypy not to complain about bits of code 
that don't use type declarations.

In an exactly analogous way, mypy could detect that calling 
print() in SideEffectlyInt.__add__ is incompatible with the 
(supposedly declared) purity of int.__add__() if SideEffectlyInt 
was declared as:

class SideEffectyInt(int):
    @pure
    def __add__(self, other):
        if other == 3:
            print(“YAY")
        return super().__add__(other)

And just like before, if mypy was more strict, it could detect the 
purity-breaking of SideEffectyInt.__add__() from inheritance.

> This SideEffectyInt() object is suitable for passing into your 
> pure “add” function, but has an impure add logic. I’m not sure 
> how mypy could resolve this problem: I presume it’d need purity 
> declarations for every possible function on every type *and* the 
> ability to see all function invocations, which is pretty 
> difficult given that Python’s dynamism makes it possible to 
> invoke arbitrary functions.

This is correct, but I believe your statement remains correct when 
one replaces "purity" by "typing": In order to verify with 
certainty that the typing is correct for a function, mypy would 
have to know the typing declaration of every function that is 
called inside it.

> So I don’t really see how this pure decorator could *enforce* 
> purity.

It seems to me that purity could be enforced to the same degree 
that correct typing can be enforced.  In other words, the goal of 
mypy seems not to be to prove that typing of a program is 
consistent (Python is too dynamic for that), but rather to help 
finding possible errors.  It seems to me that the same service 
could be provided for purity.  That should be good enough for many 
applications.

In that spirit, perhaps it would make more sense to assume purity 
by default if unspecified (just like mypy assumes type correctness 
when no typing information is present), and have both "pure" and 
"impure" (dirty? ;-) decorators.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 818 bytes
Desc: not available
URL: <http://mail.python.org/pipermail/python-ideas/attachments/20160609/fdc01fcd/attachment-0001.sig>