Well-Typed Substructural Languages
In this post I'll explain how to build well-typed by construction implementations of substructural languages, that is, languages in which our ability to delete, copy and/or swap variables in scope is restricted. I will begin by recounting the folklore that I learned from Conor Mc Bride and Zanzi, and then I will explain a useful trick that I invented: terms that are parametrised by an action of a category of context morphisms.
Personally, my main interest in this topic comes from my plans to implement a bidirectional programming language in which all programs are optics, so they can be run in both a forwards mode and a backwards mode. Due to the subtle categorical structure of optics, such a programming language is substructural in a very unique and complicated way. I have found in practice that actions of context morphisms help a lot to make this problem tractable. I'll be continuing to document my development of this language on the CyberCat Institute blog.
We begin with a tiny language for types, with monoidal products (a neutral name because later we will be making it behave like different kinds of product), a unit type to be the neutral element of the monoidal product, and a "ground" type that is intended to contain some nontrivial values.
