4 ms·

Invariants need to be encoded one way or another anyway, you can't escape that. If your type system is not sophisticated enough this gets tedious and awkward to

by 4ad 2y ago

Invariants need to be encoded one way or another anyway, you can't escape that. If your type system is not sophisticated enough this gets tedious and awkward to do in the type system, so it's easier to do in (dynamic) code. But dependent types simplify this, they make it much easier to express yourself in types compared to, say, all the various fancy extensions to System F. Computing types becomes just like computing terms. That said, there is a vast design space between Javascript/Python and dependent types. Plain old ADT suffice in 95% of cases, yet the only mainstream language with ADTs is Rust. This is a shame.

yen223 2y ago
(Assuming ADT here refers to Algebraic Data Types, as opposed to abstract data types) Swift, Kotlin, Scala and Typescript all support forms of ADTs, just with different names. - Swift calls them "enums" (like Rust) - Kotlin and Scala has "sealed classes" - Typescript has "discriminated unions"
- 4ad 2y ago
  I forgot about Swift, that's true (and great). Kotlin (and even Java 15+ nowadays) can emulate ADTs with sealed classes, but the ergonomics are incredibly bad and the ecosystem is not build around the concept. Scala has ADTs, but I would put Scala in the same category as Haskell or OCaml. A niche language. Typescript does not have ADT, they have union types. You can build a discriminated type out of a union type, but you have to do this manually. This misses on the ergonomics of using ADTs plus people do it in different ways. ADTs in one way or another are becoming more mainstream, but they are very far from being accepted by default.
  - yen223 2y ago
    Agree with you on the ergonomics of sealed classes in kotlin/scala/java. It works, but it's clunky. I quite like Typescript's approach. You do get exhaustive switch-case matching, so that's like 80% of what I want out of sum types. Typescript also lets you enforce that a type is one of the variants of a sum type, something which e.g. Haskell doesn't let you do. I assume this is a function of Typescript doing union types, but it's pretty convenient. Definitely see ADTs becoming mainstream, because they are genuinely useful. Biggest gap to adoption imo is that no SQL database supports sum types or anything equivalent.
    - DylanSp 2y ago
      Typescript's exhaustiveness checking can be kind of clunky sometimes, particularly if you have a switch statement that's just causing side effects and not returning a value. Last time I looked at it, I think you had to add a default case with some sort of dummy statement assigning a value to a variable with type `never`; while that's doable, the ergonomics are a bit annoying.
      - yen223 2y ago
        I recall having to add that dummy 'never' branch in the past, but I haven't had to do that in newer projects on recent versions of Typescript.
        DylanSp 2y ago
        I just tried it in the online playground. I didn't get any sort of error with one of the cases unhandled. https://www.typescriptlang.org/play/?noFallthroughCasesInSwitch=true&q=115#code/C4TwDgpgBAKglgWzgOwOYFEBuFnCgXigG8pkBDBCALigCIBnYMgJ2FoG4oBXeiZgZSasIAExoAjAPaSANhDLIoAXygAfYqQrU6AYxmTeIjlBFdmZYHEnIayLgnF9l7AFBud1xlAAWCkXKwcPEIACghsXBp4JDRA3ABKAgA+YhcoKHoAdzhgHW8oMIjgADpySkSiNPSoHTJeOkYWNioq6prPPBQcuAtRACEQAFVeZgIocKDinj5BJtFXNvSPZHpZCGL9VBCuy16RAeG+eIXF8WZ5AGtXVqgAeluauuhaPQNRWha2++rlr0tKehgBRjCa4YqmcyWawndLfdJnS4nJQuJSuIA https://www.typescriptlang.org/play/?noFallthroughCasesInSwi...
        yen223 2y ago
        Hmm. I think this is because in that situation, all cases (including the unhandled one) are "correctly" returning undefined. I can see that if I made the branch return a string, Typescript will correctly show the "Not all code paths return a value" error
        DylanSp 2y ago
        Yep, or if you declare an explicit return type for the function, TS correctly gives a "Function lacks ending return statement and return type does not include 'undefined'." error. But if you have a function that's purely side-effecting, I think you still have to do something manual.
