In Racket, programmers can create powerful abstractions by bundling together a family of values, functions, and syntax extensions in the form of a new language. These languages, however, are typically untyped. Turnstile is a new Racket {library,language} for creating typed languages by integrating type checking with Racket’s existing tools for describing languages. The technique is described by fellow PRL’ers in the paper Type Systems as Macros.
Racket encourages language developers to take full advantage of linguistic reuse by defining new language forms in terms of existing constructs. Unsurprisingly, language extensions often retain some of the Racket-y flavor from the underlying constructs. Implementors save time and energy while users of the language benefit from the familiarity they already have with the Racket ecosystem.
Unfortunately, Turnstile does not lend itself to expressing one of Racket’s most ubiquitous idioms: naming local bindings with define. Early experience reports from Turnstile, including my own, suggest that language implementors very much desire to include define-like binding forms in their languages.
This blog post provides a brief overview of what Turnstile is and how it works, an introduction to defining typed language forms, and how to equip these languages with a define binding form.
The literature on mixed-typed languages presents (at least) three fundamentally different ways of thinking about the integrity of programs that combine statically typed and dynamically typed code. Recently, we have been sorting them out.
This post explains the sampling method introduced in the paper On the Cost of Type-Tag Soundness
The Racket School 2018: Create your own language • 9–13 July • Salt Lake City
A few weeks back, we published a draft of an article entitled Monotonicity Types. In it, we describe a type system which we hope can aid the design of distributed systems by tracking monotonicity with types.
Recently, “final encodings” and “finally tagless style” have become popular techniques for defining embedded languages in functional languages. In a recent discussion in the Northeastern PRL lab, Michael Ballantyne, Ryan Culpepper and I asked “in what category are these actually final objects”? As it turns out our very own Mitch Wand wrote one of the first papers to make exactly this idea precise, so I read it available here and was pleasantly surprised to see that the definition of a final algebra there is essentially equivalent to the definition of observational equivalence.
In this post, I’ll go over some of the results of that paper and explain the connection to observational equivalence. In the process we’ll learn a bit about categorical logic, and I’ll reformulate some of the category theory in that paper to be a bit more modern in presentation, cleaning some things up in the process.