Hacker News Reader

Comment by valenterry | Hacker News Reader

Typescript has a phenomenal type-system indeed. However, its foundations are not very sound. The types are pragmatic and that's what counts mostly, but going forward it would be great to have type-systems that are even more powerful and also theoretically sound with a simpler foundation (= less edge cases and workarounds). Languages like Idris are working on this.

Typescript can't really be this language because it is impeded by having to work with the javascript runtime, which makes this task much much harder to do.

View on HN

TypeScript's type foundations are not sound, and I would argue that this is a major factor why it is so good. I have yet to see a sound type system that is as pleasant to use as TypeScript's—certainly not Idris.

I am not a fan of encoding all sorts of correctness statements into a static type system. I'd much rather use a theorem proving environment for correctness, but one that is not based on type theory.

What do you gain from an unsound type system? Implicit casts still exist and one dependency returning Any means that your specification is meaningless (you can prove anything, including false).

The point is that making a typesystem sound is really hard and requires trade-offs. I think Scala is a wonderful example. Check: https://www.baeldung.com/scala/dotty-scala-3

To quote from there: > Scala 3 has dropped some unsound and useless features to make the language smaller and more regular. It has added some new constructs to increase its expressiveness. Also, it has changed some constructs to remove warts and increase simplicity, consistency, and usability.

Some of the features they dropped because they were unsound were still useful (to me).

Typescript tries neither to make their typesystem (perfectly) sound, nor to make it as elegant as possible. That results in it to be very useful/pragmatic for everyday-programming tasks.

> What do you gain from an unsound type system?

The ability to type most idiomatic javascript circa 2014. It's definitely a Faustian bargain.

I don't rely on the type system for my specification. I just rely on it to significantly reduce the number of bugs I inadvertently introduce into the implementation of my specification.

How are you sure you haven’t introduced bugs if the specification/type has an error it doesn’t tell you about?

I have trouble parsing your sentence, to be honest. What are you asking?

Are you asking how am I sure that/if my specification is correct?

Are you asking how do I make sure I have no bugs without a proof?

Maybe you are asking something else entirely?

Because the type system is unsound, you could add an error to your implementation and the type system will not catch it. It will happily tell you that everything type checks.

How do you use that to prevent errors?

Yes, that can happen. Just as a sound type system will also not prevent all possible bugs. So what? TypeScript's type system helps me to prevent many bugs by performing standard sanity checks, and is a very practical tool.

Just rephrase your question as "How will a pervasive system of sanity checks help me prevent errors?", and I hope you agree that it kind of answers itself.

Yes, I think that's what I said. The pragmatic approach makes to very ergonomic to use in most use cases. That it breaks on for edge-cases is not very relevant in practice usually.

> I'd much rather use a theorem proving environment for correctness, but one that is not based on type theory.

Based on what then?

I like Abstraction Logic: http://abstractionlogic.com

Haskell’s type system isn’t sound either, there is unsafePerformIO.

Nobody actually wants a language with a sound type system, unless they’re writing mathematical proofs. Any time you need to do anything with the external environment, such as call a function written in another language, you need an escape hatch. That’s why every language that aspires to real world use has an unsound type system, and the more practical it aspires to be, the more unsound the type system is.

Soundness is only a goal if the consequences of a type error are bad enough: your proof will be wrong, or an airplane falls out of the sky, or every computer in the world boots to a blue screen.

For everybody else the goal should be to balance error rate with developer productivity. Sacrificing double digits of productivity for single digits of error rate is usually not worth it, since the extra errors that a very sound type system will catch will be dominated by the base rate of logic errors that it can’t catch.

I think there is a misunderstanding on your side. You seem to mix up the soundness of the type-system with the property of referential transparency. Those are two orthogonal things.

Oh and to your argument:

> For everybody else the goal should be to balance error rate with developer productivity. Sacrificing double digits of productivity for single digits of error rate is usually not worth it, since the extra errors that a very sound type system will catch will be dominated by the base rate of logic errors that it can’t catch.

I think you are missing my point.

You are merely looking at a single point in time. And yes, you are right - the balance you mention matters. But what also matters is the future. A language needs to be able to evolve. If it does not do that, it will eventually die and become replaced. If the typesystem is well made with good foundations, the language will be able to evolve and adapt faster and causing less problems for its users.

What does "soundness" mean here? I love typescript's type system, except for the quirks that are inherited from javascript, which I sometimes find infuriating, and I'm wondering if you're talking about the same thing. For example, the fact that typescript- through javascript- only exposes a single `number` type is so annoying. Sometimes that's fine, but other times it would be nice to be able to say "No, this isn't just any damn number, this is an integer! This is an iterable ID for god's sake!" so you at the very least get a static error when you try to pass in `1.001`, or something that could be `1.001`. And that's just a very basic example of how a collection of number types with more granularity would be an improvement. Especially if they were a little more robust than that and were composable. Imagine being able to type `integer | negativeFloat` or other such wacky composed types. Ideally you could compose your types programmatically, and define shit like "the type is a `float` who's floor value has a % 3 of 0".

https://www.typescriptlang.org/docs/handbook/type-compatibil...

https://www.typescriptlang.org/play/?strictFunctionTypes=fal...

     // This can go all the way back to the smallest common type:

     listenForEvent("mouse", (event: {}) => { });

Typescript {} is a trap that means "any container of things is fine" (including objects), it's not the empty struct. One of the very ugly oddities of the language.. `Record<string, never>` or something like that is the closest equivalent to an empty struct.

https://github.com/typescript-eslint/typescript-eslint/issue...

Informally, a sound type system is one that never lies to you.

Formally, the usual notion of soundness is defined with respect to an evaluation strategy: a term-rewriting rule, and a distinguished set of values. For pure functional programs this is literally just program execution, whereas effects require a more sophisticated notion of equivalence. Either way, we'll refer to it as evaluating the program.

There are two parts:

- Preservation: if a term `a` has type `T` and evaluates to `b`, then `b` has type `T`.

- Progress: A well-typed term can be further evaluated if and only if it is not a value.

Reply on news.ycombinator.com