3 ms·

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 fo

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.

auggierose 2y ago
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.
- agentultra 2y ago
  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).
  - valenterry 2y ago
    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 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.
  - nyssos 2y ago
    > What do you gain from an unsound type system? The ability to type most idiomatic javascript circa 2014. It's definitely a Faustian bargain.
  - auggierose 2y ago
    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.
    - agentultra 2y ago
      How are you sure you haven’t introduced bugs if the specification/type has an error it doesn’t tell you about?
      - auggierose 2y ago
        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?
        agentultra 2y ago
        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?
        auggierose 2y ago
        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.
- valenterry 2y ago
  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?
  - auggierose 2y ago
    I like Abstraction Logic: http://abstractionlogic.com http://abstractionlogic.com
zarzavat 2y ago
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.
- valenterry 2y ago
  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.
- valenterry 2y ago
  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.
the8thbit 2y ago
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".
- shepherdjerred 2y ago
  https://www.typescriptlang.org/docs/handbook/type-compatibility.html#a-note-on-soundness https://www.typescriptlang.org/docs/handbook/type-compatibil... https://www.typescriptlang.org/play/?strictFunctionTypes=false#example/soundness https://www.typescriptlang.org/play/?strictFunctionTypes=fal...
  - yencabulator 2y ago
    // 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/issues/2063 https://github.com/typescript-eslint/typescript-eslint/issue...
- nyssos 2y ago
  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.

auggierose 2y ago

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.

agentultra 2y ago
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).
- valenterry 2y ago
  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 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.
- nyssos 2y ago
  > What do you gain from an unsound type system? The ability to type most idiomatic javascript circa 2014. It's definitely a Faustian bargain.
- auggierose 2y ago
  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.
  - agentultra 2y ago
    How are you sure you haven’t introduced bugs if the specification/type has an error it doesn’t tell you about?
    - auggierose 2y ago
      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?
      - agentultra 2y ago
        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?
        auggierose 2y ago
        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.
valenterry 2y ago
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?
- auggierose 2y ago
  I like Abstraction Logic: http://abstractionlogic.com http://abstractionlogic.com

zarzavat 2y ago

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.

valenterry 2y ago
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.
valenterry 2y ago
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.

the8thbit 2y ago

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

shepherdjerred 2y ago
https://www.typescriptlang.org/docs/handbook/type-compatibility.html#a-note-on-soundness https://www.typescriptlang.org/docs/handbook/type-compatibil... https://www.typescriptlang.org/play/?strictFunctionTypes=false#example/soundness https://www.typescriptlang.org/play/?strictFunctionTypes=fal...
- yencabulator 2y ago
  // 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/issues/2063 https://github.com/typescript-eslint/typescript-eslint/issue...
nyssos 2y ago
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.