5 ms·

I’d love to be able to do dependent types in TS. Does this make that possible?

by davedx 3y ago

frogulis 3y ago
Might be wrong here, but I'm of the understanding that a dependent type system is undecidable, and so to have static dependent types you need to have a more restricted language, like the inability to write arbitrarily recursive functions. In short I don't think so but I'd also love a good explanation as to why I'm wrong.
- pxeger1 3y ago
  Typescript's type system is already undecidable (except that they limit recursion depth). I don't know much about dependent types but I'd guess it similarly doesn't matter much in practice that in the general case they're undecidable?
- Smaug123 3y ago
  A fully-featured dependent type system may be undecidable, but that doesn't mean you can't make one - it just means that there will be valid programs that the type checker nevertheless rejects, or there will be valid programs for which the type checker never terminates. It doesn't stop you from creating a type checker in the first place; it just weakens the guarantees you can make about that type checker. The Typescript type checker is (or at least was) already Turing-complete (https://github.com/microsoft/TypeScript/issues/14833 https://github.com/microsoft/TypeScript/issues/14833) without fully supporting dependent types.
amitport 3y ago
No. Typescript cannot access runtime values (I assume you mean types that depend on runtime values). In TypeScript types can depend on other types and it does support literal types which covers a lot of use cases. What do you need dependent types for? [Edit: why the down vote?]
- deleted 3y ago
  [deleted]
- pyrale 3y ago
  > No. Typescript cannot access runtime values (I assume you mean types that depend on runtime values). That's not the meaning of dependent types, and dependent type checkers don't require runtime information.
  - amitport 3y ago
    "a dependent function may depend on the value (not just type) of one of its arguments" from wikipedia https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type The value does not exist during compilation. AFAIKT dependent type are used mostly during executable proof checkers to verify claims on the value-dependent types. So maybe using the term runtime is a bit to specific, but you do not have values (except literals) during typescript execution phase.
    - ReleaseCandidat 3y ago
      > The value does not exist during compilation. type Z = []["length"] type One = [0]["length"] type Two = [0,0]["length"]
    - PhilipRoman 3y ago
      The "value" in this case is symbolic, sort of like defining an array with variable length arr[x] and having the compiler verify that arr[x+5] is always out of bounds before knowing the actual value of x. If the type system is not powerful to prove correctness of some expression, you will need to insert a runtime check that lets the compiler to trust the value at compile time.
      - reuben364 3y ago
        You still need a way of normalizing expressions that is consistent with your runtime. To say that types ((x: bool) => F<true && x>) and ((x: bool) => F<false || x>) are the same, wrt judgemental equality, requires normalizing both to ((x: bool) => F<x>).
pyrale 3y ago
I guess you could use it to implement an algebra that allows you to build dependent types, but that would be unfit for practical uses. As a case in point, Haskell has first-class experience for HKTs, and dependent types implementation in haskell is getting hindered by the limits of the language.
- ReleaseCandidat 3y ago
  For anybody interested in the details, here is the last report of the ongoing implementation of dependent types in GHC: https://discourse.haskell.org/t/ghc-dh-weekly-update-6-2023-06-07/6383 https://discourse.haskell.org/t/ghc-dh-weekly-update-6-2023-...

I’d love to be able to do dependent types in TS. Does this make that possible?

by davedx 3y ago

I’d love to be able to do dependent types in TS. Does this make that possible?

Might be wrong here, but I'm of the understanding that a dependent type system is undecidable, and so to have static dependent types you need to have a more restricted language, like the inability to write arbitrarily recursive functions. In short I don't think so but I'd also love a good explanation as to why I'm wrong.

pxeger1 3y ago
Typescript's type system is already undecidable (except that they limit recursion depth). I don't know much about dependent types but I'd guess it similarly doesn't matter much in practice that in the general case they're undecidable?
Smaug123 3y ago
A fully-featured dependent type system may be undecidable, but that doesn't mean you can't make one - it just means that there will be valid programs that the type checker nevertheless rejects, or there will be valid programs for which the type checker never terminates. It doesn't stop you from creating a type checker in the first place; it just weakens the guarantees you can make about that type checker. The Typescript type checker is (or at least was) already Turing-complete (https://github.com/microsoft/TypeScript/issues/14833 https://github.com/microsoft/TypeScript/issues/14833) without fully supporting dependent types.

amitport 3y ago

No. Typescript cannot access runtime values (I assume you mean types that depend on runtime values). In TypeScript types can depend on other types and it does support literal types which covers a lot of use cases. What do you need dependent types for? [Edit: why the down vote?]

deleted 3y ago
[deleted]
pyrale 3y ago
> No. Typescript cannot access runtime values (I assume you mean types that depend on runtime values). That's not the meaning of dependent types, and dependent type checkers don't require runtime information.
- amitport 3y ago
  "a dependent function may depend on the value (not just type) of one of its arguments" from wikipedia https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type The value does not exist during compilation. AFAIKT dependent type are used mostly during executable proof checkers to verify claims on the value-dependent types. So maybe using the term runtime is a bit to specific, but you do not have values (except literals) during typescript execution phase.
  - ReleaseCandidat 3y ago
    > The value does not exist during compilation. type Z = []["length"] type One = [0]["length"] type Two = [0,0]["length"]
  - PhilipRoman 3y ago
    The "value" in this case is symbolic, sort of like defining an array with variable length arr[x] and having the compiler verify that arr[x+5] is always out of bounds before knowing the actual value of x. If the type system is not powerful to prove correctness of some expression, you will need to insert a runtime check that lets the compiler to trust the value at compile time.
    - reuben364 3y ago
      You still need a way of normalizing expressions that is consistent with your runtime. To say that types ((x: bool) => F<true && x>) and ((x: bool) => F<false || x>) are the same, wrt judgemental equality, requires normalizing both to ((x: bool) => F<x>).

pyrale 3y ago

I guess you could use it to implement an algebra that allows you to build dependent types, but that would be unfit for practical uses. As a case in point, Haskell has first-class experience for HKTs, and dependent types implementation in haskell is getting hindered by the limits of the language.

ReleaseCandidat 3y ago
For anybody interested in the details, here is the last report of the ongoing implementation of dependent types in GHC: https://discourse.haskell.org/t/ghc-dh-weekly-update-6-2023-06-07/6383 https://discourse.haskell.org/t/ghc-dh-weekly-update-6-2023-...