Low-level Semantics

WTy2 is a programming language (read: language for writing programs). Programs are usually written with the intention of executing them on a computer, and so some thought should probably be put into how that might be achieved.

Original goals for WTy2 included having it be a suitable language for systems programming, with predictable compilation and blazing-fast performance. These are noble goals, but the reality of making a programming language is that there is only so much time and so I must admit: while I think (hope) that I have come up with novel and interesting ideas in the realm of abstraction, I have not been able to crack how to place those in a systems-programming-appropriate type system, and I do not believe I am likely to anytime soon.

Specifically, the state-of-the-art right now in this area seems generally to focus on linear/uniqueness typing, borrowing, monomorphisation and allowing unboxed types with suitable restrictions. Let's address each in turn:

• Linearity/Uniqueness Typing - A very powerful type system feature, useful for expressing contracts with types (i.e: safe resource usage) on top of benefits for memory management implementation. However, it is also hard to combine with dependent types. Idris2 has managed the linearity half via QTT, but suffers from a lack of quantity polymorphism that requires code be duplicated to handle the different quantities, which is unnacceptable in an abstraction-driven language IMO.

• Borrowing - Linearity/uniqueness typing also has an additional problem: it is very restrictive (especially if it is the default). Lending a temporary reference (with the caller afterwards still free to drop or move the referenced value safely) becomes pretty necessary when using these typing features in practice. Unfortunately, these guarantees about how long referenced values live for are hard to track, requiring (lifetime) annotations and/or very restricted use. Further, when references become pervasive in a language with subtyping, considerations must be made over whether that subtyping relation is coercive - effectively a decision between variance and efficient/flexible runtime representation. Both would be nice!

• Monomorphisation - Noticing how typeclasses, invented merely as a tool for abstraction in Haskell fit so perfectly with a low-level compilation strategy of compiling distinct versions of functions for each type is in my opinion the coolest thing by far about Rust. It's so clean that I spent quite a few months obsessed with the idea, looking at ways to enhance it ¹.

  Simultaneously, when types are viewed as sets of values, monomorphisation starts to look insane - it's entirely predicated on the idea that the number of sets of values considered by a program is vastly smaller than the number of values it deals with (for one, the number of those sets must be finite or your executable must become infinitely large). This simply isn't the case when subtyping, fancy-typing, let alone dependent typing are added to the mix. Plus as a dual to the predictability you get as a programmer, the compilation strategy reveals implementation details, requiring consideration on whether to suffer executable bloat or dynamic dispatch cost.

• Unboxed Types - I already rejected the duplication of code associated with linearity-without-polymorphism so that I similarly reject it in the context of (un)boxing should come as no surprise - and polymorphism over unboxed values relies on full monomorphisation. Further, giving control over exactly the representation of data inherently leaks implementation details (e.g: the decision of whether to pass by reference or value based on the size a type vs a pointer) to the programmer.

  It is unfortunate that this is probably the feature least compatible with WTy2 and yet is one with potentially the highest impact (zero-cost FP via unboxed closures is very enticing). My hope is that a compiler doing extensive cross-module specialisation might be able to automatically unbox, but this is something that should be explored far down the line.

I argue there are really two main aspects of implementation that these features are focussed on: memory management and runtime representation of values/dispatch strategy. For the former, WTy2 will take inspiration from Lean and Koka (similarly functional, pure, strict programming languages with rich type systems) and adopt a form of reference counting. What's especially nice about this approach is that it combines well with the lower-level type system features that might be added later (in-place updates for values with a refcount of one is just a runtime version of in-place updating of uniques, borrows can skip the refcount increment/decrement etc...). For the latter, in the best case specialising functions for specific sets of values is likely to be a significant optimisation, but the baseline strategy must support WTy2's infinitely large types, existential types etc... - a uniform runtime representation of values is required. See the dedicated section for the current design.

• Extend rust-style impl returns to allow returning values of potentially different types. This can be implemented by monomorphising all code following the call-site and statically dispatching at the return statement.
• Allow variables to be generic (take a type parameter), allowing first-class higher-rank polymorphic functions, and also, perhaps more interestingly, super efficient heterogeneous unordered collections (data-oriented programming without the hassle).