5 ms·

What always annoys me to no end is when people complain that python type hints are not runtime enforced, when this is quite normal for most statically typed lan

by zohch 5y ago

What always annoys me to no end is when people complain that python type hints are not runtime enforced, when this is quite normal for most statically typed languages: C++, go, rust. Python already had runtime type checking mechanisms and the use of these does inform the behavior of static type checkers for python like mypy. All that being said, Beartype is really nifty and seems quite useful.

mjburgess 5y ago
The spirit of a type-system is that invalid code never runs. The compilation step in static languages type-checks such that the compiled-instructions wont run if the source-code is invalid. Since this isnt how python works, one would reasonably expect the spirit of a type system to be preserved -- ie., to enforce runtime checks.
- zohch 5y ago
  > The spirit of a type-system is that invalid code never runs. > The compilation step in static languages type-checks such that the compiled-instructions wont run if the source-code is invalid. Nothing is forcing anyone to run code that does not pass type checking with `mypy --strict`. > Since this isnt how python works, one would reasonably expect the spirit of a type system to be preserved -- ie., to enforce runtime checks. Python already had mechanisms for this, which again, as I said, already informs the static type checking mechanisms. Also, no, this is not what I expect from the type hints, this is not what I felt was missing from python before type hints. What I want from type hints and in python in general is static type checking, I want to know, without executing one single line of code, if I have type errors, that is the key selling point of mypy and type hints to me and the key deficiency that python had without type hints and mypy. I already had every ability to do runtime type checking in python before type hints and mypy, and they were woefully inadequate in comparison to static type checking.
  - lozenge 5y ago
    Is the standard library type checked? Are there still mistakes in the typeshed like 2**-1 is int?
    - zohch 5y ago
      > Is the standard library type checked? There are type hints for the standard library and using `--strict` works just fine if that is all you are using. This does not preclude bugs from the standard library or errors in types but bugs in a statically typed language's compiler also does not defeat the purpose of static typing either and having a static typed language does not eliminate the possibility of bugs in the compiler or standard library either. It seems people forget that reinterpret_cast, void * (c++), Object (java), (interface{}) (golang) exists. If all you are using is the standard library then you will be able to write much safer code in python than in golang, given it passes static type validation. At least python's type system has generics. > Are there still mistakes in the typeshed like 2*-1 is int? I'm sure there are still mistakes, just like I'm sure there are still bugs in most compilers.
- pawelmurias 5y ago
  C++ type system allows invalid code (that uses freed or uninitialized memory) to run and just do weird incorrect things.
  - eru 5y ago
    Sort-of. That code is invalid in some informal sense, but not invalid as far as the formal typesystem is concerned. There's also something about 'soundness' one could say.
    - zohch 5y ago
      You can compile code using reinterpret cast "incorrectly" in c++ just fine.
      - eru 5y ago
        Maybe, but isn't that explicitly opting out of the typesystem's guarantees?
  - choeger 5y ago
    So does every Turing-complete language with non-termination. Type systems are decidable and thus cannot, by definition, rule out all errors. Instead, they look at a subset of possible errors. This subset is provably eliminated from valid code. "Dynamically typed" languages reduce that subset to the empty set.
guenthert 5y ago
Am I unreasonable in hoping for optional type hints to be taken advantage of by a compiler to produce correct, optimized code, similar to what (sufficiently smart) Common Lisp compilers do?
darthrupert 5y ago
This comment is in the top #10 of the stupidest things I've read on this site. Congratulations! As personal advice, I suggest not being annoyed about a thing you're totally wrong about.

by zohch 5y ago

mjburgess 5y ago

The spirit of a type-system is that invalid code never runs. The compilation step in static languages type-checks such that the compiled-instructions wont run if the source-code is invalid. Since this isnt how python works, one would reasonably expect the spirit of a type system to be preserved -- ie., to enforce runtime checks.

zohch 5y ago
> The spirit of a type-system is that invalid code never runs. > The compilation step in static languages type-checks such that the compiled-instructions wont run if the source-code is invalid. Nothing is forcing anyone to run code that does not pass type checking with `mypy --strict`. > Since this isnt how python works, one would reasonably expect the spirit of a type system to be preserved -- ie., to enforce runtime checks. Python already had mechanisms for this, which again, as I said, already informs the static type checking mechanisms. Also, no, this is not what I expect from the type hints, this is not what I felt was missing from python before type hints. What I want from type hints and in python in general is static type checking, I want to know, without executing one single line of code, if I have type errors, that is the key selling point of mypy and type hints to me and the key deficiency that python had without type hints and mypy. I already had every ability to do runtime type checking in python before type hints and mypy, and they were woefully inadequate in comparison to static type checking.
- lozenge 5y ago
  Is the standard library type checked? Are there still mistakes in the typeshed like 2**-1 is int?
  - zohch 5y ago
    > Is the standard library type checked? There are type hints for the standard library and using `--strict` works just fine if that is all you are using. This does not preclude bugs from the standard library or errors in types but bugs in a statically typed language's compiler also does not defeat the purpose of static typing either and having a static typed language does not eliminate the possibility of bugs in the compiler or standard library either. It seems people forget that reinterpret_cast, void * (c++), Object (java), (interface{}) (golang) exists. If all you are using is the standard library then you will be able to write much safer code in python than in golang, given it passes static type validation. At least python's type system has generics. > Are there still mistakes in the typeshed like 2*-1 is int? I'm sure there are still mistakes, just like I'm sure there are still bugs in most compilers.
pawelmurias 5y ago
C++ type system allows invalid code (that uses freed or uninitialized memory) to run and just do weird incorrect things.
- eru 5y ago
  Sort-of. That code is invalid in some informal sense, but not invalid as far as the formal typesystem is concerned. There's also something about 'soundness' one could say.
  - zohch 5y ago
    You can compile code using reinterpret cast "incorrectly" in c++ just fine.
    - eru 5y ago
      Maybe, but isn't that explicitly opting out of the typesystem's guarantees?
- choeger 5y ago
  So does every Turing-complete language with non-termination. Type systems are decidable and thus cannot, by definition, rule out all errors. Instead, they look at a subset of possible errors. This subset is provably eliminated from valid code. "Dynamically typed" languages reduce that subset to the empty set.

guenthert 5y ago

Am I unreasonable in hoping for optional type hints to be taken advantage of by a compiler to produce correct, optimized code, similar to what (sufficiently smart) Common Lisp compilers do?

darthrupert 5y ago

This comment is in the top #10 of the stupidest things I've read on this site. Congratulations! As personal advice, I suggest not being annoyed about a thing you're totally wrong about.