The Vega Programming Language

Since announcing projects before having anything to show for them is apparently en vogue now, I guess I’ll join in and announce that I’m building another programming language! Yeah yeah I know, working on two languages at the same time is a ton of effort, but this is my project so I’m the one who gets to decide what’s a bad idea :)

Unlike Polaris, which is relatively specialized to shell-like freestanding scripts, the goal for Vega is to be the ideal general purpose programming language I would want to use. As such, it’s going to be somewhat similar to Haskell, my favorite existing language, but with some significant differences. Some of the notable features I’m going for are - (hopefully lightweight) dependent types - good type inference - direct-style row-polymorphic algebraic effects - globally coherent type classes (like Haskell’s and Polaris’ but unlike Coq’s) - linearity - good C FFI - first class implicit existential types - anonymous row-polymorphic records and maybe polymorphic variants

A cool consequence of dependent types is that they give you ML-style modules pretty much for free since a module can just be represented as a record of values and types (like modules in Dhall or Lua) and a functor is just a function that transforms modules.

As for the runtime system, I’ll probably do something similar to OCaml 5 with segmented stacks for extremely efficient one-shot effects. Thanks to linearity, a handler could then specify whether it uses its continuation linearly or not and only take the slow route (that involves copying stack frames) in the non-linear case. Linearity also helps model resource acquisition without the need for stack unwinding or anything like that (since linear resources cannot be passed across calls to functions with non-linear effects)

But for now, I’ve only got a half-written dependent type checker with decent inference working.

It’s written in Haskell this time, which is quite nice after mostly working in OCaml for Polaris. OCaml is fun and all, but wow, there are a few things I’ve missed so much: - type classes - super simple metaprogramming through GHC.Generics - Trees that Grow that aren’t terrible - order independent declarations and easy mutual recursion - the ability to use data structures other than lists and mutable arrays without massively sacrificing ergonomics.

I would like to self-host Vega at some point, so it’s quite nice that these are all features I’ve got planned for it anyway. Especially Trees that Grow should be very natural with dependent types.