Have our conversations about programming paradigms grown stale? It seems so. Paradigms like object-oriented programming and functional programming, the two most talked-about, are decades-old. Nearly always, conversations about them devolve into reciting the same desiccated stereotypes. Is this because the notion of a programming paradigm has outlived its usefulness? Dr. Harper appears to think so. Even among those who find some value in one paradigm or another, there is a notable wariness to engage in fruitful discussions across diverse communities.
The previous Lifecycle of a Reference post illuminates the working relationship between references and regions. It explains how a reference’s region annotations are programmer-definable struct-like types, which can specify an allocated object’s region state using fields, and region-based operations on an object (e.g., allocate and free) using methods. This, however, leaves out an important part of the story about region definitions: their global state and global runtime logic. Holistically, a Cone region is fully defined by an importable module, within which lies:
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.