The article's exploration of the meaning of "type" within the context of programming reminds me of my particular take, which is that a type is no more than an invariant bag of predicates that must be true about a particular entity in the program.
Because programs are generally intended to be run on actual hardware, many programming languages use types to mirror what the hardware will actually execute efficiently, for example integers of certain fixed bit widths (8/16/32/64/etc.). These are so standardized that everyone knows what they will do, and they generally have the convenient property that standard mathematical operations will resolve to the same or another convenient type. There are exceptions of course. For integer division, there is a problem when the divisor is zero. Unlike floats where Inf/-Inf/Nan satisfy the type, there is no room in standard integer types to store Inf/-Inf/NaN or undefined. Consequently, either some integer must be furnished as the result, or that section of code simply cannot proceed (either handled by termination or exception).
There's no inherent reason why a programming language can't have a wildly richer set of built-in or user-defined types. For example, the type of prime numbers, or the type of single digit integers: >= 0 and < 10, or the type of code blocks that are guaranteed to terminate. Or the increasingly prevalent not-null pointer types, or types (e.g., "Option") that might or might not have the desired target type. The actual restrictions are practical: (1) how is the data actually represented and carried around in the physical computer, and (2) how is the type (the invariant bag of predicates) proven to be satisfied, so it can be relied on by the programmer and operated on by the compiler.
Historically the critical bifurcation between "value" and "type" came down to this: Value is what can be reliably computed when a program is run. Type is what can be reliably computed when a program is compiled.
I take issue with this compile-time / runtime formulation. Computer programs are useful because they take unpredictable inputs at runtime. A program that takes no runtime inputs or only fixed ones always produces the same result, and hence, no matter how complicated, can be rendered to fixed outputs at compile-time. With dynamic runtime inputs, types enable the programmer to constrain the set of possible states the program can be in and better manage complexity. Types can be proven at compile-time, yes, but they can also be proven at runtime. A maybe-null pointer satisfies a non-null pointer type once it has been checked for nullness.
The fundamental tension is that a type that is too broad is often too unconstrained to work with, and a type that is too narrow is too hard to prove satisfied for any possible runtime input.
a type is no more than an invariant bag of predicates
I have a type system implemented in Janet along these lines (which also has a declarative testing, documentation etc. framework attached). Implementing prime? and then using it everywhere is easy and good!
The article's exploration of the meaning of "type" within the context of programming reminds me of my particular take, which is that a type is no more than an invariant bag of predicates that must be true about a particular entity in the program.
Because programs are generally intended to be run on actual hardware, many programming languages use types to mirror what the hardware will actually execute efficiently, for example integers of certain fixed bit widths (8/16/32/64/etc.). These are so standardized that everyone knows what they will do, and they generally have the convenient property that standard mathematical operations will resolve to the same or another convenient type. There are exceptions of course. For integer division, there is a problem when the divisor is zero. Unlike floats where Inf/-Inf/Nan satisfy the type, there is no room in standard integer types to store Inf/-Inf/NaN or undefined. Consequently, either some integer must be furnished as the result, or that section of code simply cannot proceed (either handled by termination or exception).
There's no inherent reason why a programming language can't have a wildly richer set of built-in or user-defined types. For example, the type of prime numbers, or the type of single digit integers: >= 0 and < 10, or the type of code blocks that are guaranteed to terminate. Or the increasingly prevalent not-null pointer types, or types (e.g., "Option") that might or might not have the desired target type. The actual restrictions are practical: (1) how is the data actually represented and carried around in the physical computer, and (2) how is the type (the invariant bag of predicates) proven to be satisfied, so it can be relied on by the programmer and operated on by the compiler.
I take issue with this compile-time / runtime formulation. Computer programs are useful because they take unpredictable inputs at runtime. A program that takes no runtime inputs or only fixed ones always produces the same result, and hence, no matter how complicated, can be rendered to fixed outputs at compile-time. With dynamic runtime inputs, types enable the programmer to constrain the set of possible states the program can be in and better manage complexity. Types can be proven at compile-time, yes, but they can also be proven at runtime. A maybe-null pointer satisfies a non-null pointer type once it has been checked for nullness.
The fundamental tension is that a type that is too broad is often too unconstrained to work with, and a type that is too narrow is too hard to prove satisfied for any possible runtime input.
I have a type system implemented in Janet along these lines (which also has a declarative testing, documentation etc. framework attached). Implementing
prime?and then using it everywhere is easy and good!