Where Do Type Systems Come From?

#1

Post by philix001 » Fri, Jul 07, 2017, 9:44 PM UTC

Where Do Type Systems Come From?
blog.felipe.rs

Re: Where Do Type Systems Come From?

#2

Post by smcl » Fri, Jul 07, 2017, 10:14 PM UTC

I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. I get that these underpin the technology we as programmers use every single day, but I'm a little ashamed that I can't get excited about the subject and feel like it's too late for me to bother trying.

Re: Where Do Type Systems Come From?

#3

Post by agumonkey » Fri, Jul 07, 2017, 10:19 PM UTC

smcl wrote: post #2

I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. I get that these underpin the technology we as programmers use every single day, but I'm a little ashamed that I can't get excited about the subject and feel like it's too late for me to bother trying.

To each his own path. Maybe you'll change course, maybe not, maybe type theory will evolve (HoTT comes to mind).

Re: Where Do Type Systems Come From?

#4

Post by pier25 » Fri, Jul 07, 2017, 10:20 PM UTC

Reminded me of Gödel's incompleteness theorems.

First incompleteness theorem

Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F.

Second incompleteness theorem

For any consistent system F within which a certain amount of elementary arithmetic can be carried out, the consistency of F cannot be proved in F itself.

Re: Where Do Type Systems Come From?

#5

Post by agumonkey » Fri, Jul 07, 2017, 10:20 PM UTC

Types are close to adjoint functors / adjunctions and partial evaluation. Assigning restricted information to part of a structure to gain knowledge through limitation (math).

Re: Where Do Type Systems Come From?

#6

Post by Kenji » Fri, Jul 07, 2017, 10:24 PM UTC

smcl wrote: post #2

I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. I get that these underpin the technology we as programmers use every single day, but I'm a little ashamed that I can't get excited about the subject and feel like it's too late for me to bother trying.

It's never too late to bother trying. If you think it'll benefit you in life, just go for it and study it.

Re: Where Do Type Systems Come From?

#7

Post by philix001 » Fri, Jul 07, 2017, 10:25 PM UTC

smcl wrote: post #2

I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. I get that these underpin the technology we as programmers use every single day, but I'm a little ashamed that I can't get excited about the subject and feel like it's too late for me to bother trying.

I don't think it's common for programmers to have in depth opinions about type systems. And most of the ones who do may not really know what they're talking about.

Re: Where Do Type Systems Come From?

#8

Post by ridiculous_fish » Fri, Jul 07, 2017, 10:37 PM UTC

smcl wrote: post #2

I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. I get that these underpin the technology we as programmers use every single day, but I'm a little ashamed that I can't get excited about the subject and feel like it's too late for me to bother trying.

> I get that these underpin the technology we as programmers use every single day

Is this actually true? Of course Haskell, Idris, etc. leverage type theory, but how much type theory underlies the type systems of widespread practical languages like C# or Java? Can something like C++'s SFINAE be grounded in type theory, or is it just a hack?

Re: Where Do Type Systems Come From?

#9

Post by simplify » Fri, Jul 07, 2017, 10:37 PM UTC

If you haven't thought much about type systems but want to understand what the big deal is, I wrote a post specifically for you [1]. It draws motivation for wanting a good static type system from first principles.

[1] https://gilbert.ghost.io/type-systems-for-beginners-an-intro...

Re: Where Do Type Systems Come From?

#10

Post by AnimalMuppet » Fri, Jul 07, 2017, 10:39 PM UTC

Kenji wrote: post #6

smcl wrote: post #2

I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. I get that these underpin the technology we as programmers use every single day, but I'm a little ashamed that I can't get excited about the subject and feel like it's too late for me to bother trying.

It's never too late to bother trying. If you think it'll benefit you in life, just go for it and study it.

If. I suspect that smcl can't get excited about type systems because of not seeing the benefit.

For me, types are sets of possible values, plus sets of valid operations on those values. I don't much care where they come from. As far as I am concerned, they are an engineering construct to make programming easier and safer, and are interesting only to the degree that they accomplish those goals. Any connection to pure math is completely incidental; if there were no such connection, it would not make (programming) types any less useful.

Now, math often gives deeper insight into what's going on, and enables you to create more powerful (useful) abstractions. But if the useful abstractions don't correspond perfectly to types as used by mathematics, I don't care.