Good information about type systems based on contracts/constraints?

Question

Hello!

Problem:

I am looking for good introduction about type systems, which are based on contracts/constraints
(sorry, I don't remember which term one is appropriate for a type system).

I need that information to be able to implement an experimental type system of such kind.

As far as I know, such type system is used in XSD (Xml Schema Definition).

Instead of defining a data type, one defines constraints on the set of possible values.

Example:

I define some method with a parameter, which is either "nothing", or matches the integral range [0..100].

Such method would accept following values:

"nothing"
0
1
...
100

I hope, I could make my self clear.

Answer 1

You can have a look at languages like Haskell, or even Agda. Also, Oleg has lots of great resources.

Answer 2

This is not my area of expertise, so it might be off topic, but Microsoft Research has a project Code Contracts, which "provide a language-agnostic way to express coding assumptions in .NET programs. The contracts take the form of preconditions, postconditions, and object invariants".

Answer 3

Common Lisp offers such type testing at run time. It has an elaborate type system, but it's not used as you might be accustomed to in a statically-typed language. The macro check-type accepts a typespec, which can be a built-in specification or one defined by the macro deftype. The constraints expressible with typespecs are those of a predicate function written in the host language, which is to say that anything you can inspect a run time can be the criteria for what constitutes your new type.

Consider this example:

(defun is-nothing (val)
  (when (stringp val)
    (string= val "nothing")))

(deftype strange-range ()
  "A number between 0 and 100 inclusive, or the string \"nothing\"."
  '(or (integer 0 100)
       (satisfies is-nothing)))

That defines a type called "strange-range". Now test a few values against it:

CL-USER> (let ((n 0))
           (check-type n strange-range))
NIL
CL-USER> (let ((n 100))
           (check-type n strange-range))
NIL
CL-USER> (let ((n "nothing"))
           (check-type n strange-range))
NIL
CL-USER> (let ((n 101))
           (check-type n strange-range))

The last one triggers the debugger with the following message:

The value of N should be of type STRANGE-RANGE.
The value is: 101
   [Condition of type SIMPLE-TYPE-ERROR]

This one provokes the same outcome:

CL-USER> (let ((n "something"))
           (check-type n strange-range))

The constraints one can impose this way are expressive, but they don't serve the same purpose that the elaborate type systems of languages like Haskell or Scala do. While type definitions can coax the Common Lisp compiler to emit code more tailored to and efficient for the types of the operands, the examples above are more of a concise way to write run-time type checks.