3 ms·

Python types are unprovable, since the type of a variable can change at runtime. It's the Halting problem. All you can do is enforce types on static function bo

Python types are unprovable, since the type of a variable can change at runtime. It's the Halting problem. All you can do is enforce types on static function boundaries - but that doesn't prove you won't send a different type through the boundary at runtime. GHC types are mathematically provable. Types are guaranteed to stay within your defnitions, so you can analyze the type graph without ever having to run the program.

neolog 5y ago
> since the type of a variable can change at runtime. Can you give an example of that? Mypy catches this: def addsome(val: int) -> int: val += 1.1 # tmp.py:2: error: Incompatible types in assignment (expression has type "float", variable has type "int") return val I'm sure there are cases where it doesn't notice, but afaik those are considered bugs. Doesn't Haskell have bugs?
- MillenialMan 5y ago
  Provided you don't circumvent strict typing, no, Haskell does not have typing bugs. Or rather, it has so few that you can functionally behave as if the type checking is flawless. One of the main benefits of strict typing is that confidence - 95% coverage is helpful, but it's just helpful. 100% coverage allows you to program completely differently. It's also static - does Mypy throw that error when that program is statically analysed, or at runtime?
  - neolog 5y ago
    Mypy shows that error statically.
dragonwriter 5y ago
> Python types are unprovable, since the type of a variable can change at runtime You can certainly statically identify places where such changes are possible and the possible changes, in fact, Python static typecheckers do this. > It's the Halting problem. The Halting problem is a real thing, but you can simply bail out on any path that reaches a certain depth without resolution and fallback to the broadest possible type (failing narrower constraints) to avoid it.
- MillenialMan 5y ago
  You can identify some places changes are possible, but the problem is fundamentally unprovable, because of the Halting problem. You can't just hand-wave that away by saying, "we can use tricks to get 95% coverage." Ok, but if the type graph is not a provable entity that you can derive without simulating the program, you've sacrificed the fundamental point of C-style types, and that means you can never operate on them in the same way you can with C.

neolog 5y ago

> since the type of a variable can change at runtime. Can you give an example of that? Mypy catches this: def addsome(val: int) -> int: val += 1.1 # tmp.py:2: error: Incompatible types in assignment (expression has type "float", variable has type "int") return val I'm sure there are cases where it doesn't notice, but afaik those are considered bugs. Doesn't Haskell have bugs?

MillenialMan 5y ago
Provided you don't circumvent strict typing, no, Haskell does not have typing bugs. Or rather, it has so few that you can functionally behave as if the type checking is flawless. One of the main benefits of strict typing is that confidence - 95% coverage is helpful, but it's just helpful. 100% coverage allows you to program completely differently. It's also static - does Mypy throw that error when that program is statically analysed, or at runtime?
- neolog 5y ago
  Mypy shows that error statically.

dragonwriter 5y ago

> Python types are unprovable, since the type of a variable can change at runtime You can certainly statically identify places where such changes are possible and the possible changes, in fact, Python static typecheckers do this. > It's the Halting problem. The Halting problem is a real thing, but you can simply bail out on any path that reaches a certain depth without resolution and fallback to the broadest possible type (failing narrower constraints) to avoid it.

MillenialMan 5y ago
You can identify some places changes are possible, but the problem is fundamentally unprovable, because of the Halting problem. You can't just hand-wave that away by saying, "we can use tricks to get 95% coverage." Ok, but if the type graph is not a provable entity that you can derive without simulating the program, you've sacrificed the fundamental point of C-style types, and that means you can never operate on them in the same way you can with C.