Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Typing Is Hard

3fx.ch

Post reply on HN
Print view View original

11–20 of 134 posts

Re: Typing Is Hard

#11

Post by muglug »

pansa2 wrote: post #10

> Where are Python, Bash, etc.? [...] While there exist extensions to some dynamic languages imbuing them with static type checking these are not part of the language, and the complexity depends not on the language but the extension. But TypeScript is included. Isn’t it an extension to JavaScript in the same way that Mypy is an extension to Python? Is there a technical difference that justifies one being included and…

I think it’s an important difference: TypeScript is a language that has a typechecker bundled with it. The language and the typechecker are clearly connected, and TypeScript users are very very strongly encouraged to use the typechecker on all typescript code. Type checking is also implicitly described as a language feature.

Python has no bundled typechecker, and its authors do not insist users use MyPy, Pyre or any other SA tool.

Re: Typing Is Hard

#12

Post by nwatson »

muglug wrote: post #11
pansa2 wrote: post #10

> Where are Python, Bash, etc.? [...] While there exist extensions to some dynamic languages imbuing them with static type checking these are not part of the language, and the complexity depends not on the language but the extension. But TypeScript is included. Isn’t it an extension to JavaScript in the same way that Mypy is an extension to Python? Is there a technical difference that justifies one being included and…

I think it’s an important difference: TypeScript is a language that has a typechecker bundled with it. The language and the typechecker are clearly connected, and TypeScript users are very very strongly encouraged to use the typechecker on all typescript code. Type checking is also implicitly described as a language feature. Python has no bundled typechecker, and its authors do not insist users use MyPy, Pyre or any…

Type annotations in recent 3.x releases though have made Python a much better language, and in practice the Jetbrains- (Pycharm-)-bundled type-checkers work very well. I'm much more comfortable recently working with larger codebases in Python and don't miss the C++/Java type constraints now.

Re: Typing Is Hard

#13

Post by pansa2 »

muglug wrote: post #11
pansa2 wrote: post #10

> Where are Python, Bash, etc.? [...] While there exist extensions to some dynamic languages imbuing them with static type checking these are not part of the language, and the complexity depends not on the language but the extension. But TypeScript is included. Isn’t it an extension to JavaScript in the same way that Mypy is an extension to Python? Is there a technical difference that justifies one being included and…

I think it’s an important difference: TypeScript is a language that has a typechecker bundled with it. The language and the typechecker are clearly connected, and TypeScript users are very very strongly encouraged to use the typechecker on all typescript code. Type checking is also implicitly described as a language feature. Python has no bundled typechecker, and its authors do not insist users use MyPy, Pyre or any…

So TypeScript is a separate language from JavaScript, but Mypy is just an extension to Python. Isn’t that merely a difference in marketing?

Re: Typing Is Hard

#14

Post by gjulianm »

abeppu wrote: post #3

I guess, unsoundness sounds concerning. But is undecidability? When this is an issue, it's always because someone worked to do some really elaborate or general compile-time computation. It seems a lot (literally too much) to ask that you can do really unrestrained type-level computation and also still always have termination.

To me, unsoundness doesn't sound too concerning. It is a theoretical property, and when programming I care about practice, which means that I care about consistency and predictability. If a type system is unsound because of certain edge cases, but works well in practice and those edge cases case an error later anyways, I don't care too much. I mean, most typed languages will have casting operators that can make unsafe operations precisely because programmers sometimes want to bypass the type system. Why sacrifice usability in the name of 'soundness' when in practice people are just going to bypass the type system when that happens?

Re: Typing Is Hard

#15

Post by bastawhiz »

pansa2 wrote: post #13
muglug wrote: post #11

Earlier quoted context omitted.

I think it’s an important difference: TypeScript is a language that has a typechecker bundled with it. The language and the typechecker are clearly connected, and TypeScript users are very very strongly encouraged to use the typechecker on all typescript code. Type checking is also implicitly described as a language feature. Python has no bundled typechecker, and its authors do not insist users use MyPy, Pyre or any…

So TypeScript is a separate language from JavaScript, but Mypy is just an extension to Python. Isn’t that merely a difference in marketing?

Python has type annotations but no type checking. The type checker you use for Python may have different soundness/decidability versus other type checkers.

There's only one (official) TypeScript type checker, which works in only one way, and introduces both type annotations as well as syntax which compiles to JavaScript that's executed at runtime (enums, decorators).

Re: Typing Is Hard

#16

Post by dwohnitmok »

quickthrower2 wrote: post #9

Ah that might be why there are Rank2 and RankN types as seperate extensions in Haskell.

Despite the theoretical decidability of rank-2 type inference their actual implementations in GHC are the same IIRC (so rank-2 types are not fully inferrable by GHC). I think the difference is really just one of historicity and backwards compatibility at this point. They resolve to the same underlying mechanism.

Re: Typing Is Hard

#18

Post by Zababa »

pansa2 wrote: post #13
muglug wrote: post #11

Earlier quoted context omitted.

I think it’s an important difference: TypeScript is a language that has a typechecker bundled with it. The language and the typechecker are clearly connected, and TypeScript users are very very strongly encouraged to use the typechecker on all typescript code. Type checking is also implicitly described as a language feature. Python has no bundled typechecker, and its authors do not insist users use MyPy, Pyre or any…

So TypeScript is a separate language from JavaScript, but Mypy is just an extension to Python. Isn’t that merely a difference in marketing?

It's not a difference in marketing. Types anotations are part of Python, but not of JavaScript. CPython will happily run a program with type anotations, V8 will fail to parse Typescript.

You could draw similarities with using Typescript to check JSDoc comments and MyPy to check Python 2.7 comments, but that's again because type hints are neither part of Python 2.7, nor JavaScript.

Re: Typing Is Hard

#19

Post by xixixao »

skrebbel wrote: post #5

I think we need new, better concepts to judge type systems by. Eg TypeScript has convincingly shown to a large crowd that soundness isn't an important property for many key goals of static typing, such as programmer productivity, refactoring support, preventing stupid mistakes and navigating large codebases. Soundness was Flow's big claim to fame and it just made day to day programming harder with mostly academic/cos…

I think TS had better tooling and implementation. Flow continues to improve and had some better design decisions early on. Flow has focused on internal FB needs over open source needs.

All in all, I think the soundness is not a negative / defining character and Flow could still gain in popularity, especially for projects closer in requirements to FB’s codebase.

Re: Typing Is Hard

#20

Post by diob »

skrebbel wrote: post #5

I think we need new, better concepts to judge type systems by. Eg TypeScript has convincingly shown to a large crowd that soundness isn't an important property for many key goals of static typing, such as programmer productivity, refactoring support, preventing stupid mistakes and navigating large codebases. Soundness was Flow's big claim to fame and it just made day to day programming harder with mostly academic/cos…

That last sentence really resonated with my Ruby experience. After using typescript for a few years, it feels like stepping back to JavaScript development in 2012.
Post reply on HN