3 ms·

From the article some reasons not to use TypeScript: "... in VSCode, the red lines and warnings take a long time to update on large projects. ... absence of [

From the article some reasons not to use TypeScript: "... in VSCode, the red lines and warnings take a long time to update on large projects. ... absence of [a] specification" for TypeScript's behaviour. Donny's had to infer TypeScript's behaviour mostly test cases alone. The pure size of TypeScript is daunting. It's had ten years to iterate, grow and add features. " --- Therefore for practical reasons, I stick with plain JavaScript (on Node.js etc.) and use a small assertions library https://www.npmjs.com/package/ok6 Assertions are the ultimate "types", they can assert any property you can express in your programming language. The key is to be able to make them succinct so they don't obscure your main code. Yes they don't give you compile-time type-checking, which would be useful indeed. But as hinted at the excerpts above, in practice compile-time type-checking can slow you down. In most case all I need is a way to prove to myself that "if this function runs a set of tests-cases, then the assertions in it are truthful. And, if anybody calls this function with wrong types of arguments my assertions will tell me there is a problem. Often enough of a good thing is enough. You don't need the most sophisticated language and type-system to create robust programs quickly.

ajkjk 4y ago
I dunno, I love types as documentations of how things are supposed to be structured. But I also agree that assertions are great because they can express any condition in the language. I wonder sometimes if it's possible to have a type system that is "any possible assertion, as a type".
- zem 4y ago
  in theory no, because you run into the halting problem. but even in practical terms it would impede your ability to do static type analysis long before that point.
  - ajkjk 4y ago
    I don't really care about static type analysis, in a sense: If I write an assertion `x is a number`, then fine, statically analyze that, that works today. If I write a hard-to-compute assertion like `x is Prime` (or `x is a counterexample to the Riemann Hypothesis`), then I don't care if the compiler can statically figure it out. It can simply require all callers to test that before calling this function, they assert `x is Prime` directly -- no analysis required. This way my function can be sure it is only called with prime numbers, but nobody has to write any logic in a typechecker that can figure out whether that's true for arbitrary inputs.
    - wtetzner 4y ago
      I believe that's what dependent types allow you to do. However, even in weaker type systems you can get a similar effect by just creating a PrimeNumber type, and for functions that require a prime number, only accept PrimeNumber. Then any number you want to pass to those functions will have to go through PrimeNumber's constructor.
    - zem 4y ago
      that usually gets classified under contracts rather than types. eiffel is probably the best known example of a contract based language, but also check out typed racket, it uses a nice mix of types and runtime contracts in a dynamic language.
      - galaxyLogic 4y ago
        That is good vocabulary. Clearly there is a difference between static type-checking and assertions. But "types" is not the same as "type-checking". Type-checking can happen at runtime, or at compile-time. Or both. My point was more that static type-checking can be seen equivalent to assertions, except it checks those assertions at compile time and typically lacks some expressive power compared to assertions, in most practical programming languages today. Static type-checking is more a feature of the compiler than of the language. Consider type-inference: You can have a language where types are not explicitly declared most of the time. Yet they can be checked at compile-time, assuming you have a compiler that is able to perform that amazing feat.
    - lmm 4y ago
      What are the callers supposed to do when the assertion fails? Either you carry the assertion all the way back to the point where x is created - in which case you're implementing a type system, whether you call it that or not - or you have code that will have runtime failures in the middle of your computations.
      - galaxyLogic 4y ago
        > you have code that will have runtime failures in the middle of your computations. Preferably during running of your unit-tests. In practice much of the software we use today has runtime errors. How the code handles those varies. Static typing does not prevent runtime errors does it?
- galaxyLogic 4y ago
  I think the main difference between assertions and static type-checking is that ... static checking can do its checks at compile time. That is a great feature for big projects. But the benefit of assertions is they can express arbitrary requirements, not only about the type of each argument and result but also about intra-arguments relationships between arguments, and also between arguments and the result. As an example I could say: ok (argA < argB); ... ok (result > argA - argB); It's a tradeoff: More expressivity, simplicity and speed of development vs. earlier detection of type-errors.
- consilient 4y ago
  Yes, this is called refinement typing (which is a special case of dependent typing). Idris and Agda are probably the dependently typed languages that are closest to being usable for general purpose programming, but they've still got a ways to go.