DylanSp 2y ago
I definitely agree that ADTs are a big step forward; when I learned about them from Haskell, I was kind of baffled that they weren't more common, because the concept of "this value is always either type A or type B" is pretty simple and occurs a lot. I really wish Go had included them, because it doesn't seem like a terribly complex concept, the type switch syntax would work decently for basic pattern matching, and having ADTs built into the ecosystem from the start would be much smoother.

by 4ad 2y ago

yen223 2y ago

(Assuming ADT here refers to Algebraic Data Types, as opposed to abstract data types) Swift, Kotlin, Scala and Typescript all support forms of ADTs, just with different names. - Swift calls them "enums" (like Rust) - Kotlin and Scala has "sealed classes" - Typescript has "discriminated unions"

4ad 2y ago
I forgot about Swift, that's true (and great). Kotlin (and even Java 15+ nowadays) can emulate ADTs with sealed classes, but the ergonomics are incredibly bad and the ecosystem is not build around the concept. Scala has ADTs, but I would put Scala in the same category as Haskell or OCaml. A niche language. Typescript does not have ADT, they have union types. You can build a discriminated type out of a union type, but you have to do this manually. This misses on the ergonomics of using ADTs plus people do it in different ways. ADTs in one way or another are becoming more mainstream, but they are very far from being accepted by default.
- yen223 2y ago
  Agree with you on the ergonomics of sealed classes in kotlin/scala/java. It works, but it's clunky. I quite like Typescript's approach. You do get exhaustive switch-case matching, so that's like 80% of what I want out of sum types. Typescript also lets you enforce that a type is one of the variants of a sum type, something which e.g. Haskell doesn't let you do. I assume this is a function of Typescript doing union types, but it's pretty convenient. Definitely see ADTs becoming mainstream, because they are genuinely useful. Biggest gap to adoption imo is that no SQL database supports sum types or anything equivalent.
  - DylanSp 2y ago
    Typescript's exhaustiveness checking can be kind of clunky sometimes, particularly if you have a switch statement that's just causing side effects and not returning a value. Last time I looked at it, I think you had to add a default case with some sort of dummy statement assigning a value to a variable with type `never`; while that's doable, the ergonomics are a bit annoying.
    - yen223 2y ago
      I recall having to add that dummy 'never' branch in the past, but I haven't had to do that in newer projects on recent versions of Typescript.
      - DylanSp 2y ago
        I just tried it in the online playground. I didn't get any sort of error with one of the cases unhandled. https://www.typescriptlang.org/play/?noFallthroughCasesInSwitch=true&q=115#code/C4TwDgpgBAKglgWzgOwOYFEBuFnCgXigG8pkBDBCALigCIBnYMgJ2FoG4oBXeiZgZSasIAExoAjAPaSANhDLIoAXygAfYqQrU6AYxmTeIjlBFdmZYHEnIayLgnF9l7AFBud1xlAAWCkXKwcPEIACghsXBp4JDRA3ABKAgA+YhcoKHoAdzhgHW8oMIjgADpySkSiNPSoHTJeOkYWNioq6prPPBQcuAtRACEQAFVeZgIocKDinj5BJtFXNvSPZHpZCGL9VBCuy16RAeG+eIXF8WZ5AGtXVqgAeluauuhaPQNRWha2++rlr0tKehgBRjCa4YqmcyWawndLfdJnS4nJQuJSuIA https://www.typescriptlang.org/play/?noFallthroughCasesInSwi...
        yen223 2y ago
        Hmm. I think this is because in that situation, all cases (including the unhandled one) are "correctly" returning undefined. I can see that if I made the branch return a string, Typescript will correctly show the "Not all code paths return a value" error
        DylanSp 2y ago
        Yep, or if you declare an explicit return type for the function, TS correctly gives a "Function lacks ending return statement and return type does not include 'undefined'." error. But if you have a function that's purely side-effecting, I think you still have to do something manual.

DylanSp 2y ago

I definitely agree that ADTs are a big step forward; when I learned about them from Haskell, I was kind of baffled that they weren't more common, because the concept of "this value is always either type A or type B" is pretty simple and occurs a lot. I really wish Go had included them, because it doesn't seem like a terribly complex concept, the type switch syntax would work decently for basic pattern matching, and having ADTs built into the ecosystem from the start would be much smoother.