in theory no, because you run into the halting problem. but even in practical terms it would impede your ability to do static type analysis long before that point.
I don't really care about static type analysis, in a sense:
If I write an assertion `x is a number`, then fine, statically analyze that, that works today.
If I write a hard-to-compute assertion like `x is Prime` (or `x is a counterexample to the Riemann Hypothesis`), then I don't care if the compiler can statically figure it out. It can simply require all callers to test that before calling this function, they assert `x is Prime` directly -- no analysis required. This way my function can be sure it is only called with prime numbers, but nobody has to write any logic in a typechecker that can figure out whether that's true for arbitrary inputs.
I believe that's what dependent types allow you to do.
However, even in weaker type systems you can get a similar effect by just creating a PrimeNumber type, and for functions that require a prime number, only accept PrimeNumber. Then any number you want to pass to those functions will have to go through PrimeNumber's constructor.
What are the callers supposed to do when the assertion fails? Either you carry the assertion all the way back to the point where x is created - in which case you're implementing a type system, whether you call it that or not - or you have code that will have runtime failures in the middle of your computations.
> you have code that will have runtime failures in the middle of your computations.
Preferably during running of your unit-tests.
In practice much of the software we use today has runtime errors. How the code handles those varies. Static typing does not prevent runtime errors does it?
Which means you need more unit test coverage, have more tests to maintain, and your code structure becomes more brittle.
> Static typing does not prevent runtime errors does it?
Often it does; and if a validation rule is too complex or externally-dependent to enforce at compile time, static typing at least lets you push checking to the start of an operation, rather than in the middle of your computation.
that usually gets classified under contracts rather than types. eiffel is probably the best known example of a contract based language, but also check out typed racket, it uses a nice mix of types and runtime contracts in a dynamic language.
That is good vocabulary. Clearly there is a difference between static type-checking and assertions. But "types" is not the same as "type-checking". Type-checking can happen at runtime, or at compile-time. Or both.
My point was more that static type-checking can be seen equivalent to assertions, except it checks those assertions at compile time and typically lacks some expressive power compared to assertions, in most practical programming languages today.
Static type-checking is more a feature of the compiler than of the language. Consider type-inference: You can have a language where types are not explicitly declared most of the time. Yet they can be checked at compile-time, assuming you have a compiler that is able to perform that amazing feat.
