Ronald Garcia

Although Abstracting Gradual Typing provides a systematic approach to design gradual languages, the original framework has limitations: first, it accepts design choices that lead to type inconsistencies sneaking through evaluation. Second, when a type inconsistency is identified at run time, evaluation halts without providing any feedback on the parts of the program related to the failure, a safe approach yet unhelpful for debugging.This dissertation addresses these two limitations of the Abstracting Gradual Typing framework. For the first limitation, I impose an extra constraint on the acceptable designs for gradual types: forward completeness of every type operation. This stricter constraint guarantees that, throughout evaluation, gradual types and runtime evidence objects cannot lose precision and will only represent information consistent with the original static type system. I introduce a new design for a gradual language with record subtyping that fulfills this restriction. For the second limitation, I provide a specification for runtime program slicing that can be systematically applied to languages designed using Abstracting Gradual Typing. Slicing can separate the portions of a program that are guaranteed to be uninvolved in a runtime failure. Unlike the standard blame approach, slicing does not assume that types are correct. The slicing semantics can be used to provide a debugging tool, and I apply empirical research methods to explore whether this runtime type slicing approach is useful to developers.

View record

Today, most programmers are not professional software developers, but end-users with limited training and experience in programming. End-user-friendly programming languages and tools aim to support this type of user, and many use visual programming aids to do so. Block-based programming is a popular visual programming style that has been effectively used in computer science education and is the foundation for many modern end-user programming tools. Because of the popularity of block-based programming, language designers can use a rich set of existing technologies that save them the effort of creating visual programming designs from scratch. However, many language designers ignore that block-based programming was created with learners in mind, who have different needs than end-users. Especially when programs grow in size and complexity, blocks offer little support to help end-users understand and edit programs effectively. In our work, we augment block-based programming with visual features that extend the range of programs that end-users can comprehend and write. In particular, we create languages and environments for the domain of robotics programming that allow end-users to write larger and more expressive programs. We focus on three scenarios that represent challenges that end-users face in this domain: coordinating multiple robots that work in tandem, writing large programs that span several workstations in different locations, and reacting to external signals such as machines or user interactions. For each environment, we first discuss the limitations of existing work in the areas of block-based and end-user programming. We present and discuss the design of our visual extensions with the goal to maintain end-user-friendliness. Finally, we evaluate our work through empirical studies, both formative to inform our designs and summative to demonstrate their benefits. Our designs, and the empirical and analytical process that we applied to create them, both contribute to a stronger understanding of how to build end-user-centric tools. We further believe that although our work focuses on the domain of robotics, these contributions transfer to other areas of end-user programming as well.

View record

Dependently typed programming languages provide a way to write programs, specifications, and correctness proofs using a single language. If a dependent type checker accepts a program, the programmer can be assured that it behaves according to the specification given in its types. However, dependently typed programming languages can be hard to use.Gradual types provide a way to mix dynamically and statically typed code in a single language. Under this paradigm, programs may have imprecise types, causing certain type checks to be deferred to run time.We build the theoretical foundations for combining gradual and dependent types in a programming language, with the aim of making dependent types easier to use. The differences between these two paradigms lead to inherent tensions when choosing the properties such a language should satisfy. Gradual typing's effectful nature conflicts with the compile-time reductions of dependent type checking. Gradual run-time type comparisons clash with dependent types containing terms that bind variables. This dissertation identifies such tensions and proposes a design that finds balance between the conflicting goals.Our contribution has three parts:First, we present a foundational calculus for gradual dependent types, with functions, function types and universes. To ensure that type checking terminates, we reduce compile-time terms with approximate normalization, producing imprecise results when the available type information cannot guarantee termination. We use hereditary substitution to show that approximate normalization always terminates.Second, we present a notion of propositional equality for gradual dependent types. We devise a method of tracking run-time consistency information between imprecise equated terms, and introduce a composition operator in the language itself.Third, we show that the first and second contributions can be combined, giving a language with approximate normalization that supports inductive types and propositional equality with dynamic consistency tracking. Since hereditary substitution does not scale to inductive types, we use a syntactic model to establish termination. The same technique is used to model non-terminating run-time semantics using guarded type theory, paving the road for mechanizing the metatheory of gradual dependent types.

View record