Omega – Language of the Future
When I discovered Tim Sheard’s Languages of the Future, I realized that PLs do indeed have a future. Compared to “medieval” languages like Lisp, pre-generics Java, and Python, the more “futuristic” languages like Haskell, O’Caml, and Scala seemed to mainly offer additional static verification, and some other neat patterns, but the “bang for the buck” seemed somewhat low, especially since these languages have their own costs (they are much more complex, they rule out many “perfectly fine” programs).
Ωmega seems like a true revolution to me – it shows what can be done with a really fancy typesystem, and this seems like the first astounding advancement over existing languages, from Python to Haskell. Its mantra is that it’s possible to reap many (all?) benefits of dependent programming, without having to suffer its problems, by adding two much more humble notions to the well-understood, ordinary functional programming setting: GADTs + Extensible Kinds.
Sheard and coworkers show that these two simple extensions allow the succinct expression of many dependently-typed and related examples from the literature. Fine examples are implementations of AVL and red-black trees that are always balanced by construction – it’s simply impossible to create an unbalanced tree; this is checked by the type-system. It seems somewhat obvious that sooner than later all code will be written in this (or a similar) way.
How to understand this stuff: my route was through the generics of Java and C# (especially Featherweight Generic Java, FGJω, and all of A. Kennedy’s generics papers). Once you understand notions like type constructors, variance, and kinds, you basically know everything to understand why GADTs + Extensible Kinds = Dependent Programming (and also why polytypic values have polykinded types for that matter).
It is my belief that you must understand Ωmega now! Even if you’re never going to use it, or something like it, you’ll still learn a whole lot about programming. Compared to Ωmega, other languages are puny. ;P
Source: Omega – Language of the Future