What is a type?

I have a hard time grasping what a type really is. To demonstrate my problem, let's assume we do everything with constraints instead.

So to show if an identifier or constant can be used in a given context, just compare the constraints. Do they allow the usage? Then fine, otherwise, error.

Does this mean that the sum of constraints is the type?

How then, would you explain fundamental types, like numbers and strings? It needs to be either, not both. A function accepting both, probably has two distinct implementations, or is converting one of them to the other. For example, printing might convert the number into a string. Constraint doesn't really handle conversions (or do they?), so apparently having numbers and strings seem to me to be something else. Is this what is meant by a type? Having a "something", which then could be converted into another "something"? And constraints should be added ontop of this?

Or is the type really all of the above?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Intrinsic and extrinsic

I'll repeat this here, since it seems quite relevant.

"The Meaning of Types — From Intrinsic to Extrinsic Semantics". John C. Reynolds, BRICS Technical Report RS-00-32, December 2000.

Wrong question, a type could be anything

Roughly, a type is a syntactic construct used to express a property of interest. That already could be anything, static guarantees, resource usage, or whether the program does your laundry.

The question is what you want it to be.

So a type can be anything

So a type can be anything really, then the question should probably be what a type can be used for. Is it to make sure data isn't mixed in a way that would producer noon-obvious results?

re what a type can be used for

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

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?

Types as incompatibility?

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

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

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?