On Monday, 15 January 2018 at 19:25:16 UTC, H. S. Teoh wrote:
> At the most abstract level, a type is just a set. The members of the set represent what values that type can have.

Hm, yes, like representing an ordered pair (a,b) as {{a},{a,b}}.

But I think typing is more commonly viewed as a filter. So if you represent all values as sets, then the type would be a filter preventing certain combinations.

It is a matter of perspective, constructive or not constructive. Kinda like synthesis, additive (combine sines) or subtractive (filter noise).

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.

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