4 ms·

Good points. However, I disagree with this: > But please, stop pretending that type-level programming is a desirable thing. It's a kludge, and hopefully a temp

by _bxg1 7y ago

Good points. However, I disagree with this: > But please, stop pretending that type-level programming is a desirable thing. It's a kludge, and hopefully a temporary one. Personally, I want to write all my specifications in more-or-less the same language I use to write ordinary code. It's the tool's job to prove correctness or, if it must, tell me that it failed. I don't see explicit type-programming as (always) a kludge; oftentimes it's the primary vocabulary for expressing certain ideas. I.e. type annotations are not (always) just typechecker-hints, but can be explicit documentation of intent. > We need to be able to step up the strength of our specifications without switching language all the time. We need to integrate typed and untyped code This has been a revelation during my time spent with TypeScript. The fact that I can just add a comment that disables an unhelpful type error on a given line is a game-changer. Or that I can assert to the system "no really, this value that has a union type is actually just this particular subset of that union" (cast) and retain meaningful checks after that point. Having a type system that's flexible has made it enormously more useful. It allows you to deal with those cases where what you want to do can't be type-checked, within the context of (and playing nicely with) a broader system that is type-checked.

mike_hock 7y ago
It is sensible to include this in TypeScript, because it needs to interface with potentially large swathes of plain JavaScript, which is akin to unsafe code in Rust. TypeString type assertions are like C++ reinterpret_cast. If you're wrong about what you think it is, that's as good as undefined behavior in C++, virtually anything can happen.
- ChrisSD 7y ago
  I'm only nitpicking because this is one of the things the article complains about but I think you're conflating two types of saftey. All Javascript (TypeScript included) is "safe" in the sense of C++/Rust. Using the wrong TypeScript type in TypeScript can result in programming errors but not unsafety or undefined behaviour in C++/Rust terms.
atoav 7y ago
As somebody who moved from untyped to typed (Python to Rust) I think the two biggest arguments for typed systems are: - they encourage you to keep you code data oriented, which is usually (at least in my experience) a food thing - certain classes of mistakes can be checked for before you even run the code itself
- quickthrower2 7y ago
  They also make refactoring much easier. Renaming a function or variable and having all "true" references renamed (not just things with the same name but in a different scope), for example.
  - polityagent 7y ago
    Safely and automatically renaming a function, local or global variable does not require a type system (see clojure and many other dynamic languages). Only renaming an instance field on a class needs it (because then all accesses on an object must be renamed, which requires knowledge of the type of your variables). Incidentally programming in a more functional style reduces the need for this kind of thing. it doesn't eliminate it though so it can still be a source of runtime bugs when typos creep in, that's a trade off you have to make.
    - thrower123 7y ago
      It doesn't require it, but by all indications it makes the tooling much easier to write when there is a type system and it's constraints reducing the surface area.
    - polityagent 7y ago
      Unit tests for business logic and specifications for data shape can help to catch those typos as a side effect of the other benefits they bring. However typo catching will never be as solid as in a typed language, I've decided I'm ok with that as long as I'm not programming something that could kill someonev if it crashes.
fhars 7y ago
Another thing to consider is the type system of Idris where the compiler may recognise at compile time that the value can only be of a certain subset of a union and, more importantly, can use the type of a function to infer much of the correct implementation, like, all the cases that must be handled and sometimes even how to handle them.
- _bxg1 7y ago
  Lots of type systems support type inference. It seemed (I could have misinterpreted) like the OP was suggesting that in a perfect world all types would be inferred. That's the idea I was disagreeing with.
  - fhars 7y ago
    Normal type inference deduces the type from the code, Idris can infer the implementation from the type if the type is specific enough. In a way, this is Church in action: the type is a theorem, and the compiler is a proof assistant that helps to automatically find a proof (a correct program having that type). So Idris is an argument supporting your position: if it works (it is still part of a research program), the types are the primary expression, and the code is secondary.
agentultra 7y ago
> type annotations are not (always) just typechecker-hints, but can be explicit documentation of intent More than this, in highly expressive type systems such as Haskell's, they can carry proofs. This can be useful for constraining the capabilities of effects (ie: we can state that a particular function has the ability to make a network request but cannot open files) as well as assisting us in writing the correct implementation by construction. As an author of a type-level library it's also highly useful for generating code from arbitrary types that is also correct by construction and deriving obvious implementations so we have to write less code. Haskell's type system may soon be able to check for usage as well by encoding linearity into the type system. This will enable to tell the type checker that a function which has a resource must use it at least once. Without explicitly sequencing our nice, pure code the compiler can ensure that linearity is preserved. Idris 2 is experimenting with this as well. It seems like a pretty good idea. And all of this type level stuff is so useful that we want to do more of it. Dependently typed languages remove the separation between the type language and the language of terms. This is powerful stuff.
deleted 7y ago
[deleted]
darkkindness 7y ago
I read the OP differently. Type-level programming (not to be confused with type-oriented programming) is using the typechecker to perform computation on types, which proves guarantees at compiler time. In this case, types are less about documentation, they are literally proofs of properties of the program by construction. In fact, type-level programming is usually unreadable[0] unless the reader has deep knowledge of the specific language implementation of type families, functional dependencies, poly-kinds, etc (whatever permits typelevel programming in that language). I'm getting that the OP is arguing against these ad-hoc constructs (type families etc) and would much rather write these proofs in the same language as ordinary code (e.g. writing the law "List x where length(x) == 5" in the type rather than "forall a. List (S (S (S (S (S Z))))) a") which, well who can disagree? In a sense, you and OP both agree on the same thing. Types are good. No types (or unreadable ad-hoc constructs for types) are not good. [0]: https://aphyr.com/posts/342-typing-the-technical-interview https://aphyr.com/posts/342-typing-the-technical-interview uses type-level programming in Haskell to solve N-queens

