Hacker News Reader

Comment by davedx | Hacker News Reader

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.

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?

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) without fully supporting dependent types.

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.

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-...

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?]

> 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.

"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

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.

> The value does not exist during compilation.

    type Z = []["length"]
    type One = [0]["length"]
    type Two = [0,0]["length"]

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.

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>).

Well, I can't be bothered to edit wikipedia, but it's a confusing claim. Dependent typing does not require runtime information, results can be produced at compile time. The dependent type depends on a value, but the interesting property of the value is independently tracked in the type system, it's not retrieved from runtime information.

The gist of how it works is so:

    createEmptyIntList() => List<size=0, content=int> {...}
    push(List<size=a, content=b>) => List<size=a+1, content=b> {...}
    firstElement(List<size=a, content=b> | a > 0) => b {...}

In this example, you don't need to know runtime values, you need to know that you can safely get the first element. For that, you just need to know that something has been pushed at least once in the list.

Since push returns a type that is different from createEmptyList, your typesystem has this information.

Reply on news.ycombinator.com