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.

Many programming languages require that statements end with a semicolon. Some languages, such as Javascript, Go, Kotlin, Swift, Scala and Lua, make this requirement optional. Although a semicolon may be specified, it is not required to terminate a statement. This post explores the underlying rules various languages use to make semicolon inference possible. It also articulates the arguments for and against a language offering support for it.1 The Challenge The semicolon inference rules would be simple if every statement fit on a single line.

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.

Type theory has many kinds of typing mechanisms: product, sum, top, bottom, recursive, universal, existential, subtypes, linear, refinement, dependent, and so on. I have run across something different from all those, which I am calling “infectious typing”. If anyone knows a formal name and/or treatment for this mechanism, I would love to hear about it. Type composition allows us to create new types out of existing ones. A struct or class product types is composed of several fields, each with its own type.

In 2001, Trevor Jim (AT&T Research) and Greg Morrisett (Cornell) launched a joint project to develop a safe dialect of the C programming language, an outgrowth of earlier work on Typed Assembly Language. After five years of hard work and some published papers, the team (including Dan Grossman, Michael Hicks, Nik Swamy, and others) released Cyclone 1.0. And then the developers moved on to other things. Few have heard of Cyclone and almost no one has used it.

The prior post, When Sum Types Inherit, shows that we can (and should) use the magic of inheritance to enrich sum types to offer as powerful a capability as traditional classes. Graph-based, variant node data structures benefit from variant nodes being able to support common fields, methods, and virtual dispatch. That result, however, raises a new question: do we really need two separate language abstractions that offer very similar capabilities?