lmm 4y ago
> Yes they don't give you compile-time type-checking, which would be useful indeed. But as hinted at the excerpts above, in practice compile-time type-checking can slow you down. This is backwards. Having your type system be unplanned and ad-hoc is what makes it slow and complex (thus TypeScript, which had to retrofit a type system onto JavaScript), and making types be arbitrary runtime code is the epitome of that. There are better points on the expressivity/constraint tradeoff, but you'll only ever reach them by designing them into your programming language up-front; you can't retrofit consistency.
satvikpendem 4y ago
This is like throwing the baby out with the bath water (and is very similar to what I see with people lambasting Rust for its memory strictness and then using C, C++ or Go). I'd take a slightly slower language with static types than reverting to using a dynamically typed language, any day of the week.

ajkjk 4y ago

I dunno, I love types as documentations of how things are supposed to be structured. But I also agree that assertions are great because they can express any condition in the language. I wonder sometimes if it's possible to have a type system that is "any possible assertion, as a type".

zem 4y ago
in theory no, because you run into the halting problem. but even in practical terms it would impede your ability to do static type analysis long before that point.
- ajkjk 4y ago
  I don't really care about static type analysis, in a sense: If I write an assertion `x is a number`, then fine, statically analyze that, that works today. If I write a hard-to-compute assertion like `x is Prime` (or `x is a counterexample to the Riemann Hypothesis`), then I don't care if the compiler can statically figure it out. It can simply require all callers to test that before calling this function, they assert `x is Prime` directly -- no analysis required. This way my function can be sure it is only called with prime numbers, but nobody has to write any logic in a typechecker that can figure out whether that's true for arbitrary inputs.
  - wtetzner 4y ago
    I believe that's what dependent types allow you to do. However, even in weaker type systems you can get a similar effect by just creating a PrimeNumber type, and for functions that require a prime number, only accept PrimeNumber. Then any number you want to pass to those functions will have to go through PrimeNumber's constructor.
  - zem 4y ago
    that usually gets classified under contracts rather than types. eiffel is probably the best known example of a contract based language, but also check out typed racket, it uses a nice mix of types and runtime contracts in a dynamic language.
    - galaxyLogic 4y ago
      That is good vocabulary. Clearly there is a difference between static type-checking and assertions. But "types" is not the same as "type-checking". Type-checking can happen at runtime, or at compile-time. Or both. My point was more that static type-checking can be seen equivalent to assertions, except it checks those assertions at compile time and typically lacks some expressive power compared to assertions, in most practical programming languages today. Static type-checking is more a feature of the compiler than of the language. Consider type-inference: You can have a language where types are not explicitly declared most of the time. Yet they can be checked at compile-time, assuming you have a compiler that is able to perform that amazing feat.
  - lmm 4y ago
    What are the callers supposed to do when the assertion fails? Either you carry the assertion all the way back to the point where x is created - in which case you're implementing a type system, whether you call it that or not - or you have code that will have runtime failures in the middle of your computations.
    - galaxyLogic 4y ago
      > you have code that will have runtime failures in the middle of your computations. Preferably during running of your unit-tests. In practice much of the software we use today has runtime errors. How the code handles those varies. Static typing does not prevent runtime errors does it?
galaxyLogic 4y ago
I think the main difference between assertions and static type-checking is that ... static checking can do its checks at compile time. That is a great feature for big projects. But the benefit of assertions is they can express arbitrary requirements, not only about the type of each argument and result but also about intra-arguments relationships between arguments, and also between arguments and the result. As an example I could say: ok (argA < argB); ... ok (result > argA - argB); It's a tradeoff: More expressivity, simplicity and speed of development vs. earlier detection of type-errors.
consilient 4y ago
Yes, this is called refinement typing (which is a special case of dependent typing). Idris and Agda are probably the dependently typed languages that are closest to being usable for general purpose programming, but they've still got a ways to go.

lmm 4y ago

> Yes they don't give you compile-time type-checking, which would be useful indeed. But as hinted at the excerpts above, in practice compile-time type-checking can slow you down. This is backwards. Having your type system be unplanned and ad-hoc is what makes it slow and complex (thus TypeScript, which had to retrofit a type system onto JavaScript), and making types be arbitrary runtime code is the epitome of that. There are better points on the expressivity/constraint tradeoff, but you'll only ever reach them by designing them into your programming language up-front; you can't retrofit consistency.

satvikpendem 4y ago

This is like throwing the baby out with the bath water (and is very similar to what I see with people lambasting Rust for its memory strictness and then using C, C++ or Go). I'd take a slightly slower language with static types than reverting to using a dynamically typed language, any day of the week.