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

21–30 of 134 posts

Re: Typing Is Hard

#21

Post by chrismorgan »

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…

TypeScript and Flow exist on top of JavaScript; given JavaScript (the language and ecosystem), an unsound type system is pragmatic, and a sound type system sometimes inconvenient. It is not obviously correct to generalise that property of soundness making life hard to other languages that are designed from scratch. (I think it is unwise to so generalise, but opinions may easily differ; my point is purely that the generalisation is not manifestly correct.)

Re: Typing Is Hard

#22

Post by username90 »

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 that having a compromise between types and untyped is best.

So first, have a type all other types can be cast to, call it object and allow it to perform generic operations. Then have a type that can be cast to all other types, call it null. These two gives you a lot of the nice parts of untyped languages while still allowing for tooling like quick refactoring or name completions. When I code in a system lacking any of these I feel way slower.

Re: Typing Is Hard

#23

Post by mixedCase »

gjulianm wrote: post #14
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 unsaf…

>To me, unsoundness doesn't sound too concerning

Just debug enough TypeScript and it will sound concerning.

Re: Typing Is Hard

#24

Post by lhorie »

xixixao wrote: post #19
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.

We use flow extensively at work (we have a monorepo w/ some 400 projects in them). `ag FlowFixMe | wc -l` gives me almost ten thousand hits. Which means that in practice, there's a lot of unsoundness going on even if one chooses to use flow over TS.

A lot of people at work dislike flow because while it is generally sounder than TS, it throws some really stupid "errors" (e.g. Array prototype.filter doesn't refine arrays of nullables, it can't tell property access isn't a getter w/ side effects so it errs on the side of assuming it always is, etc).

Typescript simply draws the line in the sand clearly from the beginning so that its scope as a project stays well defined and it doesn't end up accidentally falling into obscure gaps like flow.

Re: Typing Is Hard

#25

Post by habitue »

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 your point, the example of Idris is sound and decidable, but in practice the decidability doesn't matter: you add fuel[1] to limit recursion, but it can just be some arbitrarily large number (but not infinite) number of loops.

[1] https://www.idris-lang.org/docs/current/contrib_doc/docs/Dat...

Re: Typing Is Hard

#26

Post by KMag »

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…

Ideally, we'd have different strictness subsets of a single language, a generalization of JavaScript's strict mode. In a REPL, you'd want the type system to warn you of provable mistakes ("x will always be an int here, but you're array indexing on it" type things) but still let you make them, as you're often in the middle of breaking compatibility. In a library packed up for a package manager, you'd want strictness dialed up quite a bit, probably enforcing soundness. For something security-critical like a TLS implementation, you'd want very pedantic type checking.

Libraries used across or between large organizations are often used in contexts unexpected or at least incompletely understood by the libraries' authors, and are therefore much more likely to encounter inputs that violate implicit assumptions made by the library authors. The more remote and varied the contexts in which a library is used, the more you'd want to force these assumptions to be made explicit in the library's interface.

The strictness isn't one-dimensional, either. For instance, in a CRUD webapp, you'd probably want an effects system in your type system capable of expressing which inputs are un-vetted untrusted inputs (similar to Perl's taint mode), but you might or might not want other effects to be enforced by the type system.

Re: Typing Is Hard

#28

Post by dwhitney »

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 need to write a blog entry titled, "Your test suite is basically a sh*tty type system." -- I'm in the "totally anal" camp of type system aficionados :)

Re: Typing Is Hard

#29

Post by Chris_Newton »

Those interested in this subject might also enjoy What To Know Before Debating Type Systems:

https://cdsmith.wordpress.com/2011/01/09/an-old-article-i-wr...

It’s one of those older articles where not everyone will agree with everything, but there’s still a lot of insight and food for thought.

Re: Typing Is Hard

#30

Post by yoneda »

username90 wrote: post #22
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 that having a compromise between types and untyped is best. So first, have a type all other types can be cast to, call it object and allow it to perform generic operations. Then have a type that can be cast to all other types, call it null. These two gives you a lot of the nice parts of untyped languages while still allowing for tooling like quick refactoring or name completions. When I code in a system lacki…

On the contrary, I find myself more productive in languages that do not have pervasive null because then I don't have to manually reason about which values might be null.
Post reply on HN