Here’s a video of the latest progress. In this video, I create the term
view reactive (1 + 1), which displays in the editor as
2. This might not seem like much, but the ability to define reactive views like this is the first step in allowing Unison panels to be used much like a spreadsheet, where the user fills in values and other parts of the panel are updated in response. There’s also a few other things shown which I’ll talk through below:
I’ve added a number of builtin functions to the editor. The video makes use of the following functions:
data View a -- builtin data type view : View a -> a -> a source : View a reactive : View a -- of course, there can be many other View values
view function evaluates to its second argument at runtime, but its presence can be used to annotate the syntax tree to override how subtrees are rendered. The first argument is of type
View a (capital ‘V’), and the second argument is of type
a. You’ll notice in the video that after the
1 + 1 has been filled in for the second argument, the admissible type for the first argument is now
The editor interprets
view source blah as the usual source rendering of
blah. It interprets
view reactive blah in the same way, but first evaluates
blah to normal form. Also shown in the video:
swatch, having type
View Color, after the context demanded a
Now I’ll make a controversial claim, which is that the ability to define ‘reactive’ values like this puts us on our way to making the Unison editor a richer, more powerful replacement for spreadsheets. We’re missing a few things, namely a declaration layer, which lets us define and edit more than just a single expression, and also a richer layout library. But with these things in place, this reactivity gives us many of the tools we need to reproduce modern ‘applications’ with a Unison panel. Obviously, at this early stage, the Excel and Google sheets developers shouldn’t be too worried, but with time, the ability of Unison to replicate functionality of these applications will grow quite rapidly.
A2takes the value
= A1 * A3 + B$7, and the user drags to extend the definition to build a whole sequence. Of course, a programmer has no trouble generalizing this sort of thing and just writing a step function that uses symbolic inputs, but it requires less learning to do things the spreadsheet way.
In conjunction with the above points, we also have the network effects of large numbers of people using spreadsheets for similar tasks. A culture develops around the tool, such that spreadsheets become “the way things are done”. This is something that often happens in the evolution of technology. A technology takes hold because it has features that give it a smaller learning curve and wider appeal. Possible alternatives are displaced, but very often, the winning technology has very poor characteristics beyond those that give it an advantage in growing adoption.
As an example, in the finance industry where I used to work, spreadsheets get used for everything and often grow horribly complex. The problem is that while spreadsheets are approachable and require very little learning curve, they’re also quite crippled:
With the Unison editor model, we can cover all the advantages of spreadsheets while providing a much more powerful programming model, and a much richer layout library. I’ll talk more about where this is going in a later post.
As I mentioned in update 3, the type shown in bold when the explorer is opened is the admissible type, which must be a subtype of whatever value the user fills in the explorer. So of course
Number is a subtype of
forall a . a -> [a] is a subtype of
forall a . a -> [a], but also
forall a . a is a subtype of
Number. When the explorer pops up, and in response to the user typing, we need to find all terms in the store which are a supertype of the admissible type, and it’s actually important that type-based search be perfectly accurate. Unlike Hoogle, we can’t get away with returning some ill-typed results that match some processed version of the admissible type (this would allow creation of ill-typed expressions), and we also can’t get away with an overly strict matcher that elides some results that do match (this could result in the user getting stuck, unable to fill in a value that should typecheck).
The problem is that naively doing a subtyping check is going to be overly strict. The admissible type
forall a . a (shown in the editor as just
a, implicitly quantified) is only a subtype of
forall a . a -> a (the type of the identity function) if we allow impedicative instantiation of the type variable
a. Yikes! Rather than open that can of worms, I chose to sidestep the problem. Conceptually, the admissible type is quite useful to display to the user as it lets them know what sort of terms are valid replacements for the node they’ve selected. So the explorer can work in two phases—first, we use a processed version of it as a search query, with the constraint that the search algorithm must at least return any terms that could be supertypes of the admissible type, even at some impredicative instantiation. This is very easy.
Once we have this conservative upper bound on the set of possible matches, we then try replacing each result in the expression being edited, ensuring that the result is well-typed. The replacement in context doesn’t require any impredicativity, it’s just normal typechecking. Anything passing this second level of checks is a valid replacement, and can be shown to the user as a completion in the explorer. So long as the first check phase cuts down the search space to a reasonable number of possible matches, these checks can be done very quickly.comments powered by Disqus