Data transformations in Vega

Abstract

Vega je populární knihovna na vytváření deklarativních vizualizací. Vega je velice flexibilní a široce používaná, avšak má limitované zpracování a nahlašování chyb. Zejména neplatný přístup k položkám datových zdrojů může vést k běhovým chybám a také k matoucím výstupům. V této práci řešíme problém neplatného přístupu k položkám datových zdrojů ve velké podmnožině specifikací Vega. Abychom mohli jasně uvažovat o přístupu k položkám, popisujeme for- mální sémantiku esence Vegy, o čemž se domníváme, že se zatím nikdo nepokusil. Představujeme typový systém založený na Vega transformacích manipulujících tvary datových zdrojů. Spolu s typovým systémem definu- jeme i grafově založenou malokrokovou operační sémantiku, která odpovídá běhovému vyhodnocování v prostředí Vega. Dokážeme, že námi navržený typový systém je korektní. Typovací pravidla navíc implementujeme v prototypovém typecheckeru, který hlásí různé prob- lémy související s přístupem k položkám, v podmnožině specifikací Vega, které využívají běžné transformace.

Vega is a library for creating data visualizations in a declarative way. Vega is very flexible and widely used, but has limited error handling and reporting capabilities. Most notably, invalid field access in Vega specification can result in errors as well as confusing outputs. In this thesis, we resolve the issue of invalid field access in a large subset of Vega specifications. To enable accurate reasoning about field access in Vega, we describe a formal semantics of the language - a contribution we believe to be novel. Our approach includes a type system that models how Vega transformations manipulate dataset shapes. Complementing this, we define a graph-based small-step operational semantics that corresponds to Vega's runtime evalua- tion. We prove that our type system is sound. We implement the typing rules in a proof-of-concept typechecker, which reports various access-related issues in a subset of Vega specifications which use common transformations.