pschanely / CrossHair

An analysis tool for Python that blurs the line between testing and type systems.
Other
1.03k stars 49 forks source link

Improve Support for Callable arguments using TypeVars #85

Open choct155 opened 3 years ago

choct155 commented 3 years ago

Very cool project, but I think there is something about the recursive case that may overlook invalid properties. I have made a gist here (I think the second property should fail?): https://gist.github.com/pschanely/cb5fafac16c433ea70ae70e539d87cf6

pschanely commented 3 years ago

Thank you for the bug report! Really, this sort of thing is exactly what I need, so please keep these coming along with any other feedback you can share.

Looking at the example, I think the first property should fail too, right?:

post: len(__return__) != len(a_vals)

The lengths are hopefully always equal.

But indeed, CrossHair doesn't find either of these right now. That's because its ability to generate counterexamples for higher order functions is extremely limited. Generating counterexamples with Callable arguments only works with "simple" datatypes, and even then it'll only sometimes come up with something. And for an example like yours with type variables in it, it just gives up immediately.

However, if we turn those type vars into something concrete and simple, it can sometimes handle recursive things like this. Try running this example where I've specialized it for the int->int case.

Now, you might say, golly, it doesn't seem like it'd be very hard to try substituting simple types for typevars and see if we can just get something to work. And, I'd agree! I just haven't thought enough about that case yet, or put effort into it. If you agree, let's repurpose this bug to work on better support for Callable arguments with TypeVars.