[theory] What is a type?

[thedeemon]

On Monday, 15 January 2018 at 20:46:19 UTC, Ali wrote:

> If you want to learns the ins and outs of types, this books 
> comes highly recommended
>
> https://www.cis.upenn.edu/~bcpierce/tapl/

+1, TAPL is a must read for anyone in CS, I believe.
Also recommended: "Type Theory & Functional Programming" by Simon 
Thompson,
"Practical Foundations for Programming Languages" by Robert Harper
and his and his colleagues lectures here:
https://www.cs.uoregon.edu/research/summerschool/archives.html

Many programmers remain unaware that there is a discipline called 
Type Theory, as part of math in general, it predates all 
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.