A tale on Types
My fondness for programming can be boiled down to numerous reasons, be it it's logical or problem solving nature, or the visualization of mathematical objects or simply that we can create games with it. These reasons are often given by the vast majority of programmers out there (except those who code for money, but I don't consider them programmers), me included. Recently, however, I discovered a bridge between computer science and mathematics which was a common ground to deepen my knowledge about both of these fields. Types or the Type System is the core component of this bridge.
My first encounter with the type system was while writing C, but it went unnoticed for a long time. It was only when I switched to Python and then to Typescript that I really understood what I was missing. To be honest, initially, types seemed like a hindrance (especially coming from Javascript) which forced me to reason about the nature of my code and it's behavior before running it, something I wasn't used to. It felt like a burden, an overhead that can be easily dealt with by simply running the program and observing it's output. The turning point, however, wasn't necessity (where I was forced to used types due to some reason), but my desire to learn the best practices while writing complex code. Before long, I was hooked. I have fun writing interfaces and structs (not class ... (BaseModel) though, yet) with their associated variables and functions. It felt like I was designing code, rather then simply writing it. This feeling was artistic, rather then mechanical. Thus I stumbled into a whole new paradigm of programming.
The type system, or types in general, couldn't be much simpler to understand: they simply represent data, and all we have to do is express in our code that we know what the nature of a specific data point (variable) is, at any given part of our program. This forces us to reason about our program in advance, and write much more complex code more robustly. Types have lots of advantages, but they are just a part of what makes them appealing. My interest in type system didn't peak when I was learning the advantages, it peaked when I was learning the extend of type systems. (It's internals and implementation are also close contenders). Since I have only recently discovered my passion for types, and lack the necessary knowledge and experience to make meaningful comments on this topic, I would rather like to list various features or topics that I find fascinating about a type/type system here.
The blueprint nature. Types essentially are blueprints to the entirety of our code, and much can be said about our codebase by just looking at the types file (be it types.ts, models.py or header files).
Types essentially allow generalization of concepts in ways that closely resemble the generalization of mathematical objects. One easy-to-see example is generics, but that is just the tip of the iceberg.
The Dependent Type Theory (DTT) framework. The main component of this "bridge", which is theorem-provers or proof assistants. These essentially help mathematicians verify their proofs, while assist them by filling in some gaps.
I have recently started going deeper into DTT, and it is as complex as it is fascinating. When I first read the definition of what it means, it seemed as simple as "a type that depends on it's values", but upon looking at an example, I realised why DTT isn't implemented in general-purpose programming languages, even those with an expressive type system: it is highly non-trivial. For reference, here's a snippet. This code defines a tuple, whose second value depends on it's first.
universe u v def f (α : Type u) (β : α → Type v) (a : α) (b : β a) (a : α) × β a := ⟨a, b⟩ def h1 (x : Nat) : Nat := (f Type (fun α => α) Nat x).2 #eval h1 5 -- 5
From someone coming from using only mainstream programming languages, this was initially hard to reason about (due to it's functional nature as well, similar to Haskell). This, however, allows the language to express and work with abstract mathematical concepts, and reason about them (use them in proofs). This above consequence, that a type system can express a mathematical object, comes from the Curry-Howard Isomorphism, which states that any mathematical proof can be expressed in a computable program, also called propositions-as-types (second chapter in this excellent book).
This correspondence is an excellent way for one to dabble with both programming (through languages like Idris, Agda, Coq or Lean4) and mathematics, by expressing proofs in them. One could argue that this represents less of mathematics and more of computer science, but I personally think this could be a modern approach to practicing mathematical proofs and building upon them, instead of the traditional method of writing them down on boards and papers.