-
Live & Local Schema Change: Challenge Problems
Authors:
Jonathan Edwards,
Tomas Petricek,
Tijs van der Storm
Abstract:
Schema change is an unsolved problem in both live programming and local-first software. We include in schema change any change to the expected shape of data, whether that is expressed explicitly in a database schema or type system, or whether those expectations are implicit in the behavior of the code. Schema changes during live programming can create a mismatch between the code and data in the ru…
▽ More
Schema change is an unsolved problem in both live programming and local-first software. We include in schema change any change to the expected shape of data, whether that is expressed explicitly in a database schema or type system, or whether those expectations are implicit in the behavior of the code. Schema changes during live programming can create a mismatch between the code and data in the running environment. Similarly, schema changes in local-first programming can create mismatches between data in different replicas, and between data in a replica and the code colocated with it. In all of these situations the problem of schema change is to migrate or translate existing data in coordination with changes to the code.
This paper contributes a set of concrete scenarios involving schema change that are offered as challenge problems to the live programming and local-first communities. We hope that these problems will spur progress by providing concrete objectives and a basis for comparing alternative solutions.
△ Less
Submitted 20 September, 2023;
originally announced September 2023.
-
Self-Supervised Depth Correction of Lidar Measurements from Map Consistency Loss
Authors:
Ruslan Agishev,
Tomáš Pětříček,
Karel Zimmermann
Abstract:
Depth perception is considered an invaluable source of information in the context of 3D map** and various robotics applications. However, point cloud maps acquired using consumer-level light detection and ranging sensors (lidars) still suffer from bias related to local surface properties such as measuring beam-to-surface incidence angle, distance, texture, reflectance, or illumination conditions…
▽ More
Depth perception is considered an invaluable source of information in the context of 3D map** and various robotics applications. However, point cloud maps acquired using consumer-level light detection and ranging sensors (lidars) still suffer from bias related to local surface properties such as measuring beam-to-surface incidence angle, distance, texture, reflectance, or illumination conditions. This fact has recently motivated researchers to exploit traditional filters, as well as the deep learning paradigm, in order to suppress the aforementioned depth sensors error while preserving geometric and map consistency details. Despite the effort, depth correction of lidar measurements is still an open challenge mainly due to the lack of clean 3D data that could be used as ground truth. In this paper, we introduce two novel point cloud map consistency losses, which facilitate self-supervised learning on real data of lidar depth correction models. Specifically, the models exploit multiple point cloud measurements of the same scene from different view-points in order to learn to reduce the bias based on the constructed map consistency signal. Complementary to the removal of the bias from the measurements, we demonstrate that the depth correction models help to reduce localization drift. Additionally, we release a data set that contains point cloud data captured in an indoor corridor environment with precise localization and ground truth map** information.
△ Less
Submitted 23 May, 2024; v1 submitted 2 March, 2023;
originally announced March 2023.
-
Technical Dimensions of Programming Systems
Authors:
Joel Jakubovic,
Jonathan Edwards,
Tomas Petricek
Abstract:
Programming requires much more than just writing code in a programming language. It is usually done in the context of a stateful environment, by interacting with a system through a graphical user interface. Yet, this wide space of possibilities lacks a common structure for navigation. Work on programming systems fails to form a coherent body of research, making it hard to improve on past work and…
▽ More
Programming requires much more than just writing code in a programming language. It is usually done in the context of a stateful environment, by interacting with a system through a graphical user interface. Yet, this wide space of possibilities lacks a common structure for navigation. Work on programming systems fails to form a coherent body of research, making it hard to improve on past work and advance the state of the art. In computer science, much has been said and done to allow comparison of **programming languages**, yet no similar theory exists for *programming systems*; we believe that programming systems deserve a theory too.
We present a framework of *technical dimensions* which capture the underlying characteristics of programming systems and provide a means for conceptualizing and comparing them. We identify technical dimensions by examining past influential programming systems and reviewing their design principles, technical capabilities, and styles of user interaction. Technical dimensions capture characteristics that may be studied, compared and advanced independently. This makes it possible to talk about programming systems in a way that can be shared and constructively debated rather than relying solely on personal impressions. Our framework is derived using a qualitative analysis of past programming systems. We outline two concrete ways of using our framework. First, we show how it can analyze a recently developed novel programming system. Then, we use it to identify an interesting unexplored point in the design space of programming systems.
Much research effort focuses on building programming systems that are easier to use, accessible to non-experts, moldable and/or powerful, but such efforts are disconnected. They are informal, guided by the personal vision of their authors and thus are only evaluable and comparable on the basis of individual experience using them. By providing foundations for more systematic research, we can help programming systems researchers to stand, at last, on the shoulders of giants.
△ Less
Submitted 20 February, 2023;
originally announced February 2023.
-
AI Assistants: A Framework for Semi-Automated Data Wrangling
Authors:
Tomas Petricek,
Gerrit J. J. van den Burg,
Alfredo Nazábal,
Taha Ceritli,
Ernesto Jiménez-Ruiz,
Christopher K. I. Williams
Abstract:
Data wrangling tasks such as obtaining and linking data from various sources, transforming data formats, and correcting erroneous records, can constitute up to 80% of typical data engineering work. Despite the rise of machine learning and artificial intelligence, data wrangling remains a tedious and manual task. We introduce AI assistants, a class of semi-automatic interactive tools to streamline…
▽ More
Data wrangling tasks such as obtaining and linking data from various sources, transforming data formats, and correcting erroneous records, can constitute up to 80% of typical data engineering work. Despite the rise of machine learning and artificial intelligence, data wrangling remains a tedious and manual task. We introduce AI assistants, a class of semi-automatic interactive tools to streamline data wrangling. An AI assistant guides the analyst through a specific data wrangling task by recommending a suitable data transformation that respects the constraints obtained through interaction with the analyst.
We formally define the structure of AI assistants and describe how existing tools that treat data cleaning as an optimization problem fit the definition. We implement AI assistants for four common data wrangling tasks and make AI assistants easily accessible to data analysts in an open-source notebook environment for data science, by leveraging the common structure they follow. We evaluate our AI assistants both quantitatively and qualitatively through three example scenarios. We show that the unified and interactive design makes it easy to perform tasks that would be difficult to do manually or with a fully automatic tool.
△ Less
Submitted 31 October, 2022;
originally announced November 2022.
-
Typed Image-based Programming with Structure Editing
Authors:
Jonathan Edwards,
Tomas Petricek
Abstract:
Many beloved programming systems are image-based: self-contained worlds that persist both code and data in a single file. Examples include Smalltalk, LISP, HyperCard, Flash, and spreadsheets. Image-based programming avoids much of the complexity of modern programming technology stacks and encourages more casual and exploratory programming. However conventional file-based programming has better sup…
▽ More
Many beloved programming systems are image-based: self-contained worlds that persist both code and data in a single file. Examples include Smalltalk, LISP, HyperCard, Flash, and spreadsheets. Image-based programming avoids much of the complexity of modern programming technology stacks and encourages more casual and exploratory programming. However conventional file-based programming has better support for collaboration and deployment. These problems have been blamed for the limited commercial success of Smalltalk. We propose to enable collaboration in image-based programming via types and structure editing.
We focus on the problem of schema change on persistent data. We turn to static types, which paradoxically require more schema change but also provide a mechanism to express and execute those changes. To determine those changes we turn to structure editing, so that we can capture changes in type definitions with sufficient fidelity to automatically adapt the data to suit. We conjecture that typical schema changes can be handled through structure editing of static types.
That positions us to tackle collaboration with what could be called version control for structure editing. We present a theory realizing this idea, which is our main technical contribution. While we focus here on editing types, if we can extend the approach to cover the entire programming experience then it would offer a new way to collaborate in image-based programming.
△ Less
Submitted 17 October, 2021;
originally announced October 2021.
-
System for multi-robotic exploration of underground environments CTU-CRAS-NORLAB in the DARPA Subterranean Challenge
Authors:
Tomáš Rouček,
Martin Pecka,
Petr Čížek,
Tomáš Petříček,
Jan Bayer,
Vojtěch Šalanský,
Teymur Azayev,
Daniel Heřt,
Matěj Petrlík,
Tomáš Báča,
Vojtěch Spurný,
Vít Krátký,
Pavel Petráček,
Dominic Baril,
Maxime Vaidis,
Vladimír Kubelka,
François Pomerleau,
Jan Faigl,
Karel Zimmermann,
Martin Saska,
Tomáš Svoboda,
Tomáš Krajník
Abstract:
We present a field report of CTU-CRAS-NORLAB team from the Subterranean Challenge (SubT) organised by the Defense Advanced Research Projects Agency (DARPA). The contest seeks to advance technologies that would improve the safety and efficiency of search-and-rescue operations in GPS-denied environments. During the contest rounds, teams of mobile robots have to find specific objects while operating…
▽ More
We present a field report of CTU-CRAS-NORLAB team from the Subterranean Challenge (SubT) organised by the Defense Advanced Research Projects Agency (DARPA). The contest seeks to advance technologies that would improve the safety and efficiency of search-and-rescue operations in GPS-denied environments. During the contest rounds, teams of mobile robots have to find specific objects while operating in environments with limited radio communication, e.g. mining tunnels, underground stations or natural caverns. We present a heterogeneous exploration robotic system of the CTU-CRAS-NORLAB team, which achieved the third rank at the SubT Tunnel and Urban Circuit rounds and surpassed the performance of all other non-DARPA-funded teams. The field report describes the team's hardware, sensors, algorithms and strategies, and discusses the lessons learned by participating at the DARPA SubT contest.
△ Less
Submitted 12 October, 2021;
originally announced October 2021.
-
Linked visualisations via Galois dependencies
Authors:
Roly Perera,
Minh Nguyen,
Tomas Petricek,
Meng Wang
Abstract:
We present new language-based dynamic analysis techniques for linking visualisations and other structured outputs to data in a fine-grained way, allowing a user to interactively explore how data attributes map to visual or other output elements by selecting (focusing on) substructures of interest. This can help both programmers and end-users understand how data sources and complex outputs are rela…
▽ More
We present new language-based dynamic analysis techniques for linking visualisations and other structured outputs to data in a fine-grained way, allowing a user to interactively explore how data attributes map to visual or other output elements by selecting (focusing on) substructures of interest. This can help both programmers and end-users understand how data sources and complex outputs are related, which can be a challenge even for someone with expert knowledge of the problem domain. Our approach builds on bidirectional program slicing techiques based on Galois connections, which provide desirable round-trip** properties.
Unlike the prior work in program slicing, our approach allows selections to be negated. In a setting with negation, the bidirectional analysis has a De Morgan dual, which can be used to link different outputs generated from the same input. This offers a principled language-based foundation for a popular interactive visualisation feature called brushing and linking where selections in one chart automatically select corresponding elements in another related chart. Although such view coordination features are valuable comprehension aids, they tend be to hard-coded into specific applications or libraries, or require programmer effort.
△ Less
Submitted 1 September, 2021;
originally announced September 2021.
-
Foundations of a live data exploration environment
Authors:
Tomas Petricek
Abstract:
Context: A growing amount of code is written to explore and analyze data, often by data analysts who do not have a traditional background in programming, for example by journalists.
Inquiry: The way such data anlysts write code is different from the way software engineers do so. They use few abstractions, work interactively and rely heavily on external libraries. We aim to capture this way of wo…
▽ More
Context: A growing amount of code is written to explore and analyze data, often by data analysts who do not have a traditional background in programming, for example by journalists.
Inquiry: The way such data anlysts write code is different from the way software engineers do so. They use few abstractions, work interactively and rely heavily on external libraries. We aim to capture this way of working and build a programming environment that makes data exploration easier by providing instant live feedback.
Approach: We combine theoretical and applied approach. We present the \emph{data exploration calculus}, a formal language that captures the structure of code written by data analysts. We then implement a data exploration environment that evaluates code instantly during editing and shows previews of the results.
Knowledge: We formally describe an algorithm for providing instant previews for the data exploration calculus that allows the user to modify code in an unrestricted way in a text editor. Supporting interactive editing is tricky as any edit can change the structure of code and fully recomputing the output would be too expensive.
Grounding: We prove that our algorithm is correct and that it reuses previous results when updating previews after a number of common code edit operations. We also illustrate the practicality of our approach with an empirical evaluation and a case study.
Importance: As data analysis becomes an ever more important use of programming, research on programming languages and tools needs to consider new kinds of programming workflows appropriate for those domains and conceive new kinds of tools that can support them. The present paper is one step in this important direction.
△ Less
Submitted 14 February, 2020;
originally announced February 2020.
-
What we talk about when we talk about monads
Authors:
Tomas Petricek
Abstract:
Computer science provides an in-depth understanding of technical aspects of programming concepts, but if we want to understand how programming concepts evolve, how programmers think and talk about them and how they are used in practice, we need to consider a broader perspective that includes historical, philosophical and cognitive aspects. In this paper, we develop such broader understanding of mo…
▽ More
Computer science provides an in-depth understanding of technical aspects of programming concepts, but if we want to understand how programming concepts evolve, how programmers think and talk about them and how they are used in practice, we need to consider a broader perspective that includes historical, philosophical and cognitive aspects. In this paper, we develop such broader understanding of monads, a programming concept that has an infamous formal definition, syntactic support in several programming languages and a reputation for being elegant and powerful, but also intimidating and difficult to grasp. This paper is not a monad tutorial. It will not tell you what a monad is. Instead, it helps you understand how computer scientists and programmers talk about monads and why they do so. To answer these questions, we review the history of monads in the context of programming and study the development through the perspectives of philosophy of science, philosophy of mathematics and cognitive sciences. More generally, we present a framework for understanding programming concepts that considers them at three levels: formal, metaphorical and implementation. We base such observations on established results about the scientific method and mathematical entities -- cognitive sciences suggest that the metaphors used when thinking about monads are more important than widely accepted, while philosophy of science explains how the research paradigm from which monads originate influences and restricts their use. Finally, we provide evidence for why a broader philosophical, sociological look at programming concepts should be of interest for programmers. It lets us understand programming concepts better and, fundamentally, choose more appropriate abstractions as illustrated in number of case studies that conclude the paper.
△ Less
Submitted 27 March, 2018;
originally announced March 2018.
-
Learning for Active 3D Map**
Authors:
Karel Zimmermann,
Tomas Petricek,
Vojtech Salansky,
Tomas Svoboda
Abstract:
We propose an active 3D map** method for depth sensors, which allow individual control of depth-measuring rays, such as the newly emerging solid-state lidars. The method simultaneously (i) learns to reconstruct a dense 3D occupancy map from sparse depth measurements, and (ii) optimizes the reactive control of depth-measuring rays. To make the first step towards the online control optimization, w…
▽ More
We propose an active 3D map** method for depth sensors, which allow individual control of depth-measuring rays, such as the newly emerging solid-state lidars. The method simultaneously (i) learns to reconstruct a dense 3D occupancy map from sparse depth measurements, and (ii) optimizes the reactive control of depth-measuring rays. To make the first step towards the online control optimization, we propose a fast prioritized greedy algorithm, which needs to update its cost function in only a small fraction of pos- sible rays. The approximation ratio of the greedy algorithm is derived. An experimental evaluation on the subset of the KITTI dataset demonstrates significant improve- ment in the 3D map accuracy when learning-to-reconstruct from sparse measurements is coupled with the optimization of depth-measuring rays.
△ Less
Submitted 7 August, 2017;
originally announced August 2017.
-
Miscomputation in software: Learning to live with errors
Authors:
Tomas Petricek
Abstract:
Computer programs do not always work as expected. In fact, ominous warnings about the desperate state of the software industry continue to be released with almost ritualistic regularity. In this paper, we look at the 60 years history of programming and at the different practical methods that software community developed to live with programming errors. We do so by observing a class of students d…
▽ More
Computer programs do not always work as expected. In fact, ominous warnings about the desperate state of the software industry continue to be released with almost ritualistic regularity. In this paper, we look at the 60 years history of programming and at the different practical methods that software community developed to live with programming errors. We do so by observing a class of students discussing different approaches to programming errors. While learning about the different methods for dealing with errors, we uncover basic assumptions that proponents of different paradigms follow. We learn about the mathematical attempt to eliminate errors through formal methods, scientific method based on testing, a way of building reliable systems through engineering methods, as well as an artistic approach to live coding that accepts errors as a creative inspiration. This way, we can explore the differences and similarities among the different paradigms. By inviting proponents of different methods into a single discussion, we hope to open potential for new thinking about errors. When should we use which of the approaches? And what can software development learn from mathematics, science, engineering and art? When programming or studying programming, we are often enclosed in small communities and we take our basic assumptions for granted. Through the discussion in this paper, we attempt to map the large and rich space of programming ideas and provide reference points for exploring, perhaps foreign, ideas that can challenge some of our assumptions.
△ Less
Submitted 31 March, 2017;
originally announced March 2017.
-
Types from data: Making structured data first-class citizens in F#
Authors:
Tomas Petricek,
Gustavo Guerra,
Don Syme
Abstract:
Most modern applications interact with external services and access data in structured formats such as XML, JSON and CSV. Static type systems do not understand such formats, often making data access more cumbersome. Should we give up and leave the messy world of external data to dynamic ty** and runtime checks? Of course, not!
We present F# Data, a library that integrates external structured d…
▽ More
Most modern applications interact with external services and access data in structured formats such as XML, JSON and CSV. Static type systems do not understand such formats, often making data access more cumbersome. Should we give up and leave the messy world of external data to dynamic ty** and runtime checks? Of course, not!
We present F# Data, a library that integrates external structured data into F#. As most real-world data does not come with an explicit schema, we develop a shape inference algorithm that infers a shape from representative sample documents. We then integrate the inferred shape into the F# type system using type providers. We formalize the process and prove a relative type soundness theorem.
Our library significantly reduces the amount of data access code and it provides additional safety guarantees when contrasted with the widely used weakly typed techniques.
△ Less
Submitted 10 May, 2016;
originally announced May 2016.
-
In the Age of Web: Typed Functional-First Programming Revisited
Authors:
Tomas Petricek,
Don Syme,
Zach Bray
Abstract:
Most programming languages were designed before the age of web. This matters because the web changes many assumptions that typed functional language designers take for granted. For example, programs do not run in a closed world, but must instead interact with (changing and likely unreliable) services and data sources, communication is often asynchronous or event-driven, and programs need to intero…
▽ More
Most programming languages were designed before the age of web. This matters because the web changes many assumptions that typed functional language designers take for granted. For example, programs do not run in a closed world, but must instead interact with (changing and likely unreliable) services and data sources, communication is often asynchronous or event-driven, and programs need to interoperate with untyped environments.
In this paper, we present how the F# language and libraries face the challenges posed by the web. Technically, this comprises using type providers for integration with external information sources and for integration with untyped programming environments, using lightweight meta-programming for targeting JavaScript and computation expressions for writing asynchronous code.
In this inquiry, the holistic perspective is more important than each of the features in isolation. We use a practical case study as a starting point and look at how F# language and libraries approach the challenges posed by the web. The specific lessons learned are perhaps less interesting than our attempt to uncover hidden assumptions that no longer hold in the age of web.
△ Less
Submitted 6 December, 2015;
originally announced December 2015.
-
The semantic marriage of monads and effects
Authors:
Dominic Orchard,
Tomas Petricek,
Alan Mycroft
Abstract:
Wadler and Thiemann unified type-and-effect systems with monadic semantics via a syntactic correspondence and soundness results with respect to an operational semantics. They conjecture that a general, "coherent" denotational semantics can be given to unify effect systems with a monadic-style semantics. We provide such a semantics based on the novel structure of an indexed monad, which we introduc…
▽ More
Wadler and Thiemann unified type-and-effect systems with monadic semantics via a syntactic correspondence and soundness results with respect to an operational semantics. They conjecture that a general, "coherent" denotational semantics can be given to unify effect systems with a monadic-style semantics. We provide such a semantics based on the novel structure of an indexed monad, which we introduce. We redefine the semantics of Moggi's computational lambda-calculus in terms of (strong) indexed monads which gives a one-to-one correspondence between indices of the denotations and the effect annotations of traditional effect systems. Dually, this approach yields indexed comonads which gives a unified semantics and effect system to contextual notions of effect (called coeffects), which we have previously described.
△ Less
Submitted 21 January, 2014;
originally announced January 2014.
-
Evaluation strategies for monadic computations
Authors:
Tomas Petricek
Abstract:
Monads have become a powerful tool for structuring effectful computations in functional programming, because they make the order of effects explicit. When translating pure code to a monadic version, we need to specify evaluation order explicitly. Two standard translations give call-by-value and call-by-name semantics. The resulting programs have different structure and types, which makes revisitin…
▽ More
Monads have become a powerful tool for structuring effectful computations in functional programming, because they make the order of effects explicit. When translating pure code to a monadic version, we need to specify evaluation order explicitly. Two standard translations give call-by-value and call-by-name semantics. The resulting programs have different structure and types, which makes revisiting the choice difficult.
In this paper, we translate pure code to monadic using an additional operation malias that abstracts out the evaluation strategy. The malias operation is based on computational comonads; we use a categorical framework to specify the laws that are required to hold about the operation.
For any monad, we show implementations of malias that give call-by-value and call-by-name semantics. Although we do not give call-by-need semantics for all monads, we show how to turn certain monads into an extended monad with call-by-need semantics, which partly answers an open question. Moreover, using our unified translation, it is possible to change the evaluation strategy of functional code translated to the monadic form without changing its structure or types.
△ Less
Submitted 13 February, 2012;
originally announced February 2012.
