4 ms·

How come none of the mainstream static type systems support dependent types? On paper they seem like such a neat idea for defining constraints and preventing bu

How come none of the mainstream static type systems support dependent types? On paper they seem like such a neat idea for defining constraints and preventing bugs. I heard Scala and Haskell have optional/partial support for them, so I suppose it takes a pretty sophisticated type system to begin with?

Sharlin 7y ago
To implement dependent types, your type system must go much deeper into the theorem prover territory than is normal in mainstream imperative programming languages (whose type systems are often more or less ad-hoc rather than based on rigorous theory). Furthermore, dependent types break the fundamental property that the relationship between types and terms is one-directional: types constrain terms but not the other way around. As one example, C++ has had non-type template parameters (types parameterized by values) for a long time, but only for compile-time constants. AFAIK there have been no formal proposals to introduce full-blown dependent types, rather the focus has been on improving the facilities for compile-time term-level computation.
mrkeen 7y ago
The problem is that mainstream static types systems have two massive holes in them: nulls and pervasive mutability. Knowing that a list has length n at compile time isn't that useful if you're expecting the program to change the list's length at runtime. Or maybe there was never a list in the first place because it was null.
6gvONxR4sf7o 7y ago
People are still figuring out how to make things "easy" with them. The theory says you can prove cool stuff, but the syntax to do that while making it approachable is still something people work on. But that's an outsider's perspective.
UK-Al05 7y ago
Dependent types are only recently becoming well known and popular. The type systems in mainstream languages were not built with these kind of flexibility required by dependent types.

Sharlin 7y ago

To implement dependent types, your type system must go much deeper into the theorem prover territory than is normal in mainstream imperative programming languages (whose type systems are often more or less ad-hoc rather than based on rigorous theory). Furthermore, dependent types break the fundamental property that the relationship between types and terms is one-directional: types constrain terms but not the other way around. As one example, C++ has had non-type template parameters (types parameterized by values) for a long time, but only for compile-time constants. AFAIK there have been no formal proposals to introduce full-blown dependent types, rather the focus has been on improving the facilities for compile-time term-level computation.

mrkeen 7y ago

The problem is that mainstream static types systems have two massive holes in them: nulls and pervasive mutability. Knowing that a list has length n at compile time isn't that useful if you're expecting the program to change the list's length at runtime. Or maybe there was never a list in the first place because it was null.

6gvONxR4sf7o 7y ago

People are still figuring out how to make things "easy" with them. The theory says you can prove cool stuff, but the syntax to do that while making it approachable is still something people work on. But that's an outsider's perspective.

UK-Al05 7y ago

Dependent types are only recently becoming well known and popular. The type systems in mainstream languages were not built with these kind of flexibility required by dependent types.