9 ms·

The thing with Python types is that they are “type hints” and not true types, hints is the keyword. There’s also two type checker implementations. As they are

The thing with Python types is that they are “type hints” and not true types, hints is the keyword. There’s also two type checker implementations. As they are hints it means you can still pass in wrong values in some situations and what types check on one implementation may not type check with the other implementation. So the types are superficial only in Python. The paper “Python 3 types in the wild” at https://news.ycombinator.com/item?id=26788177 https://news.ycombinator.com/item?id=26788177 is a good read. I enjoyed reading it and found it useful. I’m a fan of types as the compiler tells me I made a mistake and blocks me making mistakes. You can use the type system to make certain errors unrepeatable (impossible to make). With that my preference is use a language where types are first class rather than a language trying to retrofit some loose form of type checking on top which is nothing more than linting. Being a fan of strongly typed languages I was eager to use types in Python when I had to involuntarily use Python. After a few instances of putting in type hints and things type checking when they shouldn’t I mainly don’t bother with them now outside of data classes as they where not catching bugs I wanted so still getting runtime errors.

joshuamorton 5y ago
> As they are hints it means you can still pass in wrong values in some situations and what types check on one implementation may not type check with the other implementation. So the types are superficial only in Python. Could you elaborate. When can you pass in wrong values? The type checkers aren't always precisely the same (some do inference, mypy doesn't), but the cases where they disagree are usually because one is correct and one wants more information, not because you're able to do the wrong thing despite having annotations.
- takeda 5y ago
  I believe GP means that they are not checked at runtime. But I don't think that matters much in case of finding bugs, because you run mypy and it will scream that you are assigning wrong type. I use it whenever I can and it helped me find many bugs in the code (especially not checking if value is None through the Optional). It also makes refactoring your code in IDEs that understand types (like PyCharm) much much easier.
  - neolog 5y ago
    > I believe GP means that they are not checked at runtime. Haskell types aren't checked at runtime either, so that can't be it. Python has runtime type checks that do happen at runtime, so maybe it's Haskell that doesn't have types.
    - takeda 5y ago
      What Haskell does and other statically compiled languages is figuring the type before program runs. Once it does it is impossible to have a different type in the code. Python is dynamically typed. That means everything including things like string or integer is stored as a structure with a type. The checking of the type happens at runtime. This is major reason why languages like Python are so much slower than statically typed languages. The annotated type in Python is providing mechanism of figuring out types before code is run, this helps finding bugs, but these types are not used during normal operation[1], but that doesn't stop them from being useful for finding bugs in the code or helping with refactoring. [1] There are some packages that implement some runtime checks, but they IMO are waste of time. Basically they are ensuring that type problems that tool like mypy would detect also will cause your code to crash. It also add performance penalty as well. There's also mypyc, code that compiles python code that using types increasing its performance. It is currently used to compile mypy increasing its performance by a factor of 4 I believe. It also makes some python features unavailable if you want to use it (https://mypyc.readthedocs.io/en/latest/differences_from_python.html https://mypyc.readthedocs.io/en/latest/differences_from_pyth...)
      - neolog 5y ago
        > The checking of the type happens at runtime. Mypy checks the type before runtime, just like GHC does. Python also checks during runtime, but Haskell doesn't have that feature. Right? > This is major reason why languages like Python are so much slower than statically typed languages. Julia's dynamic typing, and hence its ability to do specialization using runtime information, is part of why it can (sometimes) beat Fortran in numerical performance.
- tiew9Vii 5y ago
  I had a situation I gave a method argument a type hint, I then called that method with a completely different type by mistake. The type checker didn’t pick up the error so I got a runtime exception where I’d expect a type checker to catch the issue. I don’t have the specific example, it was something I observed not so long ago, said well that’s shit, fixed my code issue and moved on. Not being a huge fan of Python outside of small scripts and only using Python as told to use Python I took little interest in the detail as was a case of just get the job done and move on. It’s been a while since I read the paper I shared but think that mentions it something similar if I remember correctly.
Mehdi2277 5y ago
You can have strict lint checks enforced with pre-commit hooks/ci checks. My current team I've been adding type checker tests (mypy + pyright) and for now as we're missing types I have type checkers on a nice rule of any prs you make must decrease the number of type errors (by 5, but up to you how harsh you want to be) in master to be merged forcing people to add more types. Once the type hints eventually hit 0 on our current strictness settings I'll gradually increase strictness requirements higher. Full strictness of no Any's anywhere including intermediates isn't really possible as a number of 3rd party packages lack types (tensorflow is especially sad with types). But we can get many of the strictness and that should cover a large number of basic bugs.
- deleted 5y ago
  [deleted]
pansa2 5y ago
> There’s also two type checker implementations. Four: Mypy, Pyre, Pyright and Pytype.
- gota 5y ago
  I'd expect someone to name theirs Thypon
neolog 5y ago
> The thing with Python types is that they are “type hints” and not true types Python has several type checkers, as does Haskell, each with different soundness properties. What makes GHC's type checking more "true" than Mypy's or Pytype's or Pyright's?
- tome 5y ago
  Haskell doesn't have "several type checkers". It has several compilers, and if you use a particular compiler then you use its type checker and not the type checker of another compiler. (There is also Liquid Haskell, but it doesn't check Haskell types, it checks Liquid Haskell types.)
  - neolog 5y ago
    Could you explain the significance of the distinction you're making?
    - tome 5y ago
      You first!
