2 ms·
You can do almost everything with dependent types, but dependent type systems expressive enough to be practical are usually heavy, permit almost no (guaranteed)
by mananaysiempre 5y ago
You can do almost everything with dependent types, but dependent type systems expressive enough to be practical are usually heavy, permit almost no (guaranteed) inference and tend to require a total language (unless you toss out soundness, like TypeScript does with its non-dependent types). The hope is usually that a weaker system might relieve some of these problems; besides, studying the weakest type systems that can express whatever it is you want is good mathematics in any case.
I’m absolutely hoping for a practical dependently typed language as well, but we still have a ways to go there.