7
$\begingroup$

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

$\endgroup$

1 Answer 1

10
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ 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) $\endgroup$
    – mrsteve
    Mar 25, 2013 at 3:00
  • $\begingroup$ I'm not sure I understand your question. There are refinement type systems which may capture your matrix example, see e.g. ATS:ats-lang.org $\endgroup$
    – cody
    Mar 25, 2013 at 15:35
  • 1
    $\begingroup$ @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. $\endgroup$ Mar 26, 2013 at 9:45

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.