As they explain in the related work section of the 2008 paper, the constraint types they describe are most closely related to refinement types. I wont give references, as there are plenty in the bibliography of the aforementioned paper, but I can give a quick overview.
Refinement types are a language that allow the expression of refinements of the values of a given type $C$: if $C$ is identified with the expressions of that type, then a refinement $R$ of $C$ is simply a subset $R\subseteq C$.
This is extremely helpful, as may allow the expression of invariants that the code needs to satisfy: say you have a type Rectangle
with three fields, width
, height
and area
. You are interested in the type in which area = width*height
, which you might write:
{ x :: Rectangle | x.area == x.width*x.height)
This is useful for expressing pre and post-conditions on your code. Again, a trivial example would be the head
function, which only makes sense on non-empty lists.
head :: NonEmptyList<A> -> A
In this respect, refinement types capture the notion of contracts, and are also related to axiomatic semantics or Hoare logic.
So here's the real issue: what is the language for expressing refinements? Say we authorize linear constraints, in wich we can have
n :: { x : Int | x < 2 }
and on the other hand we have a function of type
f :: { x : Int | x <= 1+1 } -> Bool
It is clear that f
can safely be applied to n
. However, for this to be statically verified, we need to prove the statement:
$$ x < 2 \Rightarrow x \leq 1+1$$
So this imposes a restriction on the expressivity of the refinement language: either the statements that need to be proven to verify type-safety are decidable (linear arithmetic and the theory of equality is a common choice in this case), or there need to be dynamic casts that are verified at runtime.
The traditional approach to dependent types, however, allows for arbitrarily complex constraints on types, with the following caveat: the onus of verification is placed on the programmer rather than on the compiler.
In this setting, an element of { x : Int | x < 2 }
is not an integer less than 2, but a pair (n, e)
where n
is an integer and e
is evidence that n<2
holds. Therefore the compiler only has to check the evidence at compile time, rather than building it herself.
Note however that some computational inferences can be performed, typically $1+1$ can be seen to be identical to $2$ (but $x<2$ can not be seen to imply $x\leq 2$ without some contribution from the user).
The obvious advantage is that arbitrarily complex constraints on the code can be verified, and the programmer may have access to automatic tools to assist the production of the required evidence (the famous "tactic language" of Coq is an example of this).
This is the main difference between refinement types and dependent types. The Haskell extensions tend to be in the second category, where evidence has to be provided by the programmer.
I do need to qualify all this: there is no hard line which differentiates refinement types from dependent types; in dependent types there may be a significant amount of information inferred by the compiler, and systems with refinement types may require information to be supplied by the developer. In fact the interaction between the communities contains IMHO some of the most interesting developments of type theory applied to practical software engineering.