4 ms·

> 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

by 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.)
- neolog 5y ago
  Sure, I'm just saying that Mypy is a real type checker. The distinction is one of degree, not of kind. Writing a spec for Mypy wouldn't make its types more "true", just as deleting Haskell's spec wouldn't make its types less true types.
  - mananaysiempre 5y ago
    Still not necessarily true. The academic usage holds that the distinction between the true type systems and the pretenders is that the first are sound: a well-typed program either evaluates to a normal form (value) or fails to terminate, but can never get stuck (segfault, terminate with an uncaught exception, however your environment implements that). Of course, a gradual system like Mypy can never both be sound in this sense and remain gradual (which is a major selling point for Mypy), so for them the rule is usually amended with “provided the program is fully annotated” (and it should be obvious whether any given program is fully annotated or not, otherwise the system is just user-hostile regardless of how sound it is; at the very least it must be decidable). That is still obviously not satisfied for Mypy, because it doesn’t track exceptions (and including uncaught exceptions in normal forms would be useless because then no Python programs would ever get stuck). The actual guarantee Mypy is supposed to provide sounds kind of wimpy, like “never gets a TypeError that is not explicitly raised in user code”, but would still be useful regardless... Except that soundness is usually a pretty non-trivial theorem, and the lack of a readable specification for Mypy’s type system precludes it from being proven. While well-typed Haskell (or SML) programs can in fact crash from the user’s perspective, the possible sources of crashes are rare and avoidable enough (for Haskell, only non-exhaustive patterns and explicit use of undefined, error, or throw) that you can call them additional normal forms without making the whole thing trivial. Every other way an untyped program could get stuck is disallowed by the type system, and there is a proof (SML) or at least a proof sketch (Haskell) of that (although of course not every untyped program that can’t get stuck is allowed by the type system, that is impossible by Turing—Gödel). Even the horrendously complicated systems that GHC implements nowadays still have papers that prove their soundness for a good enough toy example that one walks away convinced that the real thing works just as well. So yes, there is a sense in which Mypy’s system is less “true” than SML’s or Haskell’s, and it is directly caused by (though not completely reducible to) the lack of a complete human-readable spec for both Mypy and Python itself. (I love Python to bits, but its object model is surreal and its only complete description is Objects/object.c together with Objects/typeobject.c.) If a wizard waved his wand and made every copy of the Haskell Report disappear, its type system would technically remain sound, but illegibly so to human mathematicians, thus it would in fact become less “true” in this sense than previously. Multiple implementations help, but I expect that without a prose spec it wouldn’t be easy to tell that GHC, UHC and Hugs implement the same system, the same way I have no idea if Mypy and Pytype do.
MillenialMan 5y ago
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.
rowanG077 5y ago
pythons type system, just like typescripts, is completely unsound. Haskell is also unsound because of unsafeCoerce. But that makes it very clear that what you are doing is unsafe. In python you very often write unsound code that passes the type checker. This means you cannot trust the type checker to catch type errors.
- Mehdi2277 5y ago
  The primary unsoundness is lack of types. The type checkers have strictness settings that will error if you are missing any types even types internal to a function/3rd party library used. The highest strictness settings what places are there that still are unsound? The very dynamic behavior that sometimes happens has two main impacts. Either type checker doesn't understand it and on high strictness settings will treat it as an error or you need to extend the type system use plugins (mypy has some plugins for very dynamic libraries to define custom rules). Practically most large programs today can not pass maximal strictness settings as too many libraries lack type hints. But that's not a fundamental issue of python type system just a needed improvement of the ecosystem. Type hints are gradually growing and some major libraries have had noticeable improvements in the past year (numpy only started to have some types around 1.20).

by neolog 5y ago

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.)

neolog 5y ago
Sure, I'm just saying that Mypy is a real type checker. The distinction is one of degree, not of kind. Writing a spec for Mypy wouldn't make its types more "true", just as deleting Haskell's spec wouldn't make its types less true types.
- mananaysiempre 5y ago
  Still not necessarily true. The academic usage holds that the distinction between the true type systems and the pretenders is that the first are sound: a well-typed program either evaluates to a normal form (value) or fails to terminate, but can never get stuck (segfault, terminate with an uncaught exception, however your environment implements that). Of course, a gradual system like Mypy can never both be sound in this sense and remain gradual (which is a major selling point for Mypy), so for them the rule is usually amended with “provided the program is fully annotated” (and it should be obvious whether any given program is fully annotated or not, otherwise the system is just user-hostile regardless of how sound it is; at the very least it must be decidable). That is still obviously not satisfied for Mypy, because it doesn’t track exceptions (and including uncaught exceptions in normal forms would be useless because then no Python programs would ever get stuck). The actual guarantee Mypy is supposed to provide sounds kind of wimpy, like “never gets a TypeError that is not explicitly raised in user code”, but would still be useful regardless... Except that soundness is usually a pretty non-trivial theorem, and the lack of a readable specification for Mypy’s type system precludes it from being proven. While well-typed Haskell (or SML) programs can in fact crash from the user’s perspective, the possible sources of crashes are rare and avoidable enough (for Haskell, only non-exhaustive patterns and explicit use of undefined, error, or throw) that you can call them additional normal forms without making the whole thing trivial. Every other way an untyped program could get stuck is disallowed by the type system, and there is a proof (SML) or at least a proof sketch (Haskell) of that (although of course not every untyped program that can’t get stuck is allowed by the type system, that is impossible by Turing—Gödel). Even the horrendously complicated systems that GHC implements nowadays still have papers that prove their soundness for a good enough toy example that one walks away convinced that the real thing works just as well. So yes, there is a sense in which Mypy’s system is less “true” than SML’s or Haskell’s, and it is directly caused by (though not completely reducible to) the lack of a complete human-readable spec for both Mypy and Python itself. (I love Python to bits, but its object model is surreal and its only complete description is Objects/object.c together with Objects/typeobject.c.) If a wizard waved his wand and made every copy of the Haskell Report disappear, its type system would technically remain sound, but illegibly so to human mathematicians, thus it would in fact become less “true” in this sense than previously. Multiple implementations help, but I expect that without a prose spec it wouldn’t be easy to tell that GHC, UHC and Hugs implement the same system, the same way I have no idea if Mypy and Pytype do.

MillenialMan 5y ago

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.

rowanG077 5y ago

pythons type system, just like typescripts, is completely unsound. Haskell is also unsound because of unsafeCoerce. But that makes it very clear that what you are doing is unsafe. In python you very often write unsound code that passes the type checker. This means you cannot trust the type checker to catch type errors.

Mehdi2277 5y ago
The primary unsoundness is lack of types. The type checkers have strictness settings that will error if you are missing any types even types internal to a function/3rd party library used. The highest strictness settings what places are there that still are unsound? The very dynamic behavior that sometimes happens has two main impacts. Either type checker doesn't understand it and on high strictness settings will treat it as an error or you need to extend the type system use plugins (mypy has some plugins for very dynamic libraries to define custom rules). Practically most large programs today can not pass maximal strictness settings as too many libraries lack type hints. But that's not a fundamental issue of python type system just a needed improvement of the ecosystem. Type hints are gradually growing and some major libraries have had noticeable improvements in the past year (numpy only started to have some types around 1.20).