This is a series of notes taken from the Coursera course: “Programming Language”.

Types are essential components of a programming language. From practicality, types separates the definition of different categories of data within a language from its implementation. Natively computer only knows bits, how each language represents an integer with these bits are an implementation detail. (Most) language user would only need to know that an int type represents an integer.

Types give hint to the compiler what the programmer intends to do, to a certain extent. A float type variable refers to a floating point number, and may raise a warning if it is coerced into an int without explict directives due to loss of precisions. A function signature of int * float should reject arguments of type string * vector - as it’s likely a prgrammer error. There are other compilers/type checkers that takes on a different approach. Ruby/python/javascript would not check for these type errors before the program runs, but will raise a runtime exception when the program runs into these errors. The distinction sets the boundary for static typing and dynamic typing languages.

What does a type system promises for? They are said to be sound if for some condition X (undesired), the type system always rejects the program that does X. They are said to be complete, if the type system never rejects a program that never does X. We simply cannot have a type system that’s sound, complete and always terminates. This is the core essence of undecidibility.

Often times, programmers would like to reuse their code. A doubling function that works for int can also be reused for float. Instead of writing the same function or each type, languages provides generics so that programmers could reuse codes more easily. Several kinds of polymorphism rules are implemented for modern languages: parametric, subtyping and ad-hoc. Subtyping polymorphism dictates that if a function f works for type T, then it should also work for all subtype of T. Function subtyping is another interesting topic to cover.

Finally, there’s also OOPL type systems. Subtyping objects is similar to that of subtyping a record in functional terms, with some restrictions. Classes and types are fundamentally different concepts. However, there are good reasons for languages like Java and C# to purposely mix these concepts since whenever one introduces a new class, a new type for that class is also added.

I’m super excited to sum up my findings about types from the PL course journey. In the next blog post, let’s start with some basic stuff, type matching and type inferencing, two powerful features introduced in SML.

References: