Hacker News Reader

> Types are just a layer on top of your code that help enforce certain logical / mathematical properties of your code; those that your particular type system enables you to constrain.

I don't know if I really agree with that. It seems to presume the default form of data is a map<any,any> and you constrain that down to a specific set of fields. (Or similar logic over void pointer spaghetti.) If you build up a record type from scratch you're doing something quite different. Adding a field where there used to be nothing, no way to store data there in an instance, is not what I would call a constraint.

No, you're really adding a constraint. You're adding a description of what exactly a piece of data represents, allowing the compiler or interpreter to limit the ways in which you can use it.

The form of data in a computer is simply a sequence of binary information. It is up to you as a programmer to decide what it represents.

In some cases, you can use a type system to have that automatically enforced in part.

It's important to realize that the types you can use in practice as part of a formal type system are very rarely correct in the sense of fully describing what some data represents.

For example, if a string of bytes represents a HTTP request, then "valid HTTP request bytes" is the correct type, but the type known to the compiler might just be string of bytes.

Similarly, if you represent a graph by a hash table of int to list of int (with the ints labeling nodes), then the type of that is a map from int to list of int, where the int values in the latter must exist as keys as well - but the type system might not actually know that.

In practice, there will therefore often be functions that validate the contents of the data - these are basically manual run time type checking functions.

> You're adding a description of what exactly a piece of data represents, allowing the compiler or interpreter to limit the ways in which you can use it.

Let's say I'm making a new record type with a .firstname field.

And let's say I'm not declaring what data type is stored in the field. Zero description or constraint is happening there.

The .firstname field itself was unrepresentable before I added it. There is no previously existing concept of accessing a .firstname field that I am constraining.

In this scenario, my language doesn't have access to raw memory, and even once I create this record type I don't know how it's going to be stored in memory. So I'm not constraining raw pointers into organized records because there are no pointers at all. I don't have raw byte access like in your HTTP example.

In that scenario, what am I constraining? What is the unconstrained version?

This hits really close to home!

I like thinking of types as a syntactical layer, just like in natural language. Without knowing the meaning of words, we can show that certain compositions of verbs, nouns, etc. can a priori never lead to an intelligible sentence. So trying to actually turn the sentence into a meaning or reading it (compiling/running) is useless.

But then again I was trained as a linguist so…

Types are sets e.g. the Integer type is the set of all the integer values.