Lambda the Ultimate

Types are mostly used in three ways:

• To validate some properties of a program, e.g. memory safety for indexing arrays, or that every operation is well defined.
• To document a program, e.g. an API is often conveniently represented with a combination of types and natural language docs.
• Meta-programming, e.g. automatic selection of a function's implementation based on matching type of input or output, typeclasses and multi-methods.

The last option doesn't need types, but is conflated with types by many PLs. Where it's separated from types, then you might understand types as simply a form of machine-verifiable documentation, more abstract than tests.

A common feature of *most* type-systems is that types are compositional. That is, if you can determine the types of the subprograms, then you can easily compute the type of a larger program that integrates them. This is a very useful feature for modular software, but it also constrains which properties a type can effectively express, and thus which properties the type system can verify. There are some exceptions to the rule, where types aren't compositional, thus whitebox full-program analysis is required to type check.

In any case, a primary utility of static types is that they express an automatic proof over a program. It doesn't much matter what the proof is about, so long as it's not trivial (where a "trivial" property is is defined as a property that is invariant for syntactically valid programs). Automating *any* non-trivial proofs over a program can help programmers discover and eliminate many errors that are unrelated or very indirectly related to whatever we are proving.

Individual types cannot be usefully separated from the type system, the system of automated proofs.

When comparing types vs constraints, I can see both could be used to solve all those bullets. So I feel I've come back to my starting confusion. Still confused but on a higher level.

One way of using types could be to express fundamentally different things, i.e. distinguish things like strings, numbers, and, well, what more?

Then you could have unit to express things like this string is a path, which is not the same thing as arbitrary text. Or this number is velocity expressed in m/s, while another number might be weight expressed in pounds and so on.

Above all you could add constraints, where you could restrict things to be valid for certain states and other more complex relations.

The idea here would then be that types express things that are fundamentally incompatible, and the only way to get on from another is explicit conversions.

Unit would be a more complex variant of the same thing, where you could actually divide a distance in meter with time in seconds, and get velocity in m/s.

Lastly, the constraints would be simply a list of requirements that need to be fulfilled for the expression to be applicable. If not fulfilled, the expression will simply not be applied and another will be used if available.

Most of this feels familiar from other languages, except for unit handling. Is there any language that has implemented this as part of the language?

The ability to express that two numbers are incompatible in some way is very useful, e.g. to avoid mixing up distance with velocity, or to avoid confusing altitude with flight distance. This is certainly a useful application of types.

However, that is not what types are about. It's just an effective pattern for using types, which solves some problems. Much like OOP is not about any specific OO design pattern.

The difference between type systems and constraint systems is largely in who solves them (man vs machine) and consequently how much detail is required (constraint systems need to fully describe requirements and heuristic preferences so a machine can write the details; types only need enough detail to resist accidents between intention and implementation, because a sapient entity also writes and debugs most of the program).

Types could lay the foundation, and constraints would then add details whenever needed. The question is then what to call the constrained type?

If you constrain the API for an anstract type, we call that an interface (or signature).

If you constrain the values of a concrete type, we call that a refinement type.

If you constrain how a value of an abstract type is replicated, moved, or removed, we call that a substructural type.

What kind of constraint are you envisioning?