by _bxg1 7y ago

mike_hock 7y ago

It is sensible to include this in TypeScript, because it needs to interface with potentially large swathes of plain JavaScript, which is akin to unsafe code in Rust. TypeString type assertions are like C++ reinterpret_cast. If you're wrong about what you think it is, that's as good as undefined behavior in C++, virtually anything can happen.

ChrisSD 7y ago
I'm only nitpicking because this is one of the things the article complains about but I think you're conflating two types of saftey. All Javascript (TypeScript included) is "safe" in the sense of C++/Rust. Using the wrong TypeScript type in TypeScript can result in programming errors but not unsafety or undefined behaviour in C++/Rust terms.

atoav 7y ago

As somebody who moved from untyped to typed (Python to Rust) I think the two biggest arguments for typed systems are: - they encourage you to keep you code data oriented, which is usually (at least in my experience) a food thing - certain classes of mistakes can be checked for before you even run the code itself

quickthrower2 7y ago
They also make refactoring much easier. Renaming a function or variable and having all "true" references renamed (not just things with the same name but in a different scope), for example.
- polityagent 7y ago
  Safely and automatically renaming a function, local or global variable does not require a type system (see clojure and many other dynamic languages). Only renaming an instance field on a class needs it (because then all accesses on an object must be renamed, which requires knowledge of the type of your variables). Incidentally programming in a more functional style reduces the need for this kind of thing. it doesn't eliminate it though so it can still be a source of runtime bugs when typos creep in, that's a trade off you have to make.
  - thrower123 7y ago
    It doesn't require it, but by all indications it makes the tooling much easier to write when there is a type system and it's constraints reducing the surface area.
  - polityagent 7y ago
    Unit tests for business logic and specifications for data shape can help to catch those typos as a side effect of the other benefits they bring. However typo catching will never be as solid as in a typed language, I've decided I'm ok with that as long as I'm not programming something that could kill someonev if it crashes.

fhars 7y ago

Another thing to consider is the type system of Idris where the compiler may recognise at compile time that the value can only be of a certain subset of a union and, more importantly, can use the type of a function to infer much of the correct implementation, like, all the cases that must be handled and sometimes even how to handle them.

_bxg1 7y ago
Lots of type systems support type inference. It seemed (I could have misinterpreted) like the OP was suggesting that in a perfect world all types would be inferred. That's the idea I was disagreeing with.
- fhars 7y ago
  Normal type inference deduces the type from the code, Idris can infer the implementation from the type if the type is specific enough. In a way, this is Church in action: the type is a theorem, and the compiler is a proof assistant that helps to automatically find a proof (a correct program having that type). So Idris is an argument supporting your position: if it works (it is still part of a research program), the types are the primary expression, and the code is secondary.

agentultra 7y ago

> type annotations are not (always) just typechecker-hints, but can be explicit documentation of intent More than this, in highly expressive type systems such as Haskell's, they can carry proofs. This can be useful for constraining the capabilities of effects (ie: we can state that a particular function has the ability to make a network request but cannot open files) as well as assisting us in writing the correct implementation by construction. As an author of a type-level library it's also highly useful for generating code from arbitrary types that is also correct by construction and deriving obvious implementations so we have to write less code. Haskell's type system may soon be able to check for usage as well by encoding linearity into the type system. This will enable to tell the type checker that a function which has a resource must use it at least once. Without explicitly sequencing our nice, pure code the compiler can ensure that linearity is preserved. Idris 2 is experimenting with this as well. It seems like a pretty good idea. And all of this type level stuff is so useful that we want to do more of it. Dependently typed languages remove the separation between the type language and the language of terms. This is powerful stuff.

deleted 7y ago

[deleted]

darkkindness 7y ago

I read the OP differently. Type-level programming (not to be confused with type-oriented programming) is using the typechecker to perform computation on types, which proves guarantees at compiler time. In this case, types are less about documentation, they are literally proofs of properties of the program by construction. In fact, type-level programming is usually unreadable[0] unless the reader has deep knowledge of the specific language implementation of type families, functional dependencies, poly-kinds, etc (whatever permits typelevel programming in that language). I'm getting that the OP is arguing against these ad-hoc constructs (type families etc) and would much rather write these proofs in the same language as ordinary code (e.g. writing the law "List x where length(x) == 5" in the type rather than "forall a. List (S (S (S (S (S Z))))) a") which, well who can disagree? In a sense, you and OP both agree on the same thing. Types are good. No types (or unreadable ad-hoc constructs for types) are not good. [0]: https://aphyr.com/posts/342-typing-the-technical-interview https://aphyr.com/posts/342-typing-the-technical-interview uses type-level programming in Haskell to solve N-queens