Paul Chiusano

Functional programming, UX, tech, econ

TwitterGitHubLinkedInRSS


Consulting services

I offer Scala and FP consulting services. If you're interested in working together, please contact me.


About my book

My book, Functional Programming in Scala, uses Scala as a vehicle for teaching FP. Read what people are saying about it.


Popular links

Unison: a next-gen programming platform
unison.cloud: the worldwide elastic computer (coming soon)
Type systems and UX: an example
CSS is unnecessary

Unison update 5: a better spreadsheet

[   fp   unison   ]            

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:

What’s going on?

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

The 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 View Number.

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:

A better spreadsheet, and a better application framework

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.

Programmers like to scoff at spreadsheets, but they’re extremely popular among nonprogrammers. Why is that? Here are just a few reasons:

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.

Technical note: avoiding the need for impredicative instantiation when searching for functions

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 Number, and 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