[theory] What is a type?

[Ola Fosheim Grøstad]

On Tuesday, 16 January 2018 at 06:26:34 UTC, thedeemon wrote:
> "Practical Foundations for Programming Languages" by Robert 
> Harper

Well, I have that one, and the title is rather misleading. Not at 
all practical.

> electronic computers and it's still very relevant today. Anyone 
> dabbling into compilers and programming language theory should 
> learn the basics of type theory, proof theory and some category 
> theory, these three are very much connected and talk about 
> basically the same constructions from different angles (see 
> Curry-Howard correspondence and "computational 
> trinitarianism"). It's ridiculous how many programmers only 
> learn about types from books on C++ or MSDN, get very vague 
> ideas about them and never learn any actual PLT. Of course type 
> is not a set of values, or any other set, not at all.

I don't really agree with this, empirically speaking. As many 
people have designed good languages without such a focus, and 
many have designed not very good languages with this focus...

Anyway, let's not make this too complicated, no need for a pile 
of tomes:

https://en.wikipedia.org/wiki/Type_theory