Visual non-linear editing, live programming, and synthesis for (some of) OCaml.

This page contains the video figure (above) and the artifact (below) so you can try Maniposynth yourself.

Abstract

Traditionally, writing code is a non-graphical, abstract, and linear process. Not everyone is comfortable with this way of thinking at all times. Can programming be transformed into a graphical, concrete, non-linear activity? While nodes-and-wires and blocks-based programming environments do leverage graphical direct manipulation, users perform their manipulations on abstract syntax tree elements, which are still abstract. Is it possible to be more concrete—could users instead directly manipulate live program values to create their program?

We present a system, Maniposynth, that reimagines functional programming as a non-linear workflow where program expressions are spread on a 2D canvas. The live results of those expressions are continuously displayed and available for direct manipulation. The non-linear canvas liberates users to work out-of-order, and the live values can be interacted with via drag-and-drop. Incomplete programs are gracefully handled via hole expressions, which allow Maniposynth to offer program synthesis. Throughout the workflow, the program is valid OCaml code which the user may inspect and edit in their preferred text editor at any time.

With Maniposynth's direct manipulation features, we created 38 programs drawn from a functional data structures course. We additionally hired two professional OCaml developers to implement a subset of these programs. We report on these experiences and discuss to what degree Maniposynth meets its goals of providing a non-linear, concrete, graphical programming workflow.

Read the paper for more.

Artifact Download

You can grab the VM or a prebuilt binary. The Ubuntu VM includes the prebuilt binary and VS Code. The advantage of the VM is that VS Code is preconfigured with the OCaml language server and a special highlighting rule to dim AST annotations. The disadvantage of the VM is that it's a 1000x bigger download than the binaries. I also find graphical interaction in VirtualBox to be rather clunky, even with hardware acceleration on. And the VS Code configuration is entirely optional, Maniposynth works with any text editor that will refresh when the file changes on disk (see below for how to enable this in Vim/Emacs if you prefer those editors).

Pre-built binaries (~5MB, effectively what we gave to user study participants):

• Download MacOS Artifact
• Download Linux x86_64 Artifact

VM Image (with VS Code configured)

• Download OVA VM Image (~6.5GB). For some reason, S3 changes the extension to .ovf; change it back to .ova before opening. And you shouldn't need it, but the VM username/password is maniposynth/maniposynth.

Build from source (if the above fail)

• Download Source (It should be easy to build. Install opam and then see the README.md in the source.)

Quickstart

If you dowloaded the VM, there's an "Open Maniposynth" shortcut on the desktop that will start the Maniposynth server, open the artifact folder in VS Code, and open Maniposynth in Chromium on a scratch.ml file.

For the pre-built binaries, enter the artifact folder and start the server. (On Mac, to trust the executable, you will have to right-click the executable and select "Open". After that first time, you can start it from the command line as normal.)

xxxxxxxxxx
        
        

        

        

            

                

                

                
                
$ ./maniposynth
            
        
    
    
    
    
    

    
    

    
    
    

Then open Chrome and navigate to a file path relative to the server, e.g. http://localhost:1111/examples/length.ml. You can also create a new file (in your editor) and type that file path in the URL, e.g. http://localhost:1111/scratch.ml.

Open up the same file in your editor, side by side, for the full bimodal experience.

If you have ocamlformat installed and in your $PATH, generated code will have better formatting, but this is not required.

Live Refresh

VS Code will automatically refresh when code is changed on disk. For Vim and Emacs, see below:

Vim

Thanks to eli on Super User for this solution. Run this in Vim:

xxxxxxxxxx
    
    

    

    

        

            

            

            
:set autoread | au CursorHold * checktime | call feedkeys("lh")
        
    
    
    
    
    
    

    
    

    
    
    

After cursor stops moving, this will check every updatetime seconds for file changes, which is every 4 seconds by default. (More specifically, Vim waits for the cursor to stop moving for some time, then checks disk, then moves the cursor again with “lh” to retrigger and loop.)

To poll every half second instead of every 4 seconds:

xxxxxxxxxx
    
    

    

    

        

            

            

            
:set updatetime=500
        
    
    
    
    
    
    

    
    

    
    
    

If you get annoying bells, turn Vim’s bell off:

xxxxxxxxxx
    
    

    

    

        

            

            

            
:set visualbell t_vb=
        
    
    
    
    
    
    

    
    

    
    
    

Emacs

For Emacs, enable global-auto-revert-mode:

