Scottish Programming Languages Seminar

Abstract

Optimizing programs to run efficiently on modern parallel hardware is hard but crucial for many applications. The predominantly used imperative languages — like C or OpenCL — force the programmer to intertwine the code describing functionality and optimizations. This results in a portability nightmare that is particularly problematic given the accelerating trend towards specialized hardware devices to further increase efficiency.

Many emerging DSLs used in performance demanding domains such as deep learning or high-performance image processing attempt to simplify or even fully automate the optimization process. Using a high-level — often functional — language, programmers focus on describing functionality in a declarative way. In some systems such as Halide or TVM, a separate schedule specifies how the program should be optimized. Unfortunately, these schedules are not written in well-defined programming languages. Instead, they are implemented as a set of ad-hoc predefined APIs that the compiler writers have exposed.

In this talk, we show how to employ functional programming techniques to solve this challenge with elegance. We present two functional languages that work together — each addressing a separate concern. RISE is a functional language for expressing computations using well known functional data-parallel patterns. ELEVATE is a functional language for describing optimization strategies. A high-level RISE program is transformed into a low-level form using optimization strategies written in ELEVATE. From the rewritten low-level program high-performance parallel code is automatically generated. In contrast to existing high-performance domain-specific systems with scheduling APIs, in our approach programmers are not restricted to a set of built-in operations and optimizations but freely define their own computational patterns in RISE and optimization strategies in ELEVATE in a composable and reusable way. We show how our holistic functional approach achieves competitive performance with the state-of-the-art imperative systems Halide and TVM.

This talk is based on the functional pearl "Achieving High-Performance the Functional Way — A Functional Pearl on Expressing High-Performance Optimizations as Rewrite Strategies" to appear at ICFP 2020.

Abstract

There are two standard ways of specifying a type system for ML: an orthogonal presentation and a syntax-directed presentation. The former allows implicit generalisation and instantiation anywhere in a program, and is thus not syntax-directed. The latter fuses generalisation with let-bindings and instantiation with variables, and is thus non-orthogonal. By introducing explicit syntax for generalisation and instantiation, that is, semi-explicit polymorphism, we obtain a presentation of Explicit ML, a mild variant of ML, which is both orthogonal and syntax-directed. Moreover, we recover the usual implicit version of ML as syntactic sugar.

FreezeML is a small extension of ML providing first-class polymorphism and sound and complete type inference of principal types, whose typing rules are non-orthogonal. We show that Explicit ML extends naturally to Explicit FreezeML, an orthogonal presentation of an explicit variant of FreezeML. We recover the usual implicit version of FreezeML as syntactic sugar. Explicit FreezeML is a conservative extension of both Explicit ML and System F.

Abstract

We will present implementations of various automatic differentiation (AD) modes via effects and handlers. The underlying theory is still in progress.

Automatic differentiation's aim is to calculate the derivative of a program which uses mathematical functions. A natural class of functions to consider are smooth (infinitely differentiable) functions. Smooth functions form an algebraic (Lawvere) theory in the context of universal algebra. Algebraic theories are often at the base of denotational semantics for effects and handlers, and this observation leads to natural implementations of AD.

We implement forward mode, reverse mode, and checkpointed reverse mode in the Frank language. These modes can be nested (which is non-trivial in some systems). Their implementation as handlers also seems to enable useful equational reasoning.

Abstract

We present StarChild and Lazuli, two libraries which leverage refinement types to verify neural network, implemented in F* and Liquid Haskell. Refinement types are types augmented, or refined, with assertions about values of that type, e.g., “integers greater than five”, which are checked by an SMT solver. Crucially, these assertions are written in the language itself. A user of our library can refine the type of neural networks, e.g., “MNIST neural networks which are robust against adversarial attacks”, and expect F* to handle the verification of this claim for any specific network, without having to change the representation of the network, or even having to learn about SMT solvers.

Our initial experiments indicate that our approach could greatly reduce the burden of verifying neural networks. Unfortunately, they also show that SMT solvers do not scale to the sizes required for neural network verification.

Abstract

I will talk about a system that combines Dependent Types and Linear Types. As an application of this system, I will show how to transport Martin Hofmann's LFPL and Amortised Resource analysis systems for resource constrained computing to full dependent types. This results in a theory where unconstrained computations are allowed at the type level, but only polynominal time computations at the term level. The combined system now allows one to explore the world of propositions whose proofs are not only constructive, but also of restricted complexity.