First Research Log

My current research goal is to show that gradual typing can be implemented with good runtime and space performance. In particular statically typed programs in a gradual language should have very little overhead over the same program in a statically typed with a similar feature set. Conversely, dynamically typed programs should have performance on par with dynamically typed programs. To prove this hypothesis, I am building a prototype ahead of time compiler for a statically typed programming language.

Current Work

My work this week has been focused on coming up with an idea of how recursive types could be implemented with coercions. From a language design standpoint I have chosen the recursive type to be equi-recursive. This means that a μ node and it’s unfolding are definitionally equal (anywhere one is valid so is the other). I think in the future we will want to compile this to a iso-recursive intermediate language, because by doing so we may be able to apply recursive coercions lazily.

So far I have an interpreter that works for the benchmark that I would like to compile. This includes the rules necessary for converting type based casts into coercions, applying coercions, and composing coercions to make them space efficient. More on that later. Formalization and proofs will come soon.

I also recently started porting our compiler to have an LLVM backend by using the Sham library a friend of mine is writing. This should eventually support tail-call optimization which means we can show how to introduce low-overhead space-efficient tail-call casts. More on this later.