1. Hit F10 to go to the top menu
2. Options > Customize Emacs > Specific Option
3. Type global-auto-revert-mode
4. Move the cursor to [ Toggle ] and hit Enter
5. Move to [ Apply and Save ] and hit Enter

Dimming AST Annotations (Optional)

To dim AST attribute annotations to make code more readable, in VS Code install the Highlight extension (fabiospampinato.vscode-highlight). This artifact includes a .vscode/settings.json that contains the regex and styling for annotations. It should "just work" if you open the artifact folder in VS code (e.g. via code artifact). You may have to edit the styling in .vscode/settings.json if you use a dark theme. (The VM is already configured with the Highlight extension.)

Bugs to know

• Pasting code that was copied from a rich-text source often fails. You will have to retype the code manually or try pasting into a plain text buffer and recopying.
• The positioning code is still not great—don't fight too much with trying to reposition things if they do not end up where you want. If something "disappears", it was probably bumped further down the page.
• If the page fails to render at all, there is likely a major type error or syntax error in your code. You will have to repair the file in your text editor and then refresh the browser. The Maniposynth terminal output may provide a hint as to what's wrong.
• The undo history does not remember edits that happened in the text editor.

Have fun!

Artifact Evaluation Walkthrough

For artifact evaluation, we claim (a) that our artifact works as described in the Overview example in Section 2 of the paper, and (b) that our artifact works not just on the overview example.

To verify these claims, (a) we ask the artifact reviewers to follow the walkthrough in the paper Overview, including the variations, and (b) we ask the reviewers to try one example of their own choosing, either of their own design or from Table 1.

Initial variation (Sec 2.1)

Start with a blank file. (Delete everything in your text editor and save.)

• Double-click on top-level canvas to add code.

• Type [, then autocomplete to [0; 0; 0] and hit Enter to select the autocomplete option, then Enter again to submit.

• Notice the new let-binding int_list = [0; 0; 0] on the canvas and in the code. This box is a tangible value (TV).

• Try repositioning the TV: hover the cursor near the edge of the box (a gray border should appear) and then drag the TV to a new position.

• Verify the TV moves, and a [@pos ...] attribute appears in the code.

• Double-click on the white canvas to add code, write length int_list and hit Enter.

• Notice the new function skeleton on the canvas and in the code.

• Double-click the pink-background x1 and rename it to list.

• Drag length (??) from the toolbar at the top of the window into the subcanvas inside length (the whitespace below "Bindings inside function").

• Notice the new let-binding length2 = length (??).

• Notice the length function is now recursive (let rec length list = ...).

• Hover the cursor over the opening [ on the input list in the IO grid, press Destruct.

• Notice the new match case split in the code, with two branches.

• Notice the pink hd and tail name subscripts on the input list [0; 0; 0] in the IO grid.

• Notice the hd and tail pattern TVs on the subcanvas (below "Bindings inside function").

• Notice "⇠ list ⇢" and the two return TVs in the returns area ("Return expression(s) and value(s)"), one return for each branch.

• Drag the tail list (either the value [0;0] or the tail name) onto the (??) of length (??).

• Notice in the code that length2 = length tail is now in a particular branch inside the match case split.

• You may want to toggle the "Show variable values instead of variable uses" option on or off in Maniposynth's gear menu, according to your preference. Off is more understandable (and matches the screenshots in the paper).

• Click on [] in the IO grid to focus the call frame for the base case.

• Notice that all the TVs in the function are grayed out, except for the return TV for that branch (which is still a hole (??)).

• Double-click that (??) and set it to 0.

• Click [0] in the IO grid to bring the second-to-last call frame into focus.

• Double-click the remaining hole (??) and begin typing "1 + " (one space plus space).

• Notice the values have been colored.

• Autocomplete to the 0 that has the same color as the return from length2 = length tail.

• Notice that the return expression is now 1 + length2.

• Notice in the IO grid that the function is producing the expected outputs for all inputs.

Undo and delete (Sec 2.2)

This section claims that Undo works, and delete works on expressions and on let-bindings.

• Click some expression (black text on green background) and hit delete; verify it becomes (??).

• Hit Undo; verify it undid.

• Click a let-binding TV such as length2 = length tail (click the outer edge of a box to select the whole binding) and hit delete. If the binding is still used, it will become (??).

• Delete the length2 use, then try deleting the length2 binding. Verify the let-binding disappears.

Drag-to-extract (Sec 2.3)

• Undo until the length function contains only length2 = length (??) but no match statement. (Make sure the display refreshes between each time you click Undo, otherwise you may have to clear the file and start over.)

• Hover your cursor over the first ; in the input list. ; 0; 0] should be highlighted. Drag this into the (??) in length (??).

• Notice that the match case split is inserted and the binding is now length2 = length tail.

Autocomplete-to-extract (Sec 2.3)

• Undo until the length function exists, but is just an empty skeleton with no let-bindings.

• Double-click the return hole expression, type "1 + length " (one space plus space length space), and autocomplete to the ; 0; 0] tail.

