1 of 13

Grove: A Bidirectionally Typed Structure Editor Calculus

Michael D. Adams, Eric Griffis, Thomas J. Porter,

Sundara Vishnu Satish, Eric Zhao, Cyrus Omar

2 of 13

01

Table of contents

02

03

04

Introduction

Grove By Example

Type-Checking &

Inference

Additional Information

3 of 13

Introduction

4 of 13

Problems in traditional VCS

The Granularity Problem

Alice’s Edits

b) Bob’s Edits

c) Merge Conflict

5 of 13

The Relocation Problem

Alice’s edits

Bob’s edits

c) After sharing edits

6 of 13

Grove by Example

Now let’s look at some of the interesting cases that can arise in a collaborative settings and how Grove handles them

commutativity of edits (CmRDT)
directed multigraph
UIDs on vertices and edges
decomposition into groves

Now this happens because traditional version control systems like git rely on a patch language and three-way merge algorithms because they diff the results to synthesize patches. So they often struggle with correctly identifying and managing conflicts particularly when its changes to the same line or relocation of code. Through Grove, we propose a novel approach that derives patches by looking at the edit history eliminating patch synthesis and three-way merge algorithms. So all the edits in Grove commute and the repository state forms what is known in the research literature as a (commutative replicated data type) CmRDT. And the core data-type underpinning grove is a directed multigraph with uniquely identified vertices and edges. However, users edit is a tree-native setting so we decompose graphs intro groves, which are set of syntax trees with in-built support for the various conflicts that can occur.

7 of 13

Picture 1

Picture 2

Picture 3

8 of 13

Relocation Revisited

9 of 13

The Grove Workbench

10 of 13

Type-checking & Inference

Builds upon Total Error Localization & Recovery (cite)
Conventional bi-directional typing system
Unmarked - (marking) -> Marked
Marked Exps are used to gather inference constraints & location conflict contexts (& how they are useful)
Briefly define all the things here & add pictures of the judgments

11 of 13

Mechanized Metatheory + Workbench

12 of 13

Thank you!

13 of 13

Thanks!

Do you have any questions?

youremail@freepik.com

+91 620 421 838

yourwebsite.com

Please keep this slide for attribution

CREDITS: This presentation template was created by Slidesgo, and includes icons by Flaticon and infographics & images by Freepik