Live data from Hacker News

Typing Is Hard

3fx.ch

51–60 of 134 posts

Re: Typing Is Hard

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

Re: Typing Is Hard

#52
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 has shown me that I hate TypeScript.

Re: Typing Is Hard

#53
post #24
post #19

Earlier quoted context omitted.

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

Flow also used a ton of memory, and would crash pretty frequently with really bizarre errors, at least back when I had to work with it 2 years ago.

Re: Typing Is Hard

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

Re: Typing Is Hard

#55
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 taught me that I actually don’t care about types and all I care about is the shape of data. In most cases I think of types/interfaces in Typescript as strict data definitions. A function takes in a collection of data; as long as the data matches the shape I expect, don’t care what the data represents.

That's exactly what types are for dude

Re: Typing Is Hard

#56

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

Or perhaps type checking simply not terminating at all.

Re: Typing Is Hard

#57
post #30

Earlier quoted context omitted.

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.

People build huge programs in untyped languages, reasoning about null is trivial in comparison. The cost of not having null is that all initialization and generic code gets much harder to write and work with, the benefit is that once in a blue moon you get a hard to debug null pointer error. I've worked as a software engineer at large companies for years and never had a hard to debug null pointer error, so at least t…

People also used to build huge castles without any power tools. That something can be done with a tool is not an argument for that tool to be efficient or even good at it.

Re: Typing Is Hard

#58

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

This! In fact GHC does this. You can even configure the limit yourself per module if you require higher values.

Re: Typing Is Hard

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

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

Re: Typing Is Hard

#60
post #46

Earlier quoted context omitted.

Consider that you might be the weirdo here. Kotlin is eating scala's lunch by specifically jettisoning the advanced type stuff. If you can give 80% of the value with 20% of the confusion, that's a win for most devs.

Kotlin is eating Scala's hype by hyping how much better their ad-hoc informally-specified implementation of half the advanced type stuff is. Having had to actually debug errors from their "suspend functions", "platform types" and goodness knows what else, there's nothing simpler about it.

I think optimally, you have a powerful effect and dependent linear type system with adjustable strictness of checking. You'd use the very weakest level for a REPL : warn if there is no set of types that allows a function to execute without throwing a runtime type error. Most applications would be run/compiled with stricter checking. Libraries packed up for package managers would presumably be checked with full effects checking and without implicit soundness escape hatches of the kind you get in TypedScript. Security-critical libraries, such as TLS implementations, would hopefully be compiled to make full use of dependent types.

Hopefully you'd also have a lifetime system integrated with the malloc implementation. Your malloc implementation needs at a minimum a size_t header on each allocation, and you could use this similarly to how OpenJDK / Oracle's JVM lazily allocates rwlocks by "promoting" the object header's GC word to a tagged pointer to an rwlock and a copy of the original GC word. In this case, you'd probably use 2 bits of the malloc header for tagging, limiting arrays and other large objects to a maximum of 1 GB in 32-bit processes. Code for which lifetimes checked properly would completely ignore the dynamic lifetime accounting, but any code that didn't check properly would need to pass around potentially unsafe references as "fat references" as a pair of reference and rwlock. The first time an object reference hit potentially unsafe usage, its malloc header would need to be inflated to a pointer to the original size_t allocation_size and the rwlock, so that the "fat reference" could safely be made skinny and fat again as it passed between lifetime-safe and lifetime-unsafe libraries. Unfortunately for Rust-like systems that have both atomic and non-atomic reference counting, I think this means having the dynamic library headers contain a list of offsets of the non-atomic reference count operations so they can be dynamically patched if lifetime-unsafe code is ever loaded. (Or, make the safe libraries twice as big and modify the program linkage table and patch up all return addresses on stacks the first time any lifetime-unsafe code is loaded.)

The two bits for tagging the size_t allocation_size in the malloc implementation would be one bit for tagging if it was a size_t or a *struct {size_t allocation_size; size_t rwlock;} The other bit would be a "one bit reference count" for optimizing the common case where there's at most one reference to the object.

Edit: actually, the mixing of lifetime-safe and lifetime-unsafe code falls down for statically compiled systems that allow references into the middle of objects. IBM's OS/400's (i5/OS's) Technology Independent Machine Interface (TIMI) uses 128-bit pointers for everything, so maybe it's not so bad to make all references "fat references", and optimize them to regular references when escape analysis shows they will never leave lifetime-safe libraries. In any case, it's more complicated than I originally thought to efficiently mix dynamic race condition detection along with compile time elision via Rust-like compile-time borrow checking. You could use an atomic hash map to keep track of locations of the rwlocks in order to inflate thin references to fat references every time lifetime-unsafe code gets a reference from lifetime-safe code, but all of those lookups sound prohibitively expensive.

Post reply on HN