Hacker News new | ask | show | jobs
by frogulis 1111 days 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.
2 comments
Smaug123 1111 days 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) without fully supporting dependent types.

link
pxeger1 1111 days 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?
link