3 ms·

Stronger types for Python

25 points by andrewcooke 16y ago

andrewcooke 16y ago
Thought people might find this amusing / interesting (wish I had written it for April 1... although it does work). It's a spin-off from the use of type annotations to guide the interpretation of JSON data (Pytyp will marshal JSON/YAML data into Python classes, which is useful if you're using JSON to talk to some kind of service). [Edit: Optional, product and sum types are supported, along with simple polymorphism. There's currently no type variables and no dispatch by type - although I think both could be added]
- masklinn 16y ago
  It's really cool that optional, product and sum types are supported. Does it work correctly with abstract base classes as well? (I'm expecting yes, just checking). Could it work with structural types as well? That would strike me as "more pythonic", and I've always been surprised that no Python type-annotation scheme can handle structural specs (though abcs are a step in the right direction).
  - andrewcooke 16y ago
    Thanks. I assume it works with ABCs, but haven't actually tried it (I ran out of time and wanted to publish something as a first release this weekend). Structural types would make more sense for general use, but not for what the larger library was actually intended for (I think) so I never really looked in that direction (and I don't have any ideas on how to extend it to include them, either). I do have an idea for a kind of type matching across sum types which will be quite neat if it works...
riobard 16y ago
If type annotations are fully respected that programmers code it like a statically-typed language (no type change for a variable in scope), will it be possible to AOT compile it?
- rabidsnail 16y ago
  In theory you should be able to AOT compile python now, with type inference. There are cases where the types are not inferable, as there are cases where the programmer does not provide type hints. But I think an approach similar to clojure's where types are inferred when possible, type hints can be provided optionally, and runtime reflection is used as a fallback when the type cannot be determined ahead of time is a good approach. You generally don't worry about types in clojure any more than you worry about types in python; you only add type hints in performance-sensitive code in cases where the compiler can't figure out the types on its own.
- andrewcooke 16y ago
  You could, but it's not really worth it - you'd end up with a pretty boring language. Also, JITs (in particular PyPy) should be able to get decent performance in the near future without asking the programmer to do anything unusual. In simple terms they assume that types are whatever they find and compile for that (occasionally the assumption is wrong, and they have to correct and do something else, but most of the time you get good performance just by pretending the program was written with static types, even though it wasn't). Obviously it's more complex than that, but you get the idea (the hard part is largely reducing the number of times you need to check you're assumptions are still OK)
ubernostrum 16y ago
Except these aren't "strong" types. Python has those. These are pretend-static types.
- andrewcooke 16y ago
  Sure; in the docs I call them "runtime verification of type annotations".
rubergly 16y ago
I'm a university student, and as a thesis project I've been working on a static type-checker for Python. I'm interested to see if people think this would be of practical good (my advisor and I certainly think it could be).
- m0th87 16y ago
  I would be extremely excited about a static type checker, and given how favorably Python is seen in this community, plenty of others would be here as well. So please do post when you have a finished product! I'm sure you've seen these already, but if not, they would be highly relevant: * GvR did a commentary on some of the challenges that would arise with an optional type system: http://www.artima.com/weblogs/viewpost.jsp?thread=85551 http://www.artima.com/weblogs/viewpost.jsp?thread=85551 * Python 3 included some syntactic changes precisely to support things like type checking: http://www.python.org/dev/peps/pep-3107/ http://www.python.org/dev/peps/pep-3107/
  - rubergly 16y ago
    I indeed have read Rossum's blog posts, but I haven't been following Python 3 at all, and only found out about annotations after looking at Pytyp, so that's definitely interesting and helpful, thanks.
- andrewcooke 16y ago
  if you mean inferring types from un-annotated programs, it has been tried a couple of times - if you search around you can find other people's attempts (i think there is a thesis and a dead project on the net). [To answer your question; I think it would be useful (I once started work on something similar myself, but never got to actually unifying types). However, the fact that other people have tried and failed to be come popular suggests that there are (more) problems (than you might expect).]
  - rubergly 16y ago
    I'm not trying to do type inference (yet, that might be a direction of expansion for next year), and, anyway, my program is demanding type annotations in docstrings.

25 points by andrewcooke 16y ago

Thought people might find this amusing / interesting (wish I had written it for April 1... although it does work). It's a spin-off from the use of type annotations to guide the interpretation of JSON data (Pytyp will marshal JSON/YAML data into Python classes, which is useful if you're using JSON to talk to some kind of service). [Edit: Optional, product and sum types are supported, along with simple polymorphism. There's currently no type variables and no dispatch by type - although I think both could be added]

masklinn 16y ago
It's really cool that optional, product and sum types are supported. Does it work correctly with abstract base classes as well? (I'm expecting yes, just checking). Could it work with structural types as well? That would strike me as "more pythonic", and I've always been surprised that no Python type-annotation scheme can handle structural specs (though abcs are a step in the right direction).
- andrewcooke 16y ago
  Thanks. I assume it works with ABCs, but haven't actually tried it (I ran out of time and wanted to publish something as a first release this weekend). Structural types would make more sense for general use, but not for what the larger library was actually intended for (I think) so I never really looked in that direction (and I don't have any ideas on how to extend it to include them, either). I do have an idea for a kind of type matching across sum types which will be quite neat if it works...

