Typing Is Hard
3fx.ch
Typing Is Hard
1–10 of 134 posts
Re: Typing Is Hard
#2Clicked expecting a treatise about ergonomics and keyboard layouts, came away with slightly more appreciation for Rust’s long compile times.
Re: Typing Is Hard
#3I 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.
Re: Typing Is Hard
#4I 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.
I 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.
Re: Typing Is Hard
#5I 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.
Re: Typing Is Hard
#6[deleted]
Re: Typing Is Hard
#7I 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.
I 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.
Re: Typing Is Hard
#8It_is_ hard - there's a typo in it "satifies".
Re: Typing Is Hard
#9Ah that might be why there are Rank2 and RankN types as seperate extensions in Haskell.
Re: Typing Is Hard
#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 the other not, or is it just a case of popularity?