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
represents an integer.
Types give hint to the compiler what the programmer intends to do, to a certain extent. A
type variable refers to a floating point number, and may raise a warning if it is coerced into
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
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
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
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