By Scott J Maddox.
First published 2021-10-06.
My apologies for the lack of any updates since the last (and only) Introducing Dawn (Part 1) post back in April. While many of the higher level design goals and plans for Dawn are fairly clear in my mind and notes, the lower level details are still changing rapidly. As a result, it’s quite difficult to continue introducing Dawn to a general audience at the current time. So, I’ve opted to hold off on completing and publishing the rest of the “Introducing Dawn” series until the relevant parts of the language are prototyped and somewhat stable. Nonetheless, I thought it would be good to provide some updates on progress and setbacks, and to talk a bit about what I’m planning next.
Since the last post, I’ve abandoned the publicly released Dawn Phase 1 Haskell prototype in favor of a (so far unreleased) Rust prototype. Despite being particularly well suited to rapid prototyping of programming languages, Haskell had become too painful to work with due to its painfully long compile times, complicated Monad-based IO and error handling systems, and confusing debugging tools. To be fair, these issues are all undoubtedly induced or exacerbated by my own relative inexperience with the language. Nonetheless, I decided to start fresh with a Rust prototype, Rust being a language that I have much more experience with and which is also well suited to rapid prototyping of programming languages thanks to the availability of algebraic data types and pattern matching.
While the Rust prototype is roughly as far along as the Haskell prototype was, it has more recently become clear that the prototype type system is unsound due to improper handling of higher-kinded function type covariance and contravariance. Unfortunately, addressing this soundness issue without compromising either type inference or expressiveness turns out to be fairly complicated, due to the need for higher-kinded and impredicative polymorphism. Luckily, the necessary type theory appears to have already been developed, and it should be reasonably straightforward to adapt it to a concatenative language. It is considerably more complicated than the Hindely-Milner-based type system I was using before, though, so it will take some time to fully grok and implement.
Since it’s absolutely critical for my higher level goals that Dawn have a solid and sound theoretical foundation, I’ve decided to take a step back and formalize the core of the language in a series of incremental steps, and to implement a small toy prototype language for each step, beginning with the untyped concatenative calculus. The formalization and implementation of this first step is essentially complete, and an associated blog post is coming soon!