It’s been my goal to actually start writing a language for a while, and I think early 2026 is as good a time as any.
My first goal is to implement something with both higher-kinded polymorphism and subtyping. Full type inference isn’t a goal; what I’ve seen in examples for bidirectional type inference would be plenty, and I generally have a high tolerance for sprinkling on additional manual annotations when needed.
I’m planning on working through “Programming Language Foundations in Agda” to get started. For actually designing the type system, is “Algebraic Subtyping”by Stephen Dolan a good place to start?
I would really appreciate any signposts that people who are more familiar with this world would be willing to provide 🙏