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.
A short guide to Redex concepts, conventions, and common mistakes.