Simply Typed Lambda Calculus (STLC) is a foundational model in programming language theory, known for its simplicity and strong typing discipline. However, its rigid typing rules can restrict practical software development. To address this limitation, we introduce subtyping into STLC, allowing for more flexible type assignments following Liskov’s Substitution Principle. We implemented an algorithmically driven type system supporting subtyping, and then expanded it with joins and meets, based on Types and Programming Languages by Pierce [13]. Our implementation addresses the complexity introduced by subtyping in both theoretical and practical aspects, particularly highlighting challenges in algorithmic type checking. This paper discusses our implementation details, encountered challenges, and the historical and practical significance of subtyping.
Simply Typed Lambda Calculus (STLC) offers a ro- bust theoretical framework for reasoning about functional languages. Despite its elegance, STLC is limited by its strict type matching requirement: it is required that every function argument exactly matches the declared parameter type. For example, a function that takes as input a record with less fields (e.g. { x : Bool }) cannot directly accept records with additional fields (e.g. { x : Bool , y : Bool }) even if intuitively, it is perfectly safe to do so. Subtyping addresses this rigidity. It is the formalization of the idea that something more specific is suitable where something more general is needed.
The idea behind subtyping traces its roots back to the early history of programming languages. In the late 1960s, the development of Simula 67 [1], often regarded as the first object-oriented language, introduced the idea of class-based inheritance. Although Simula 67 did not formally distinguish subtyping from inheritance, it laid out an important concept: subclass instances could be used wherever superclass instances were expected. The formal notion of subtyping emerged explicitly in the 1980s. Barbara Liskov and Jeannette Wing, in their work on data abstraction and safe substitution [2], [3], articulated what is now called the Liskov Substitution Principle or Safe Substitution Principle: a guideline for when it is safe to substitute instances of one type for another. This was formally stated in their 1994 paper as follows:
”Subtype Requirement:
Let ϕ(x) be a property provable about objects x of type T. Then ϕ(y) should be true for objects y of type S where S is a subtype of T [3].”
At around the same time, researchers such as Luca Cardelli and Peter Wegner initiated the study of type systems with explicit subtyping relations [4]. Cardelli’s 1984 development of the Amber language marked an important milestone, systematically introducing subtype polymorphism into type theory [5].
During the 1980s and 1990s, as object-oriented programming gained widespread popularity, subtyping became less of an academic notion and more of a fundamental language feature. Languages like C++ [6], Eiffel [9] and later Java [7] integrated subtyping through class hierarchies and interfaces. In Java, for instance, a class B that extends a class A is treated as a subtype, enabling instances of B to be used wherever instances of A are expected [7]. Eiffel in particular emphasizes adherence to Liskov’s principle by integrating subtyping with a strong contract-based system [8], [12].
Beyond nominal inheritance, languages like OCaml and TypeScript explore structural subtyping: where a value’s type is determined by its structure rather than its nominal declaration, bringing even greater flexibility and enabling polymorphism based purely on shape [10], [11]. Today, subtyping remains a cornerstone of programming-language design in most mainstream languages.
This paper outlines our implementation strategy, describing the algorithmic approach to subtyping and detailing the implementation of key concepts, including function types, product types, record types, conditionals, and type operations such as joins and meets. Our algorithmic approach is adapted from its presentation in Types and Programming Languages by Pierce [13].