riobard 16y ago

If type annotations are fully respected that programmers code it like a statically-typed language (no type change for a variable in scope), will it be possible to AOT compile it?

rabidsnail 16y ago
In theory you should be able to AOT compile python now, with type inference. There are cases where the types are not inferable, as there are cases where the programmer does not provide type hints. But I think an approach similar to clojure's where types are inferred when possible, type hints can be provided optionally, and runtime reflection is used as a fallback when the type cannot be determined ahead of time is a good approach. You generally don't worry about types in clojure any more than you worry about types in python; you only add type hints in performance-sensitive code in cases where the compiler can't figure out the types on its own.
andrewcooke 16y ago
You could, but it's not really worth it - you'd end up with a pretty boring language. Also, JITs (in particular PyPy) should be able to get decent performance in the near future without asking the programmer to do anything unusual. In simple terms they assume that types are whatever they find and compile for that (occasionally the assumption is wrong, and they have to correct and do something else, but most of the time you get good performance just by pretending the program was written with static types, even though it wasn't). Obviously it's more complex than that, but you get the idea (the hard part is largely reducing the number of times you need to check you're assumptions are still OK)

ubernostrum 16y ago

Except these aren't "strong" types. Python has those. These are pretend-static types.

andrewcooke 16y ago
Sure; in the docs I call them "runtime verification of type annotations".

rubergly 16y ago

I'm a university student, and as a thesis project I've been working on a static type-checker for Python. I'm interested to see if people think this would be of practical good (my advisor and I certainly think it could be).

m0th87 16y ago
I would be extremely excited about a static type checker, and given how favorably Python is seen in this community, plenty of others would be here as well. So please do post when you have a finished product! I'm sure you've seen these already, but if not, they would be highly relevant: * GvR did a commentary on some of the challenges that would arise with an optional type system: http://www.artima.com/weblogs/viewpost.jsp?thread=85551 http://www.artima.com/weblogs/viewpost.jsp?thread=85551 * Python 3 included some syntactic changes precisely to support things like type checking: http://www.python.org/dev/peps/pep-3107/ http://www.python.org/dev/peps/pep-3107/
- rubergly 16y ago
  I indeed have read Rossum's blog posts, but I haven't been following Python 3 at all, and only found out about annotations after looking at Pytyp, so that's definitely interesting and helpful, thanks.
andrewcooke 16y ago
if you mean inferring types from un-annotated programs, it has been tried a couple of times - if you search around you can find other people's attempts (i think there is a thesis and a dead project on the net). [To answer your question; I think it would be useful (I once started work on something similar myself, but never got to actually unifying types). However, the fact that other people have tried and failed to be come popular suggests that there are (more) problems (than you might expect).]
- rubergly 16y ago
  I'm not trying to do type inference (yet, that might be a direction of expansion for next year), and, anyway, my program is demanding type annotations in docstrings.