Dependent Typing

A DependentTyping system describes types in terms of the values that inhabits the type. I.e. in a DependentTyping system, one could discuss all prime numbers, all unbalanced trees, all linked lists of more than fifty items, the type described by the set of integers {1,2,3}, etc.

No value in a DependentTyping system can be given a single type; values can only ever be said to conform to a type. This is because the only smallest type for a particular value is the trivial type that describes that precise value, but such a type description is generally far too trivial to be of any value in the DependentTyping system. (I.e. the value 3 is a prime, is an integer, is a positive integer, is a non-negative integer, etc... but it's smallest type in a DependentTyping system is the type that contains only 3.) Because of this, traditional TypeInference (which assigns a single type to each value) is not useful in a DependentTyping system.

However, TypeInference over variables can still be of value. Such a system would need to return a type descriptor that carries the properties that the variable must carry. First order predicates over the values are easily sufficient type descriptors... though if types and type-descriptors are also values, then you're suddenly into higher-order logics.

For advantages, a DependentTyping system allows non-trivial proofs for properties of both type-safety and program correctness. In a StaticTyping system, it also allows many non-trivial optimizations.

However, this comes at a major cost. Determining whether a given type in a DependentTyping system actually contains any values, or contains only a unique value, is undecidable in the general case. Second, determining whether two different types are equal becomes a difficult problem, also generally undecidable. Third, determining whether a particular value belongs to a type can trivially be turned into an NP-hard problem or problem for which there is no known polynomial-time solution. To make these decisions practical, DependentTyping is often limited to languages where termination can be guaranteed.

As such, when working with a statically checked DependentTyping system, programmers must be careful to limit their own expressiveness to that which they're willing to wait on when it comes time for TypeChecking, and they need to know that simply waiting for a very long time on a very powerful machine won't necessarily make the proofs happen. Systems to speed up proofs are incredibly valuable. (A trivial aid is to memoizing previous successful proofs in the compile-test-modify cycle.)

Use of ManifestTyping on variables and functions can also significantly simplify the overall proof process and further aid in communication and documentation. This is, at least in part, because programmers lack the tendency to describe the sort of massively complex types that might otherwise exist in a fully TypeInference based DependentTyping system. These do force the programmer to deal with all possible cases of these simpler types and prevents some optimizations on the external interfaces to a module, but that is generally an acceptable loss due to the gain in both simplicity and the ability to easily modularize code.

TypeInference in a DependentTyping system and ConstraintProgramming are something like duals of one another, at least informally. TypeInference finds the necessary DependentTypes to prove or disprove safety over every application of function value to input value, while ConstraintProgramming finds the necessary value(s) to meet 'constraints', which may also be expressed in terms of DependentTypes.

The above isn't 'official'. It's my understanding of the topic.

Perhaps this is the ideal solution to the old "Circle vs Oval" type problem? A circle is a dependant type of an oval. This, of course, leads one to start thinking: "can I provide optimizations to my dependant type"? That is, can I do some neat ExternalPolymorphism tricks where I check if a circle is an oval or a normal circle and do different operations on it? Having learned AdaLanguage in school, I've always felt that mainstream OOP type systems are missing something in not being able to intuitively model units of measure, constraints, etc.

It can easily handle CircleAndEllipseProblem when discussing values (which are mathematical and immutable). However, DependentTyping is generally described as being over values, not MutableState, so it doesn't handle the Circle vs. Ellipse Objects particularly well. The mathematical 'value' or 'type' an object can usually be described only in terms of its invariants (the messages and message protocols it accepts, the guarantees it makes over multiple-message interactions, etc.) and its momentary state (the value held by its state at some particular point in time). If the object can be described as having a value that is a function of time, then that works well enough... but that's not usually the case, as there is no static, compile-time-predictable function of time for object state, so we're left with invariants... the messages and discussions an object can handle, and any promises it makes.
I suppose, though, that if you can guarantee that you're the only one interacting with the object, and you can prove that you don't send any messages the objects can't properly handle or that ruin any assumptions you've made, then it may be possible to treat a circular ovalObject as a circleObject when the situation is right. It is certainly possible to automatically start accepting requests for things like 'radius' on an ovalObject when conditions are correct, especially in DynamicTyping systems. OTOH, if you cannot guarantee that you're the only one interacting with the object (e.g. in a highly concurrent system) then this problem cannot be handled by DependentTyping at all because you cannot guarantee the needed invariants for the duration of your interaction. Type-safety checks of any sort can be invalidated within microseconds of you performing them. A perfectly circular ovalObject cannot be safely treated as a circleObject if it might change and lose its 'radius' accessor while you're in the middle of observing it.