- mananaysiempre 5y ago
  Every correct Haskell ’98 or Haskell 2010 implementation (not that a lot of them are still alive) accepts exactly the same set of programs, because that set is described in the Report. Every correct Standard ML implementation (of which there are still a few, surprisingly) with extensions turned off accepts exactly the same set of programs, because that set is described in the Definition. GHC with its innumerable extensions and impenetrable (if well-defined) typing rules is and was always intended to be a testbed for wild type system ideas; that whatever it accepts became the received superset of standard Haskell (of which it is the only implementation) is in my opinion a failure of the Haskell community and the very thing that turned me away from Haskell after several years. On the other hand, the only real description of what Mypy accepts is the source code of Mypy, and while many interesting programs that fall into that set also happen to be accepted by Pytype or whatever else, it’s not in any useful sense a bug if some are not. There’s also no practical way to tell if an arbitrary program is accepted except to try throwing it into the typechecker, because there is no human-adapted description of what constitutes being accepted. None of which is to say that Mypy is not useful. It is useful, tremendously so. But as far as maturity of type systems in Haskell or SML goes, it’s not even in the same league. (So that this is not taken as academic elitism, neither are Scala, OCaml, or Typed Racket.)

joshuamorton 5y ago

> As they are hints it means you can still pass in wrong values in some situations and what types check on one implementation may not type check with the other implementation. So the types are superficial only in Python. Could you elaborate. When can you pass in wrong values? The type checkers aren't always precisely the same (some do inference, mypy doesn't), but the cases where they disagree are usually because one is correct and one wants more information, not because you're able to do the wrong thing despite having annotations.

