# Constraints

A critical advantage of Whiley over other programming languages, such as Java or C#, is the ability to define constrained types. A constrained type is simply a type with a specific constraint imposed upon it. For example, the type of natural numbers can be defined like so:

```define nat as int where \$ >= 0
```

Here, “`\$`” is used to refer to the value held by a variable of type `nat`. Thus, we see that `nat` is an `int` whose values are never negative. Any attempt to pass a negative number to a variable of type `nat` will result in a compile-time error. The following program illustrates some simple methods:

```nat f(nat x):
return x + 1 // always OK

nat g(nat x):
return x - 1  // always a compile-time error

nat h(int y):
x = y      // always a compile-time error
```

Whiley reasons about the values of variables in a modular fashion. That is, it considers all the available information and attempts to determine whether a particular state is invalid or not. In the above example, the first function `f()` is valid because incrementing a natural number always gives a natural number. However, subtracting one from a natural number may give a negative number. Hence, function `g()` is considered invalid as `x` could be zero on entry. A similar argument applies for function `h()`.

Type constraints are not limited to primitive types, and can be used on any type. The following provides some more interesting examples:

```define nelist as [int] where |\$| > 0 // non-empty list
define zlist as {int} where !(0 in \$) // cannot contain 0
define dim as {int low, int high} where low < high
```

By using quantifiers, you can define more useful constraints on lists and sets. For example:

```define pset as {int} where no { x in \$ | x < 0 }
```

This defines a set type where no element can be negative (or, conversely, where every element must be a natural number). We can define this equivalently like so:

```define nat as int where \$ >= 0
define pset as {nat}
```

Whiley simply inlines the above definition for `nat` into that for `pset`, arriving at something similar to the previous definition.