Types are sets

A type describes a set of values. Any value in that set is said to be of that type. A subclass of a type is a subset of the values. This may sound obvious, but it is good to keep in mind nevertheless.

Types are abstract

A type is not an implementation. You cannot "instantiate" a type directly. You can only construct values which satisfy the constraints of the type (and are thus members of the type's set). In C++/Java terms, all types are like purely abstract interfaces.

Types can be passed like values

Types in Evlan can be passed around just like functions and values. A function can take a type as one of its parameters or return a type as its result. A member field of an object can be a type, and that object's other fields can be based on that type.

For example, arrays contain a field called "Element", which is the type of element stored in the array. It can be useful to refer to this field when dealing with arbitrary arrays.

Types can depend on values

The type of one variable can depend on the value of another. For example, you can declare that one variable must always be less than another variable. The compiler can reason about numbers and insure that this constraint is held. This is especially useful for, e.g., requiring that an index into an array be less than the size of the array, allowing out-of-bounds errors to be detected at compile time.

Another use of dependent types is to choose the type of one variable conditionally based on the value of another. For example, you could have a variable "x" which might be a number or a string depending on some boolean variable "isString". This sort of construct is useful for, e.g., implementing type-safe unions.