4 ms·

I know I'll likely get a biased answer here but what do you think the cons are of using types in this way? My current thinking is that types should should optim

I know I'll likely get a biased answer here but what do you think the cons are of using types in this way? My current thinking is that types should should optimize for an easy learning curve so folks can just get on with writing code. This seems like it would require a deep knowledge of TS. lodash does come to mind in fact. The last few shops where I've worked use a very small subset of lodash utilities and ignore most of the library. Their documentation is terse so it's often easier to just write your own code that is longer but more readable to the average engineer.

mpoteat 3y ago
Well, slower compile times, and additional complexity are the biggest cons. There is a project I'm working on to eliminate the latter bit - ideally, a way to represent these complex types with "zero type-level code"
- Byamarro 3y ago
  Could you elaborate on the project? I'm curious
imiric 3y ago
Conversely, and I don't mean to sound flippant, but are there any pros of (ab)using types in this way? These projects are interesting in an amusing "oh look, another Turing complete type system" way, for the author to gain expertise, and as something to highlight in CVs and to chat about during interviews. But other than that, I would never actually choose to use any of this in a real-world project. Depending on the stability of this API (TPI?), and subjecting colleagues to esoteric libraries would be a nightmare to maintain and support.
- amw-zero 3y ago
  The pros of any type-level logic all boil down to automatically enforcing something that you want to be enforced. The key word being _automatically_. This can be frustrating in the moment sometimes, but other times a type can do two really powerful things: 1. prevent someone you’ve never spoken to from doing something legitimately dangerous 2. provide browsable documentation about the constraint its enforcing and how other places in the code resolve the constraint. It doesn’t always work out that way, sure, but that’s the ideal types are striving for.
  - troupo 3y ago
    > provide browsable documentation about the constraint its enforcing and how other places in the code resolve the constraint. It doesn't provide "browsable documentation". It provides complex unreadable types that you have to painstakingly manually "compile" in your head to figure out what the hell is going on
    - shadowgovt 3y ago
      Generally (at least if we're talking typescript and vscode), the IDE serves as a REPL UI for the type system. You don't have to compile in your head; you can declare a variable or assignment with some type property and see where an error is thrown.
      - troupo 3y ago
        For errors that can be automatically fixed by IDE, yes. It doesn't make this documentation ;) I've seen quite a few cases where IDE's type expansion (whether on hover or in type errors) would result in a dozen lines of nested types. Worse than no documentation at all.
        shadowgovt 3y ago
        A dozen lines of nested types are like a dozen lines of source code, and I generally recommend treating them the same if they aren't legible: poke it with a REPL (in this case, try to declare a variable or new type that should work if your understanding of the types are correct) and see what the tools say. (And, of course, as with other source code, illegibility implies more documentation needed. For type systems in particular, I think people tend to under-declare their types [i.e. they'll do "Record<KeyType, Array<{name: string, address: string}>" instead of "Record<KeyType, EmployeeRecords>"], which gives the compiler fewer hooks to shortcut talking about a complex type). There is one thing consistently true about type systems that frustrates me: I write in procedural code all day, but basically all type systems are functional code. It is frustrating to have to spin my reasoning around to attack a problem in a different language structure when I've been doing straight-line statement-by-statement all day. I don't have a solution to that, but I observe the challenge.
movpasd 3y ago
If you push all your code into the type system, you're basically just writing your program in a clunkier, less readable language. So, you will just end up having to debug your type system, which defeats the whole purpose. I think expressive type systems are great, but like most things in engineering, it's a trade-off; the complexity of having to manually manage invariants vs. the complexity of managing the type system.
- madsbuch 3y ago
  > If you push all your code into the type system, you're basically just writing your program in a clunkier, less readable language. It would be funny to see web servers running the typescript compiler (type checker) instead of a JS runtime, though.
