Introduction

We distinguish 2 types of languages: typed (Java, C#, etc.) and untyped (Python, Scala, JavaScript). A type is a set of values, like:

• Int is the set of all integers.
• Float is the set of all floats.
• Bool is the set {true, false}.
• etc.

In typed languages:

• Every concrete value is an element of some type or types
• Every legal program has a type

These languages will throw out exceptions when an expected type differs from the found one:

This is the whole idea of type checking: making sure we avoid type errors.

Why do we care about this? If we have a weak typed language, where we don’t check the types, like C, catastrophic errors may happen:

This is known as the heart bleed bug, which allowed anyone on the Internet to read the memory of the systems protected by the vulnerable software. This comprised the secret keys used to identify the service providers and to encrypt the traffic, the names, and passwords of users and the actual content.

What is Type Checking?

There are multiple definitions of what Type Checking is:

• Benjamin Pierce, Types and Programming Languages (2001): A type system is a tractable syntactic method for proving the absence of certain program behaviours by classifying phrases according to the kinds of values they compute.
• Wikipedia: A data type (or simply type) is a collection or grouping of data values, usually specified by a set of possible values, a set of allowed operations on these values, and/or a representation of these values as machine types.