Programmatic and Direct Manipulation, Together at Last

A technical report by Ravi Chugh et al. Abstract:

We present the SKETCH-N-SKETCH editor for Scalable Vector Graphics (SVG) that integrates programmatic and direct manipulation, two modes of interaction with complementary strengths. In SKETCH-N-SKETCH, the user writes a program to generate an output SVG canvas. Then the user may directly manipulate the canvas while the system infers realtime updates to the program in order to match the changes to the output. To achieve this, we propose (i) a technique called trace-based program synthesis that takes program execution history into account in order to constrain the search space and (ii) heuristics for dealing with ambiguities. Based on our experience writing more than 40 examples and from the results of a study with 25 participants, we conclude that SKETCH-N-SKETCH provides a novel and effective work- flow between the boundaries of existing programmatic and direct manipulation systems.

This was demoed at PLDI to a lot of fanfare. Also see some videos. And a demo that you can actually play with, sweet!

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

This looks *very* promising

I have been dreaming about something like this for a long time. Almost all the illustrations I make are of the kind that would benefit from a mixed programmatic/direct approach.

It also looks like a good starting point for reconciling graphics with version control. The Little code should support diffing and merging just like any other code, whereas merging changes to an SVG almost always creates a mess.

Wish list:
- integration with a good SVG editor (Inkscape would be a good start)
- integration with a decent programming language ecosystem for interfacing with non-graphic code (Racket looks like a good candidate)

General problem

I think the general premise of this work, that direct manipulation is often preferable to programmatic representation, is on the mark and a useful idea for programming language design in general. For example, this is why programmers prefer C style formatting strings to C++ streams - the formatting string is a WYSIWYG representation of the output.

This work seems to focus on the case where the parametric family specified is only a means to an end (the final vector graphics). Things get harder when you need to visualize the entire parametric family and also when the data you're defining isn't intrinsically graphical. I know Sean has worked on these issues and made comments about desiring "continuity" in general domains.

I don't see how the specific heuristics proposed here will generalize to other domains and suspect they may have problems working "at scale" with a complicated vector model. That's the the real meat of problem that I'm interested in. Manually annotating which variables get sliders is closer to where I see this kind of thing heading -- easy support for building visualization / manipulation elements.

It is a start.

Frankly, I'm just happy others see this as an interesting avenue of research, even if the road is long long to getting to something that works. I've been thinking a lot about this lately. Programming as a problem solving activity basically abstracts concrete examples (usually with paper and a white board, our existing programming environments do not help much). 2D graphical domains have the most obvious path to supporting this process using a programming environment, and it shouldn't be a surprise that we start there.

So the first step is to figure what we are doing for 2D graphics, then the next step is to break out of the 2D box. Even in the first step, there is a lot to do; how do we create parametric 2D diagrams via direct manipulation?


And the last paragraph of my post above sounded pretty harsh and pompous when I re-read it, so I edited it and toned it down. I didn't change the point I was trying to make, which is basically that, if you generalize enough, the problem becomes "programming by example" (provide inputs and outputs and the compiler will generate the program) which is AI complete / very hard. I would rather focus on making it easy to build user specified manipulable visualizations rather than trying to automate too much.

Yes it does! On the other

Yes it does! On the other hand, programming by example can be made more feasible by making it more interactive: the compiler just doesn't choose an implementation, but helps you find one based on known inputs and outputs. Direct manipulation is just w way to express concrete inputs and outputs...we are then just missing the faculties to abstract between the two (like add a unifying variable when two properties have similar values).

Guided proof search

Given a specification for a program as a type (dependent type, or logic meta-program), an implementation of that specification is a proof. Programming by example becomes a proof search, and what you are looking for is a guided proof search. I am interested in this, but from a REPL sort of interface. Of course like python workbooks, the program input and output could be graphics or graphs.

Most programs don't involve

Most programs don't involve proofs, so this approach doesn't appeal to me, but isn't that exactly what COQ does already?

Badly. Does badly.

Badly. Does badly.

The program is the proof

Most programs do not include proofs they are the proof. For example I want a program with the type signature : forall a . a -> a, does such a program exist? What is the shortest proof? The proof is the implementation, and in this case it is trivial to find (\x . x). Yes Coq can do this, and that was my point, the technology to do what you want already exists. I prefer Twelf.

Degenerate solutions

A set of examples doesn't constitute a very rigorous specification, though. Programming-by-example is usually severely under-constrained.

Degenerate is fine

Degenerate is fine, as you stop on the first solution, or find the shortest solution (within bounded time or search depth). For a simple example consider the type:
forall a b . (a, c, b) -> (a, d, b) which is underspecified (we effectively don't care what c and d are). It's fairly easy to see how this can be extended to arbitrary arrays of numbers with unknowns representing input and output vectors (you only need a type level encoding for ints. So a function to map the array [1, ?, 3] to [2, ?, 4] becomes the search for a function to implement the type: ((()), a, (((())))) -> (((())), b, ((((()))))), or something like that with a better encoding of ints. The shortest solution is (\x . x + 1), of course by pure search this might be difficult to find, you might need t give a strategy hint to try applying the same transform to all elements, and then search a library of simple arithmetic operators to see if any fit (or nearly fit).

Rhetoric and related work

I find that there is a large over-interpretation of the Curry-Howard correspondence, and I would recommend avoiding the claim that "programs are proof". In my experience, this point is often misunderstood and leads to claims that are blown out of proportion. On the contrary, claiming that "proofs are programs" seems to have a much lower nuisance potential.

I do more than agree on the general point that techniques derived or inspired from proof search can be helpful to program synthesis. (I have not yet read the paper cited in this thread, but I'm not sure it is so relevant in this case.) The idea that examples can be understood as a form of under-specification, and integrated in a more general proof-search-inspired synthesis mechanism, has been realized in particular in Example-Directed Synthesis: A Type-Theoretic Interpretation, by Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic, 2016, which you may be interested in.

Most programs don't prove anything useful?

I think your point is that most programs don't prove anything useful. For example a lot of programs prove the Haskell type IO () is inhabited, yet they all do different things. This argument is somewhat weakened by Haskell having no side effect control. What happens when the hypothesis includes more meta-information about the program than just types, but can include static values, and other properties. This is why I tend to view a hypothesis as a meta-program and not a type, so its no longer limited by curry-howard.

Haskell programs only prove

Haskell programs only prove things in a very boring logic; specifically the logic where all propositions are provable. This is one of the reasons that gasche's claim is right -- very few typed programs "prove" anything in a logic of any interest.

Recognizing the elephant

This is not only the same elephant as programming-by-example, but also the same elephant as aspect-oriented programming. In all of these, the problem is how to deduce the whole from some parts (which is of course, meta, the problem with the elephant as well).

Visual programming

Well, if you "parameterize" the sliders instead then you get the kind of visual programming you see in 3d content tools. That seems to have won out versus regenerating textual code as in this svg example.

i wish the cake were not a lie

I want to have it and consume it. I want the sliders and the ascii. I want it all working together. I don't want to have to choose one or the other.

Maya Ascii

Well, with Maya you have Maya Ascii - but I doubt you'll really want to look at it.