PyCon US 2021 Recordings are Available • Hacker News Board

Re: PyCon US 2021 Recordings are Available

#101

Post by gota » Sun, Jun 06, 2021, 6:28 AM UTC

pansa2 wrote: post #53

tiew9Vii wrote: post #29

Earlier quoted context omitted.

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…

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

I'd expect someone to name theirs Thypon

Re: PyCon US 2021 Recordings are Available

#102

Post by Mehdi2277 » Sun, Jun 06, 2021, 9:30 PM UTC

rowanG077 wrote: post #91

neolog wrote: post #56

Earlier quoted context omitted.

> 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?

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.

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

Re: PyCon US 2021 Recordings are Available

#103

Post by MillenialMan » Mon, Jun 07, 2021, 2:47 PM UTC

neolog wrote: post #95

MillenialMan wrote: post #82

Earlier quoted context omitted.

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 prog…

> 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?

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?

Re: PyCon US 2021 Recordings are Available

#104

Post by neolog » Mon, Jun 07, 2021, 9:24 PM UTC

MillenialMan wrote: post #103

neolog wrote: post #95

Earlier quoted context omitted.

> 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?

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 sta…

Mypy shows that error statically.

Re: PyCon US 2021 Recordings are Available

#105

Post by dragonwriter » Mon, Jun 07, 2021, 9:33 PM UTC

MillenialMan wrote: post #82

neolog wrote: post #56

Earlier quoted context omitted.

> 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?

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 prog…

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

Re: PyCon US 2021 Recordings are Available

#106

Post by MillenialMan » Tue, Jun 08, 2021, 10:07 AM UTC

dragonwriter wrote: post #105

MillenialMan wrote: post #82

Earlier quoted context omitted.

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 prog…

> 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…

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.

Re: PyCon US 2021 Recordings are Available

#107

Post by mananaysiempre » Sun, Jun 13, 2021, 4:06 PM UTC

neolog wrote: post #97

mananaysiempre wrote: post #94

Earlier quoted context omitted.

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…

Thanks, that makes sense to me. It's hard to find people who are knowledgeable enough about both static and dynamic systems and able to explain in layman's terms. Is there somewhere (online?) I can go to talk with people like you?

Calling me “knowledgeable” on this stuff might be a bit of a stretch, but then my standard of “knowledgeable” here is probably somewhere around “did a thesis on it”.

The people on #haskell at Freenode (nowadays Libera) were extremely friendly and helpful when I frequented it about five to ten years ago, although of course there are a subtle but important limits to initiating discussions that are interesting to people on the channel but not strictly on topic for it.

My more general advice is (for a double combo of both trite and condescending) read a book. Specifically, read Pierce’s “Types and programming languages”. I usually cherry-pick paragraphs and sections from books rather than read them from start to finish, but this particular book I basically gulped down in two sittings on two-hour flights (being trapped in economy seating helps) and found extremely enlightening both in that it dissolved the mystery around some lofty-sounding words I was always afraid of (“corecursion” and “coinduction”, “terminating” vs “productive”) and in that it contained completely elementary mathematical insights that have previously passed me by (Tarski fixed point theorem and order theory in general).

While I did have an advantage of having encountered, if not understood, basically all of the words inside it beforehand, I still believe it might be helpful even if you have absolutely no background in type systems. And don’t be put off by the use of Java in the case study, it is genuinely on point there.

For a more practical and yet more advanced (dependent types!) view, you can try “Type-driven programming in Idris” and “The little typer”, but I haven’t studied the former as carefully and have only skimmed the latter, so can’t recommend either with the same degree of certainty. I guess just follow the general advice on difficult literature: look around, follow references, don’t hesitate to put down things that don’t work for you, and if all else fails, let it stew for a week before trying again.