takeda 5y ago
I believe GP means that they are not checked at runtime. But I don't think that matters much in case of finding bugs, because you run mypy and it will scream that you are assigning wrong type. I use it whenever I can and it helped me find many bugs in the code (especially not checking if value is None through the Optional). It also makes refactoring your code in IDEs that understand types (like PyCharm) much much easier.
- neolog 5y ago
  > I believe GP means that they are not checked at runtime. Haskell types aren't checked at runtime either, so that can't be it. Python has runtime type checks that do happen at runtime, so maybe it's Haskell that doesn't have types.
  - takeda 5y ago
    What Haskell does and other statically compiled languages is figuring the type before program runs. Once it does it is impossible to have a different type in the code. Python is dynamically typed. That means everything including things like string or integer is stored as a structure with a type. The checking of the type happens at runtime. This is major reason why languages like Python are so much slower than statically typed languages. The annotated type in Python is providing mechanism of figuring out types before code is run, this helps finding bugs, but these types are not used during normal operation[1], but that doesn't stop them from being useful for finding bugs in the code or helping with refactoring. [1] There are some packages that implement some runtime checks, but they IMO are waste of time. Basically they are ensuring that type problems that tool like mypy would detect also will cause your code to crash. It also add performance penalty as well. There's also mypyc, code that compiles python code that using types increasing its performance. It is currently used to compile mypy increasing its performance by a factor of 4 I believe. It also makes some python features unavailable if you want to use it (https://mypyc.readthedocs.io/en/latest/differences_from_python.html https://mypyc.readthedocs.io/en/latest/differences_from_pyth...)
    - neolog 5y ago
      > The checking of the type happens at runtime. Mypy checks the type before runtime, just like GHC does. Python also checks during runtime, but Haskell doesn't have that feature. Right? > This is major reason why languages like Python are so much slower than statically typed languages. Julia's dynamic typing, and hence its ability to do specialization using runtime information, is part of why it can (sometimes) beat Fortran in numerical performance.
tiew9Vii 5y ago
I had a situation I gave a method argument a type hint, I then called that method with a completely different type by mistake. The type checker didn’t pick up the error so I got a runtime exception where I’d expect a type checker to catch the issue. I don’t have the specific example, it was something I observed not so long ago, said well that’s shit, fixed my code issue and moved on. Not being a huge fan of Python outside of small scripts and only using Python as told to use Python I took little interest in the detail as was a case of just get the job done and move on. It’s been a while since I read the paper I shared but think that mentions it something similar if I remember correctly.

Mehdi2277 5y ago

You can have strict lint checks enforced with pre-commit hooks/ci checks. My current team I've been adding type checker tests (mypy + pyright) and for now as we're missing types I have type checkers on a nice rule of any prs you make must decrease the number of type errors (by 5, but up to you how harsh you want to be) in master to be merged forcing people to add more types. Once the type hints eventually hit 0 on our current strictness settings I'll gradually increase strictness requirements higher. Full strictness of no Any's anywhere including intermediates isn't really possible as a number of 3rd party packages lack types (tensorflow is especially sad with types). But we can get many of the strictness and that should cover a large number of basic bugs.

deleted 5y ago
[deleted]

pansa2 5y ago

> There’s also two type checker implementations. Four: Mypy, Pyre, Pyright and Pytype.

gota 5y ago
I'd expect someone to name theirs Thypon

neolog 5y ago

> The thing with Python types is that they are “type hints” and not true types Python has several type checkers, as does Haskell, each with different soundness properties. What makes GHC's type checking more "true" than Mypy's or Pytype's or Pyright's?

tome 5y ago
Haskell doesn't have "several type checkers". It has several compilers, and if you use a particular compiler then you use its type checker and not the type checker of another compiler. (There is also Liquid Haskell, but it doesn't check Haskell types, it checks Liquid Haskell types.)
- neolog 5y ago
  Could you explain the significance of the distinction you're making?
  - tome 5y ago
    You first!
mananaysiempre 5y ago
Every correct Haskell ’98 or Haskell 2010 implementation (not that a lot of them are still alive) accepts exactly the same set of programs, because that set is described in the Report. Every correct Standard ML implementation (of which there are still a few, surprisingly) with extensions turned off accepts exactly the same set of programs, because that set is described in the Definition. GHC with its innumerable extensions and impenetrable (if well-defined) typing rules is and was always intended to be a testbed for wild type system ideas; that whatever it accepts became the received superset of standard Haskell (of which it is the only implementation) is in my opinion a failure of the Haskell community and the very thing that turned me away from Haskell after several years. On the other hand, the only real description of what Mypy accepts is the source code of Mypy, and while many interesting programs that fall into that set also happen to be accepted by Pytype or whatever else, it’s not in any useful sense a bug if some are not. There’s also no practical way to tell if an arbitrary program is accepted except to try throwing it into the typechecker, because there is no human-adapted description of what constitutes being accepted. None of which is to say that Mypy is not useful. It is useful, tremendously so. But as far as maturity of type systems in Haskell or SML goes, it’s not even in the same league. (So that this is not taken as academic elitism, neither are Scala, OCaml, or Typed Racket.)