Roundcrisis

About Contact me Presentations rss feed  rss

What is a type system

31 Dec 2014

Curiosity killed the cat, good thing cats have 9 lives…

I don’t know you, but after using a few programming languages I have too many questions about type systems, some that come to mind:

Probably some of those questions make no sense, at least, until I understand the answers.

Thankfully, I was not alone in asking myself questions. For example this question seems to spiral into no concrete answers.

If you are looking for a post about Strong vs Weak typing and Static vs dynamic typing articles I found a this one (there are many more)

Anyway I am starting off with the first question.

What is a type system?

According to

Ok, a bit generic, but helpful:

Other definitions I found online are as simple as:

This is a more helpful

As I was thinking a little about this I found this gem of a post:

@mrb_bk wondered What is a type system for This is totally worth the read. The post is based on studying TAPL. The TL;DR of the post goes like:

"The most basic property of this type system or any other is safety (also
called soundness): well-typed terms do not 'go wrong.'"

What does “go wrong” means in this context?

"...it means reaching a 'stuck state' that is not designated as a 
final value but where the evaluation rules do not tell us what to do next."

In this context thinking of getting stuck as runtime errors is acceptable.

"What we want to know, then, is that well-typed terms do not get stuck. We 
show this in two steps, commonly known as the progress and preservation 
theorems."

The theorem definition and explanation is in the post, but I had to stop and thing about:

"Safety = Progress + Preservation"

That is where I am going to leave this for today.

Worth Reading

As a novice in this area I found The paper by [Luca Cardelli][1] is a good read .

Also this pdf by Benjamin C. Pierce contains an overview of the available literature up until year 2003.

References

Feedback other resources?

Do you know of other type system resources I should look into? Do you know of any other links I should look into? Any comments? Let me know

Happy new year!!

Categories:   programming   development

Want to discuss this post? the best place right now for me is mastodon, please message me @roundcrisis@types.pl with your comment or question.