Over two and half years ago, I described something I called Gradual Memory Management. Inspired by Rust and Pony, my paper proposed that it is feasible and desirable for a systems programming language to allow programs to exploit multiple memory management and permission strategies. Without putting memory and data race safety at risk, doing so would facilitate significant improvements to throughput and latency, even in multi-threaded architectures. It is easy to propose wild ideas in words.
It is notable how often paradoxes arose in the historical journey that led to the Rise of Type Theory. Resolving Russell’s paradox led to his theory of types. Gödel’s Incompleteness theorems rested its proof around a variation of the Liar Paradox. Church and Turing recapitulated this result using their distinctive formalisms. Intuitionistic type theory was deliberately designed to avoid these paradoxes. And so it goes. As an undergraduate, I had the pleasure of studying Gödel’s ingenious proof as part of a course on Predicate Logic.
After three dreary posts on syntax, let’s change the pace and pursue an entirely different, deeper and more fun topic! In our community’s #theory channel on Discord, someone asked: “Is there a basis for some of the mathematics related to type theory and its relationship to its usage in programming languages?” This triggered a spirited dialogue about the historical antecedents of type theory, how type theory evolved from that, and the interplay between programming languages and type theory.
I seem to be on a roll with syntactic concerns lately, which is not where I typically spend most of my time. Today’s issue is, at least, more unusual than stylistic preferences regarding semicolons and significant indentation. This post explores the issues that arise when teaching the compiler to be agnostic as to whether it is parsing a value expression or a type expression. A value expression computes some typed value when evaluated:
The last post focused narrowly on evaluating various techniques for semi-colon inference, thereby enabling a program to successfully compile even when the programmer omits statement-ending semicolons. This post broadens this theme, looding at how the compiler can take advantage of significant indentation when handling block inference and multi-line string literals. I wander into this topic knowing that for many programmers, compiler support for significant indentation is troubling and uncomfortable. They prefer the explicit clarity of required semi-colons to end statements and curly braces to delimit blocks.
The last two posts introduced the fundamental elements underlying Cone’s type system. They also distinguished between nominal vs. structural type equivalence. However, they were largely silent about subtyping relationships between types. Given how important subtyping is to Cone’s type versatility, I thought it might also be valuable to offer a detailed treatment of these mechanisms. My approach will be practical, rather than formal (alas! no subsumptions nor lattices), distilling lessons learned from implementing a rich, but type-safe collection of subtyping mechanisms.
The prior post described the semantics underlying Cone’s fundamental types, for all types except the all-important pointer and reference types. The presence of versatile pointers/references as an explicit and distinctly-separate kind of type is a distinguishing characteristic of systems programming languages. I choose to cover them here as a separate post, since the safety guarantees of Cone’s references make them semantically rich and complex. In harmony with the subatomic theme of the prior post, reference types are themselves composed of “quarks”: pointers, regions, permissions, and lifetimes.
When I began work on the Cone programming language, I believed I had a confident handle on which primitive types this modern, safe systems language required: various sizes of atomic number types, fixed-size arrays, programmer-defined structs, raw pointers, safe references, discriminated (and raw) unions, generics, and limited support for void and tuples. My confidence was misplaced. Once or twice a year, implementation challenges and further research forced me to re-think aspects of the type system, each time deepening my understanding of what it required.
When the clock ticks over to a new decade, it is customary to look back, to reflect on how much we have accomplished, and then look forward, to sort out where we want to go. Ten years is long enough that substantive progress should be visible in the glacially-slow evolutionary pace of programming languages. One can see this by noticing how many now-influential languages had no notable marketplace presence only ten years ago: Rust, Go, Swift, Kotlin, Dart, and Julia.