Gradual Typing

Jeremy Siek is doing some great work on gradual typing, and it may get incorporated into Jython. Here is a presentation, and a video. A similar idea is Gilad Bracha’s Pluggable Types. JavaScript 2 had planned to do gradual typing, though it is unclear if that will survive the collapse of the project.

It seems I usually have negative things to say here, so I wanted to note an example of something positive. Jeremy’s work is Computer Science that is imminently relevant to practicing programmers. I think gradual types are an inevitable feature of future programming languages.

2 Replies to “Gradual Typing”

  1. Looking at Gilad Bracha’s paper I agree with the approach of formalizing the semantics of a language without a type system and the underlying idea that a type system shouldn’t change the language semantics. However, I have some doubts about the claimed advantages of optional type systems. I guess I found the handwaving about expressiveness to be unconvincing without examples (but fine for a
    workshop paper which I think is what I was reading).

    One idea I don’t like is the idea that a type system is for reasoning about any property you want. I think restricting the term to be used for reasoning about types makes sense just for reasons of clarity. The idea of resoning about other properties like aliasing, mutual exclusion, ownership or whatever strikes someone’s fancy sounds useful though.

  2. The examples in the presentation are pretty weak from a practical stand-point. All it demonstrates is what I call “syntax removal”.

    In its present form, Siek’s work has very little practical value. However, from a futuristic perspective, gradual type systems are a necessary requirement for building multi-stage programming libraries. What I can see is amazing applications for this stuff in the realm of visual languages. It would smoke using something like LLVM or Phoenix to manipulate byte codes/assembly instructions, as both these approaches have a fixed number of levels for hoisting/sinking instructions to higher/lower abstractions. Obviously, the technology in its present form compared to these two heavyweights is comparing apples to oranges, but the trick here is to think of widely different directions for gradual type systems.

    “Gradually graphing” a solution represents my favorite technique for thinking about how to build large systems. This style of programming was a huge part of early OOPSLA and ECOOP papers, but has since faded in fashion in favor of strangely verbose language research projects and proposals. Karl Lieberherr’s Demeter Method, Gregor Kiczales’s aspect-oriented programming and Paul Bassett’s frame-oriented programming are really the last innovations in how to succinctly “program between the lines”. People are now just arguing microscopic details, i.e. “feature-oriented programming” is mainly just about combining types based on equivalence relations between categories, then putting it into a champagne gown and slapping lipstick on it. I’m not a fan of researchers wasting funding dollars to these details — its more about academics pushing a slightly different methodology than standard OOP. This is like game theorists publishing papers on “refinement of Nash equilibrium”. Visual languages that use gradual type systems would be a gamechanger, as the pitch would be that you could gradually piece together a graph using whatever style you wish, be it copy-and-paste or whatever.

    Obviously, JavaScript 2 is not a compelling end-game, anyway, so it’s just as well if it doesn’t survive.

Comments are closed.