<p>As they explain in the related work section of the 2008 paper, the constraint types they describe are most closely related to <em>refinement types</em>. I wont give references, as there are plenty in the bibliography of the aforementioned paper, but I can give a quick overview.</p>

<p>Refinement types are a <em>language</em> that allow the expression of <em>refinements</em> of the <em>values</em> of a given type $C$: if $C$ is identified with the expressions of that type, then a refinement $R$ of $C$ is simply a <em>subset</em> $R\subseteq C$.</p>

<p>This is extremely helpful, as may allow the expression of <em>invariants</em> that the code needs to satisfy: say you have a type <code>Rectangle</code> with three fields, <code>width</code>, <code>height</code> and <code>area</code>. You are interested in the type in which <code>area = width*height</code>, which you might write:</p>

<pre><code>{ x :: Rectangle | x.area == x.width*x.height)
</code></pre>

<p>This is useful for expressing pre and post-conditions on your code. Again, a trivial example would be the <code>head</code> function, which only makes sense on non-empty lists.</p>

<pre><code>head :: NonEmptyList&lt;A&gt; -&gt; A
</code></pre>

<p>In this respect, refinement types capture the notion of <em>contracts</em>, and are also related to <em>axiomatic semantics</em> or <em>Hoare logic</em>.</p>

<p>So here's the real issue: what <em>is</em> the language for expressing refinements? Say we authorize linear constraints, in wich we can have</p>

<pre><code>n :: { x : Int | x &lt; 2 }
</code></pre>

<p>and on the other hand we have a function of type</p>

<pre><code>f :: { x : Int | x &lt;= 1+1 } -&gt; Bool
</code></pre>

<p>It is clear that <code>f</code> can safely be applied to <code>n</code>. However, for this to be statically verified, we need to <strong>prove</strong> the statement:
$$ x &lt; 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 <em>decidable</em> (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.</p>

<hr>

<p>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 <em>programmer</em> rather than on the compiler.</p>

<p>In this setting, an element of <code>{ x : Int | x &lt; 2 }</code> is not an integer less than 2, but a pair <code>(n, e)</code> where <code>n</code> is an integer and <code>e</code> is <em>evidence</em> that <code>n&lt;2</code> holds. Therefore the compiler only has to check the evidence at compile time, rather than building it herself.</p>

<p>Note however that some <em>computational inferences</em> can be performed, typically $1+1$ can be seen to be identical to $2$ (but $x&lt;2$ can not be seen to imply $x\leq 2$ without some contribution from the user).</p>

<p>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).</p>

