14 ms·
Typing Is Hard
- whoisburbansky 6y agoClicked expecting a treatise about ergonomics and keyboard layouts, came away with slightly more appreciation for Rust’s long compile times.
- augusto-moura 6y agoSame Would benefit from a article about RSI though
- abeppu 6y agoI 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.
- enricozb 6y agoI think this is an important point to focus on when writing a new type-safe language. LEAN for example has a very impressive type system (honestly seems like magic sometimes), and clearly all of the "impossibility" is shoved into the computational complexity of the type-checker. Despite the fact that some of the languages listed here have undecidable type systems, it doesn't feel like many common-purpose languages have purposefully gone down the undecidable route to bring some really cool type-safety.
- mhh__ 6y agoI agree. If undecidability (or some stricter but still off-putting set)in a given language means an extremely complicated compiler that would be a mark against it, but if it's just an obscure edge case or something that is already not possible in a normal language, then I really don't care. I would, however, like to see termination analysis applied to code more often - e.g. rather like only accepting a pure function in an interface, this function must terminate but might not be pure.
- gjulianm 6y agoTo 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?
- mixedCase 6y ago>To me, unsoundness doesn't sound too concerning Just debug enough TypeScript and it will sound concerning.
- robinei 6y agoSoundness gives an important benefit: Performance, for a compiler capable of utilising the type information properly. It can omit run-time checks, and unbox primitives etc.
- habitue 6y agoTo 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/Data.Fuel.html https://www.idris-lang.org/docs/current/contrib_doc/docs/Dat...
- lmm 6y agoIt might seem a lot, but Idris shows that it's possible.
- skrebbel 6y agoI 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/cosmetic benefits. I'm sure that there's more reasons why TS won the popularity contest, but TS's pragmatic forgiveness surely played a part. And I don't even see how "decideable" is a desireable property at all. So what if the type checker can infloop? It won't in practice. At the same time, most people will agree that eg Go's type system is very different from Idris's. They have very different pros and cons, both in terms of how hard they are to typecheck and how great they are to use. In fact I can't think two somewhat popular type systems that could be more different from one another, but if you only read this page you might think they're comparable. We need words for "totally anal" and "basically Ruby but some typos are caught" and everything in-between.
- xixixao 6y agoI 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.
- lhorie 6y agoWe 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.
- deleted 6y ago[deleted]
- booky2 6y agoIt_is_ hard - there's a typo in it "satifies".
- quickthrower2 6y agoAh that might be why there are Rank2 and RankN types as seperate extensions in Haskell.
- dwohnitmok 6y agoDespite 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.
- elwell 6y agoTLDR just use mavis beacon...
- pansa2 6y ago> 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 the other not, or is it just a case of popularity?
- muglug 6y agoI 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.
- nwatson 6y agoType 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.
- pansa2 6y agoSo TypeScript is a separate language from JavaScript, but Mypy is just an extension to Python. Isn’t that merely a difference in marketing?
- bastawhiz 6y agoPython 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).
- dwhitney 6y agoit drives me absolutely insane that this TypeScript compiles: const num: number = [][0]
- smlckz 6y agoHuh, go figure the following: const a = 'this is not a ' + typeof + 'number'; Or JSFuck[1] in that matter. [1]: http://jsfuck.com http://jsfuck.com
- panzerklein 6y agoIt won't with --noUncheckedIndexedAccess on.
- wutbrodo 6y agoThat seems like a pretty insane default. Do you happen to know what the thinking is? While I'm fortunate enough to have never needed to spend significant time working in JS and its spawn, I've heard a lot of good things from people I respect about TS and its incremental typing approach, so I'm starting from the baseline assumption that this is a reasonable choice.
- ygra 6y agoThere seem to have been a few options that are disabled by default and emit additional errors, that slowly get turned on by default in later versions. Perhaps this is one of them.
- wutbrodo 6y agoThat's reasonable, thanks for the info
- panzerklein 6y agoThis option is too extreme to be enabled by default. Even --strict shortcut that turns on a bunch of useful checks does not include it.
- Chris_Newton 6y agoThose 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-wrote/ 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.
- mariusor 6y ago> The knowledge of the compiler in a statically typed language can be used in a number of ways, and improving performance is one of them. It’s one of the least important, though, and one of the least interesting. Erm... no. I don't mean to invalidate the whole article from just this quote, but it's this kind of thinking is what makes today's applications slow, from browsers to office suites and web-sites. Wasting computing resources because you can, is a lazy way of thinking about development in my opinion.
- rsrsrs86 6y agoMost comments here are asking guarantees from type checkers that actually belong to semantic analysis and static analysis in general but not necessarily related to type checking.
- lmm 6y agoType checking is not the only conceivable way of achieving those guarantees, but it's effective and at least somewhat understood by most working programmers, so why do something different for the sake of it?
- darksaints 6y agoI think I remember reading that Scala 3.0 introduced some backwards incompatibility in order to make the type system sound. Anybody aware of what had to change?
- adenozine 6y agoCheck out Dotty and some of the papers on DOT calculus. Sorry, on mobile or I'd link you. Scala 3 has some different fundamentals. I don't think it's all the way sound like idris, but there's a lot of new rules underneath the hood to have types be much safer. I hate Scala, but I gotta admit the future of it looks a little promising if they nail the transition
- daurnimator 6y ago> Zig > undecidable, since evaluation of recursive functions at compile time is possible, thus requiring the compiler to solve the halting problem. Zig's comptime is limited to the number of backwards branches you allow, see https://ziglang.org/documentation/master/#setEvalBranchQuota https://ziglang.org/documentation/master/#setEvalBranchQuota
- steerablesafe 6y agoThat's kind of weak. It is similar to implementation limits in C++ type checking. No C++ compiler will hang in an infinite loop either.
- username90 6y ago> A decision problem is decidable if for any input we can compute whether the input satifies the problem in finite time. Examples of decidable problems include primality testing and boolean satisfiability. The halting problem for example is undecidable: We cannot check whether a program runs infinitely long in finite time. This isn't important for type systems though. Any undecidable type system can trivially be made decidable by putting a cap on how many instructions you can run when evaluating the type. Such limitations works really well in practice since useful types takes relatively little to evaluate, and you can put it as a compiler option in the few edge cases where someone needs a huge complicated type that goes above the cap.
- rowanG077 6y agoThis! In fact GHC does this. You can even configure the limit yourself per module if you require higher values.
- mastrsushi 6y ago> Completeness A type checker is complete if it can check every correctly typed program. Do they mean as opposed to the type check system failing with the wrong data type detected?
- phs 6y agoOr perhaps type checking simply not terminating at all.
- yen223 6y agoA typechecker that is "complete" will always accept correctly-typed programs, but it may accept some incorrectly-typed programs. A typechecker that is "sound" will always reject incorrectly-typed programs, but it may reject some correctly-typed programs.
- cryptica 6y agoStatic typing is a learning tool for junior level developers. Like training wheels on a bike. After 10 years or so of programming experience, the training wheels need to come off. People's attitude towards static vs dynamic typing would make a great topic for interview questions to weed out junior devs. Senior recruiter: "How do you feel about TypeScript?" Candidate: "I like it. It helps ensure that I don't accidentally pass the wrong type of instances to functions... Which is a very big problem for me and the people I usually work with." Senior recruiter: "Thank you for your time... We'll be in touch..." ... Candidate walks out the door. Recruiter: "That's a definite no... This candidate is the Neglectful type (pun intended)" Junior recruiter: "Could have fooled me! Too bad there are no automatic candidate type checkers for us junior recruiters... That would be the greatest thing since adult diapers." ... Both recruiters break into laughter while watching their email inboxes struggle to render the massive, never-ending flow of new resumes.
- madeofpalk 6y agoThis is... a joke, right?
- cryptica 6y agoIf a surgeon needed the help of a computer to make sure that he/she didn't confuse your heart for your kidney, would you trust that surgeon to do an operation on you?
- augustk 6y agoWhy do you think protective equipment is required in some professions? Is it because workers don't know their job? Anyway, explicit static typing 1. detects errors at compile time 2. provides documentation 3. makes programs run faster.
- cryptica 6y agoProtective equipment is typically used to protect people, not products. 1. Tests detect errors at runtime. Typing is completely redundant when you have even half-decent tests. 2. Comments, good variable and function names provides documentation too. 3. Not really. TypeScript is not faster than JavaScript for example. Even in certain cases where they are faster (e.g. comparing C/C++ with JavaScript), the max speedup is typically less than 40% in the absolute best use cases.. For the average case (typical program) the speedup is typically insignificant (like 5%, 10%...). Also, static types don't stop people from writing inefficient algorithms. On the other hand, statically typed languages with a build step slow down the develop/test iteration speed. In the case of TypeScript, transpilers add complexity to the project in many ways including compatibility issues (since now you have to worry about not just Node.js or Browser version but also TypeScript version and the different permutations)... Source mapping doesn't work right in certain environments. The output often looks mangled and is hard to debug in a constrained remote environment. Takes more time to setup. Adds many unnecessary dependencies to your project. Makes your software harder to integrate by third-parties since your schema is more rigid and might not correspond with their own type system. They encourage developers to define complex function signatures with complex interfaces and encourage passing instance references instead of simple copy-by-value primitives.. The drawbacks are significant and I could keep listing them all day.
- slaymaker1907 6y agoJava's type system is actually unsound if you include checked exceptions as part of the type system. By using generics, you can write ExceptionUtils.rethrow[1] in Java[2]. I think that this should count as true type unsoundness because unlike type casts, you aren't relying on some explicit runtime check and because checked exceptions are essentially a subset algebraic effects. In practice, rethrow can be convenient if you are already catching everything anyway or if some library is overusing checked exceptions. [1]: https://commons.apache.org/proper/commons-lang/apidocs/org/apache/commons/lang3/exception/ExceptionUtils.html#rethrow-java.lang.Throwable- https://commons.apache.org/proper/commons-lang/apidocs/org/a... [2]: https://www.baeldung.com/java-sneaky-throws#:~:text=In%20Java,%20the%20sn%20eaky%20throw%20concept%20allows,effectively%20imitating%20the%20characteristics%20of%20a%20runtime%20exception https://www.baeldung.com/java-sneaky-throws#:~:text=In%20Jav....