Lambda the Ultimate

I've been working with a type system where type requirements are not actually checked, but added automatically to the program as needed. Such a type system can better support for bottom-up programming, but also allows for lots of small types (like mixins) in a library without the requiring programmers to tediously compose their objects. As a small example, consider a UI library with various kinds of panels that vary depending on how they manage layout:

trait Panel { ... }
trait Canvas :: Panel { ... }
trait Dock :: Panel { ... }

trait Widget(c: Panel) { ... }


This language has no classes, just mixin-like traits. The :: operator means exclusive class-like inheritance, meaning Canvas and Dock cannot both be extended by the same panel object, while the : operator means normal mixin inheritance as in Scala. Canvas supports manual widget positioning, while dock allows the widget to be docked at the edge or center of the panel. We express this by defining two new kinds of widgets that exist in each panel:


trait CanvasWidget(c : Canvas) : Widget(c) { var Position : Point; }
trait DockWidget(c : Dock) : Widget(c) { var Dir : Direction; }


Now, we can define a program using just panel and widget:

val p = new Panel();
val w = new Widget(c = p);
w.Position = (100, 100);


When this code is compiled, "w" implicitly extends CanvasWidget because Position was accessed on it, which incidentally causes "p" to implicitly extend Canvas. The inference occurs at compile time, p is a canvas from the moment it is created.

All abstractions exist in a flat space and are somehow uniquely named so the programmer can select them (think wiki's disambiguation pages). Inference can then occur because the user selected a specific abstraction whose typing requirements are known, as opposed to the other way around where the type determines how a name is resolved. The usability benefits come from the user not having to know about special kinds of widgets and panels; rather they can focus on what they want to do rather than how to enable that. In general, we could then build libraries with hundreds of little traits as an extreme form of "batteries included," where the user need not be aware of most of these traits as they are applied automatically as needed.

Conflicts can arise if inference requires an object to extend two incompatible traits; e.g.,

val p = new Panel();
val w = new Widget(c = p);
w.Position := (100, 100);
w.Dir := Center;

An error occurs because "p" cannot extend both Canvas and Dock, which is necessary to support widget's access of both position and direction, the error in this case is actually on "p" rather than the accesses. My current implementation is a structured editor which would just hide "Direction" after "Position" was accessed.

I'm calling this prescriptive trait inference as an alternative to type inference which acts to catch errors rather than build programs; although this might be a bit unfair since implicit coercions driven by type inference can actually cause computation to occur (say in Scala). I want to go further on this design and build a more general language, which involves tackling the following problems:

• Supporting trait inference with imperative assignment. Basically, any value assigned to a variable is affected by traits inferred for that variable, without any regard to control flow; e.g.,

  
val dict = new Dictionary();
val e, f = new object();
dict[1] := e; dict[2] := f;
dict[some_int].Quack(); // e and f are now inferred to be ducks!


• Inference must occur in a modular way. Each encapsulation unit has its own "inference graph" that describes how values flow through it. Private members are elided from this graph to get a nice modular graph that then allows the unit to be used during inference without resorting to whole program analysis.
• "Anything goes" presents two new usability problems. First, the type of an object being created is no longer determined solely by its creation site, this can make the program harder to understand without proper tooling that reveals what has been implied. Second, that a programmer can use almost any abstraction in a large universe at any time makes normal auto-completion useless (which depends on types for filtering), the abstractions instead need to be "ranked" somehow.

Ah, this post is way too long; hopefully this doesn't come off as a brain dump. Anyways, I would appreciate some early feedback before I go off and do a general purpose language (I'm off to Krabi tomorrow, but I can't stop thinking about this :) ).