• Notice that the function is now nearly complete, except for a hole for the base case.

Asserts (Sec 2.3)

• Clear the file in your text editor and save. (The browser should refresh to a blank canvas—if not, hit reload.)

• Double-click on top-level canvas and write length [0; 0; 0] = 3

• Notice that an assert is created (in addition to a skeleton for length).

• In the function IO grid, press the "+" button, and add an assert that given the input [] the output should be 0. Hit enter.

• Notice another assert is created.

• Edit the return hole (??) to 0 and notice one assert becomes satisfied.

Program Synthesis (Sec 2.3)

• Undo until there is only one assert (length [0; 0; 0] = 3).

• Press "Synth".

• Notice the incorrect result (always returns 3 for each input).

• Press "Accept case split".

• Press "Reject" on one of the return expressions.

• Press "Reject & try again" on the other.

• Notice the correct result.

• Press "Accept" on each sub-result.

Subvisualizations, with asserts (removed from final paper)

• Clear the file in your text editor and save. (The browser should refresh to a blank canvas— if not, hit reload.)

• Double-click and write [0; 0; 0].

• Click on the literal output value (the opening [ of the bold value below int_list = [0; 0; 0])

• In the textbox next to the "Visualize" button, write length and press "Visualize"

• Notice the ? subvisualization superscripts on the [0; 0; 0] value. (A length skeleton is also created.)

• Double-click the first ? superscript, write 3 and hit Enter.

• Notice an assert is added, and a blue expected value 3 appears in the superscript.

• Similarly assert that the tail length should be 2 (the tail length is the third ?.)

• Press Synth to produce the correct function, accept the result.

• Notice the superscripts on the 0 integer values have disappeared (they are no longer type-compatible with length.)

• Notice the first two superscripts are rendered in green, indicated satisfied asserts.

Try your own example

Pick a simple function of your choice and try to implement it—the easier exercises in Table 1 can be an inspiration. Final code for each example in Table 1 is included in the artifact/examples folder, if that is helpful. It is okay to perform text edits in your editor if you get stuck—this is a bimodal environment after all! Hints:

• Reminder: the expected way to create a new function is always to provide an example call, before the function exists.

• If you need a new type, double-click on the top-level canvas and write a valid OCaml type declaration. Here are the types used in the Table 1 examples (copy-paste of these may not work, you may have to retype manually or paste into your text editor):

  xxxxxxxxxx
              
              
  
              
  
              
  
                  
  
                      
  
                      
  
                      
  type nat = Z | S of nat
                  
                  
  type 'a ltree = Node of 'a ltree * 'a ltree | Leaf of 'a
                  
  type 'a btree = Node of 'a btree * 'a * 'a btree | Empty
              
              
              
              
              
              
  
              
              
  
              
              
              

• If you are using such a custom type, remember that the toolbar at the top will contain example values that you can drag onto your canvas or into a subexpression (hover your cursor over the down arrow ▾).

• The synthesizer is unlikely to guess an if-then-else expression correctly. Drag the if (??) then (??) else (??) skeleton from the first toolbar menu into your code and at least fill in the conditional.

• More inspiration: the following single asserts will synthesize the correct function with no extra information. One trick is using uncommon constants so that the synthesizer will not guess constant literals (e.g. 17):

  xxxxxxxxxx
              
              
  
              
  
              
  
                  
  
                      
  
                      
  
                      
  fold ( + ) [ 1; 2; 3 ] 11 = 17
                  
                  
  map succ [ 1; 2; 3 ] = [ 2; 3; 4 ]
                  
  list_sum [ 10; 20; 30 ] = 60
              
              
              
              
              
              
  
              
              
  
              
              
              

  (Copy-paste may not work, you may have to retype the above.)

  To verify the function is correct, it's helpful to rename the arguments (double-click the pink names).