<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2013-03-25T03:00:24.530Z
One point I am still not sure about is that refinements  or restraints are limitet to the "immutable state of objects". In other words "Constrained types statically
capture many common invariants that naturally arise in code.". So that is just the difference to dependent type , where to actual values, e.g., i,j,k say in matrix multiplication are only known at rutime, i.e.: ∀(i , j , k :  N)  → (Mat i j) → (Mat j k) → (Mat i k)
mrsteve
CC BY-SA 3.0
2013-03-25T15:35:59.717Z
I'm not sure I understand your question. There are refinement type systems which may capture your matrix example, see e.g. ATS:http://www.ats-lang.org/
cody
CC BY-SA 3.0
2013-03-26T09:45:14.790Z
@mrsteve: no, this is precisely the kind of invariant X10 *can* handle. X10 has the requirement that you can only be dependent on immutable fields of objects. So you can depend on matrix's shape, but not on its elements, since the elements can be updated imperatively. In a functional type theory like Agda or Coq, *all* data is immutable, so you can depend on anything.
Neel Krishnaswami
CC BY-SA 3.0
2013-03-22T16:05:36.217Z
2013-03-22T16:05:36.217Z
cody
<p>Constraint types have been proposed by IBM in their X10 programming language (it's a commercial programming language, not open source software).</p>

<p>Nystrom, Nathaniel, et al. "Constrained types for object-oriented languages." ACM Sigplan Notices. Vol. 43. No. 10. ACM, 2008.
<a href="http://www.model.in.tum.de/um/reading-group/Grothoff.oopsla08.pdf" rel="nofollow">http://www.model.in.tum.de/um/reading-group/Grothoff.oopsla08.pdf</a></p>

<p>How do “constraint types” compare to dependent types? Or do they resemble more one of the haskell extensions that simulate dependent types?</p>

<p>Can say the vector append from Agda be typed as say Lists in X10?</p>

<pre><code>_++_ : ∀ {m n} {A : Set} → Vec A m → Vec A n → Vec A (m + n)  
</code></pre>

<p>Further references on constraint types:</p>

<p>Saraswat, Vijay, et al. "Constrained Types-Future Directions." CP-18th International Conference on Principles and Practice of Constraint Programming-2012. 2012.
<a href="http://www.cs.nyu.edu/~lianah/files/CP-2012.pdf" rel="nofollow">http://www.cs.nyu.edu/~lianah/files/CP-2012.pdf</a></p>

<p>Nystrom, Nathaniel, et al. "Genericity through Constrained Types.
<a href="http://www.nanocow.com/nystrom/papers/generics.pdf" rel="nofollow">http://www.nanocow.com/nystrom/papers/generics.pdf</a></p>

<p>Tardieu, Olivier, et al. "Constrained kinds." Proceedings of the ACM international conference on Object oriented programming systems languages and applications. ACM, 2012.
<a href="http://www.inf.usi.ch/faculty/nystrom/papers/res0179-tardieu.pdf" rel="nofollow">http://www.inf.usi.ch/faculty/nystrom/papers/res0179-tardieu.pdf</a></p>

<pl.programming-languages><type-theory><type-systems><dependent-type>
Constraint types (IBM/X10) compared to dependent types
mrsteve
# Constraint types (IBM/X10) compared to dependent types

(Asked by: username_0 on 2013-03-21)

Constraint types have been proposed by IBM in their X10 programming language (it's a commercial programming language, not open source software).
Nystrom, Nathaniel, et al. "Constrained types for object-oriented languages." ACM Sigplan Notices. Vol. 43. No. 10. ACM, 2008.
http://www.model.in.tum.de/um/reading-group/Grothoff.oopsla08.pdf
How do “constraint types” compare to dependent types? Or do they resemble more one of the haskell extensions that simulate dependent types?
Can say the vector append from Agda be typed as say Lists in X10?
_++_ : ∀ {m n} {A : Set} → Vec A m → Vec A n → Vec A (m + n)  

Further references on constraint types:
Saraswat, Vijay, et al. "Constrained Types-Future Directions." CP-18th International Conference on Principles and Practice of Constraint Programming-2012. 2012.
http://www.cs.nyu.edu/~lianah/files/CP-2012.pdf
Nystrom, Nathaniel, et al. "Genericity through Constrained Types.
http://www.nanocow.com/nystrom/papers/generics.pdf
Tardieu, Olivier, et al. "Constrained kinds." Proceedings of the ACM international conference on Object oriented programming systems languages and applications. ACM, 2012.
http://www.inf.usi.ch/faculty/nystrom/papers/res0179-tardieu.pdf

**Tags:** pl.programming-languages, type-theory, type-systems, dependent-type

---

## 1 answers

### Answer by username_1 on 2013-03-22. Score: 10 | Accepted answer

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

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.

> **Comments:**
> **username_0**: One point I am still not sure about is that refinements  or restraints are limitet to the "immutable state of objects". In other words "Constrained types statically capture many common invariants that naturally arise in code.". So that is just the difference to dependent type , where to actual values, e.g., i,j,k say in matrix multiplication are only known at rutime, i.e.: ∀(i , j , k :  N)  → (Mat i j) → (Mat j k) → (Mat i k)  
> **username_1**: I'm not sure I understand your question. There are refinement type systems which may capture your matrix example, see e.g. ATS:http://www.ats-lang.org/  
> **username_2**: @mrsteve: no, this is precisely the kind of invariant X10 *can* handle. X10 has the requirement that you can only be dependent on immutable fields of objects. So you can depend on matrix's shape, but not on its elements, since the elements can be updated imperatively. In a functional type theory like Agda or Coq, *all* data is immutable, so you can depend on anything.  

---