- xmcqdpt2 3y ago
  The correct balance depends on how critical the piece of code you are working on is, and how much you want to write unit tests for it. In cases where the type system can encode the invariants you care about, it can be worth the extra complexity so that you have code that has compiler enforced correctness (at least in some aspects). Of course, you can't do this for any invariant in a given type system (eg lifetimes are not representable in Java). When it is possible though, debugging a type system has the advantage that it's done on your local machine, away from prod.

mpoteat 3y ago

Well, slower compile times, and additional complexity are the biggest cons. There is a project I'm working on to eliminate the latter bit - ideally, a way to represent these complex types with "zero type-level code"

Byamarro 3y ago
Could you elaborate on the project? I'm curious

imiric 3y ago

Conversely, and I don't mean to sound flippant, but are there any pros of (ab)using types in this way? These projects are interesting in an amusing "oh look, another Turing complete type system" way, for the author to gain expertise, and as something to highlight in CVs and to chat about during interviews. But other than that, I would never actually choose to use any of this in a real-world project. Depending on the stability of this API (TPI?), and subjecting colleagues to esoteric libraries would be a nightmare to maintain and support.

amw-zero 3y ago
The pros of any type-level logic all boil down to automatically enforcing something that you want to be enforced. The key word being _automatically_. This can be frustrating in the moment sometimes, but other times a type can do two really powerful things: 1. prevent someone you’ve never spoken to from doing something legitimately dangerous 2. provide browsable documentation about the constraint its enforcing and how other places in the code resolve the constraint. It doesn’t always work out that way, sure, but that’s the ideal types are striving for.
- troupo 3y ago
  > provide browsable documentation about the constraint its enforcing and how other places in the code resolve the constraint. It doesn't provide "browsable documentation". It provides complex unreadable types that you have to painstakingly manually "compile" in your head to figure out what the hell is going on
  - shadowgovt 3y ago
    Generally (at least if we're talking typescript and vscode), the IDE serves as a REPL UI for the type system. You don't have to compile in your head; you can declare a variable or assignment with some type property and see where an error is thrown.
    - troupo 3y ago
      For errors that can be automatically fixed by IDE, yes. It doesn't make this documentation ;) I've seen quite a few cases where IDE's type expansion (whether on hover or in type errors) would result in a dozen lines of nested types. Worse than no documentation at all.
      - shadowgovt 3y ago
        A dozen lines of nested types are like a dozen lines of source code, and I generally recommend treating them the same if they aren't legible: poke it with a REPL (in this case, try to declare a variable or new type that should work if your understanding of the types are correct) and see what the tools say. (And, of course, as with other source code, illegibility implies more documentation needed. For type systems in particular, I think people tend to under-declare their types [i.e. they'll do "Record<KeyType, Array<{name: string, address: string}>" instead of "Record<KeyType, EmployeeRecords>"], which gives the compiler fewer hooks to shortcut talking about a complex type). There is one thing consistently true about type systems that frustrates me: I write in procedural code all day, but basically all type systems are functional code. It is frustrating to have to spin my reasoning around to attack a problem in a different language structure when I've been doing straight-line statement-by-statement all day. I don't have a solution to that, but I observe the challenge.

movpasd 3y ago

If you push all your code into the type system, you're basically just writing your program in a clunkier, less readable language. So, you will just end up having to debug your type system, which defeats the whole purpose. I think expressive type systems are great, but like most things in engineering, it's a trade-off; the complexity of having to manually manage invariants vs. the complexity of managing the type system.

madsbuch 3y ago
> If you push all your code into the type system, you're basically just writing your program in a clunkier, less readable language. It would be funny to see web servers running the typescript compiler (type checker) instead of a JS runtime, though.
xmcqdpt2 3y ago
The correct balance depends on how critical the piece of code you are working on is, and how much you want to write unit tests for it. In cases where the type system can encode the invariants you care about, it can be worth the extra complexity so that you have code that has compiler enforced correctness (at least in some aspects). Of course, you can't do this for any invariant in a given type system (eg lifetimes are not representable in Java). When it is possible though, debugging a type system has the advantage that it's done on your local machine, away from prod.