C◦mp◦se 2017 Speakers

Dr. Emily Riehl

[KEYNOTE] A categorical view of computational effects

Monads have famously been used to model computational effects, although, curiously, the computer science literature presents them in a form that is scarcely recognizable to a category theorist — I’d say instead that a monad is just a monoid in the category of endofunctors, what’s the problem? ;) To a categorical eye, computational effects are modeled using the Kleisli category of a monad, a perspective which suggests another categorical tool that might be used to reason about computation. The Kleisli category is closely related to another device for categorical universal algebra called a Lawvere theory, which may be a more natural framework to model computation (an idea suggested by Gibbons, Hinze, Hyland, Plotkin, Power and certainly others). This talk will survey monads, Lawvere theories, and the relationships between them and illustrate the advantages and disadvantages of each framework through a variety of examples: lists, exceptions, side effects, input-output, probabilistic non-determinism, and continuations.

Joachim Breitner

Lock-step simulation is child’s play

When implementing a multi-player network game, programmers often choose to implement “lock step simulation with client prediction”, where each client independently calculates the global state of the game, and integrate the other player’s actions as soon as he learns about them, rewinding the state to when the action actually happened. This approach to networking is infamously hard to get right and in general requires great discipline from the game programmer to avoid the clients getting out of sync.

Not so with strongly typed pure functional programming

On the programming learning platform CodeWorld, even middle school create multi-player games, without having spend a single thought on these issues, and no matter what code they write, they end up with a working networked game.

In this talk I will explain the interface that CodeWorld provides for this purpose, and show how it pulls this off under the hood.

May 18, 02:30pm

Michael Chavinda

Android programming in Froid

This talk will introduce Froid, a library for writing Android applications in Frege, a pure, lazy, functional language in the spirit of Haskell. The initial part will be an introduction to Frege - similarities to and differences from Haskell, and Java FFI. The second part of the talk will explore the design philosophy of Froid in building an object-functional library. Finally, the last talk will demonstrate how to write Android applications using Froid.

May 19, 12:45pm

Barry Burd

Teaching Haskell

So far, we've failed to impress most imperative programmers with the beauty of functional programming. We write articles and do presentations, but developers resist. Can we do a better job of describing and promoting functional thinking?

As a professor of Computer Science, I had a special opportunity to study this question. In the spring of 2017, I taught Haskell to a class of 15 undergraduates at Drew University. Most of the students were comfortable with Python and Java, but they had no experience with functional programming (not even with lambdas in Java 8). During this semester-long course, I explored the hurdles students faced, discovered which topics they learned easily and which topics gave them the most trouble. I found ways to reach past their imperative prejudices and get them to think functionally. Some of my conclusions about teaching Haskell were no-brainers, but some others were surprises.

In this talk, I describe my experiences teaching pure functional programming (and, yes, even monads) to college students. When you hear about my efforts, you'll find new ways to explain functional programming to your peers.

May 19, 09:00am

Yaron Minsky

Data Driven UIs, Incrementally

Trading in financial markets is a data-driven affair, and as such, it requires applications that can efficiently filter, transform and present data to users in real time.

But there's a difficult problem at the heart of building such applications: finding a way of expressing the necessary transformations of the data in a way that is simultaneously easy to understand and efficient to execute over large streams of data.

This talk will show how we've approached this problem using Incremental, an OCaml library for constructing dynamic computations that update efficiently in response to changing data. We'll show how Incremental can be used throughout the application, from the servers providing the data to be visualized, to the JavaScript code that generates DOM nodes in the browser. We'll also discuss how these applications have driven us to develop ways of using efficiently diffable data structures to bridge the worlds of functional and incremental computing.

May 19, 01:15pm

Stephen Compall

Working with Monads in OCaml

As a Haskeller steeped in the adage “ML doesn’t support higher kinds”, learning OCaml, I was surprised to discover that monad-generic programming in OCaml can indeed be done with 100% safety, via modules and functors, and moreover is supported directly by the popular ‘Core’ library.

In this talk, I will show how to define monad instances and write monad-generic functions using the ‘Monad’ modules, and dig into how this works at all. Attendees should get a more concrete feel for the power of the ML module system, as well as a vision of how their Haskell programs might look in ML.

May 18, 04:30pm

Nikhil Barthwal

Implementing an Event-Driven Microservices Architecture in F#: A case study of Jet.com

Web services are typically stateless entities, that need to operate at scale at large. Functional paradigm can be used to model these web services work and offer several benefits like scalability, productivity, and correctness.

This talk describes how Jet.com implemented their Event-Driven Microservices using F#. It covers topics like their Microservices, Event-Sourcing, Kafka, Build & Deployment pipeline. The objective of the talk is show how to create a scalable & highly distributed web service in F#, and demonstrate how various characteristics of functional paradigm capture the behavior of such services architecture very naturally.

May 19, 10:15am

Tikhon Jelvis

The Probability Monad

Probability distributions form a monad, giving us a lightweight, surprisingly simple probabilistic language embedded in Haskell. We can write stochastic models as normal Haskell programs and then interpret them either exhaustively or by random sampling.

I'll give an in-depth explanation of how a simple discrete probability distribution monad works, along with real-world examples from my work on supply chain optimization at Target. This simple probability monad has been a great fit for the stochastic optimization problems we're facing at Target, where different solution methods require random sampling (simulation-based optimization) or the entire distribution (policy iteration, linear programming). As a bonus, this'll give you a brief primer on supply chain optimization.

I'll also talk about the very real performance shortcomings of this approach—which we've mostly managed to dodge at Target.

Finally, I'll introduce some recent research that defines a free-monad based distribution type that can take advantage of cutting-edge research on probabilistic programming. This approach lets us work with continuous distributions and Bayesian conditioning, and lets us deploy modern sampling and probabilistic inference algorithms with performance comparable to dedicated probabilistic programming languages like Anglican.

This talk primarily draws on two papers:

- 'Probabilistic Functional Programming in Haskell' by Martin Erwig and Steve Kollmansberger which describes the discrete probability monad
- 'Practical Probabilistic Programming with Monads' by Adam Scibior, Zoubin Ghahramani and Andrew D. Gordon which describes how to extend the basic monadic approach with modern probabilistic programming techniques

May 18, 01:45pm

David Rhodes

Learning F#: Case study with branch and bound

We use the branch and bound algorithm as a realistic, non-trivial example of a functional programming challenge. This talk ports the core algoritmfrom imperative style to functional form in F#. This creates some interesting choices and also opens opportunities for parallel processing. Unit and property-based testing is also included. Much of the material is elaborated at: http://www.opcoast.com/demos/fsharp/index.html

May 18, 03:15pm

Sebastien Mondet

Typed-Tagless Final Bioinformatics

At Compose 2015, we quickly mentioned an experiment of a high-level well-typed EDSL to describe complex bioinformatics pipelines. It is a component of the [Biokepi](https://github.com/hammerlab/biokepi) library. Its first implementation had grown to be our default API to describe workflows; it was based on a long GADT declaration that would get compiled to our workflow engine's “lower-level” API. This worked quite well but we hit a couple of fundamental issues: i) the compiler code grew to become difficult to manage (huge “match” statements, and type errors unwelcoming to beginners), ii) more importantly, the EDSL could not be extended by *users* of the library (although there were a few “hooks” to achieve some tasks).

Enter “Typed Tagless Final Interpreters”... In July 2015, Oleg Kiselov introduced the [Quel](https://bitbucket.org/knih/quel) project to the OCaml mailing-list. The idea is to use OCaml's module system, to provide typed EDSLs as module types and write compilers as modules matching the signature; “programs” and program transformations are then functors taking such an implementation as argument. The approach ensures that the EDSL is extensible.

We reimplemented our EDSL based on this approch, to significant success. The talk will walk through our implementation of Biokepi's EDSL while trying to be an introductory tutorial on typed-tagless approaches.

May 18, 01:00pm

Jennifer Paykin, Kenneth Foner, Antal Spector-Zabusky

`choose` Your Own Derivative

In event-driven programming, an event is a computation that will eventually produce a value. Selective choice is a mechanism that takes in a list of events, runs them all concurrently, and returns the value of the first event to terminate. This primitive appears throughout systems and concurrent programming, ranging from Unix system calls (`select`) to asynchronous programming libraries in Haskell and in OCaml Core. Despite their ubiquity, these primitives are typically restricted to taking a list of events that all produce values of the same type. In this talk, we describe a natural type-directed generalization of selective choice to arbitrary data structures, including those containing events of different types.

The crucial observation we make is that selecting one event out of a data structure is reminiscent of *zipping* into that data structure. Conor McBride defines zippers into arbitrary “regular” algebraic data types by means of a type-level operation that acts like the partial derivative from calculus. We extend this notion of derivative to support data types containing events, and show how to use these derivatives to give a type to our generalization of selective choice. We implement these ideas in Haskell using GHC’s support for dependent types and generic programming, and demonstrate the use of generalized selective choice with a variety of examples.

May 18, 10:30am

Hongbo Zhang

BuckleScript: Making functional programming accessible to JavaScript developers

JavaScript is one of the most popular programming languages and it has an extensive ecosystem of support. However, it can become very hard to maintain for large scale applications. There are already [hundreds of JS transpilers] (https://github.com/jashkenas/coffeescript/wiki/List-of-languages-that-compile-to-JS); however, BuckleScript, the OCaml to readable JS compiler, is different in many aspects, including:

1. Unlike GHCJS, Scala.js or JSOO, BuckleScript is focused on integration with the existing JS ecosystem. One OCaml module is transpiled to one ES6 module without name mangling. Calling OCaml from JS is a no-op, which is essential for the internal migration from existing JS apps to OCaml. BuckleScript also reuses NPM as the official package manager.

2. Unlike TypeScript or PureScript, it is not a new language, which means the existing OCaml ecosystem can be reused. For example, the BuckleScript compiler itself can either be compiled into native code for bare metal performance or JS in the browser for reach.

3. The BuckleScript compiler is well-engineered. In general, it only takes 10~80ms to compile a single file in a cold start, which is faster than any other known transpiler. However, it also produces well-optimized JS code and works well with existing JS module bundlers, like Rollup and webpack.

The BuckleScript compiler was open-sourced by Bloomberg in 2016. Given its complexity, it will take time to reach maturity; however, it already has gained some significant adoption in the broader JS community. For example, in a presentation at React Conference 2017, Facebook revealed that OCaml generated using BuckleScript powers 25% of messenger.com. It is also used by Google’s V8 team to cross-compile a WebAssembly interpreter into a JS library.

May 19, 11:00am

Martín Ceresa, Gustavo Grieco

QuickFuzz Testing for Fun and Profit

Fuzzing is a technique that involves testing programs using invalid or erroneous inputs. There are two ways of producing invalid inputs: mutational fuzzing involves taking valid inputs and altering them through randomization, producing erroneous or invalid inputs that are fed into the program; generational fuzzing (sometimes also known as grammar-based fuzzing) involves generating invalid inputs from a specification or model of a file format. Unfortunately for generational fuzzing, to write specifications for generational fuzzers is the most expensive part of the process because it requires a deep knowledge of the specific file-format or protocol.

In this talk, we present QuickFuzz, an open source tool for automatically generating inputs and fuzzing programs parsing several common types of files. It is the first fuzzer to use QuickCheck, a highly effective technique developed in the functional programming field to perform automatic testing. Additionally we integrated it with fuzzers like Radamsa, Honggfuzz and other bug-finding tools such as Valgrind and Address Sanitizer to focus our tool for vulnerability discovery.

Our tool relies on existing Haskell implementations of file-format-handling libraries found on Hackage and was effective in discovering issues in real-world implementations of browsers, image processing utilities and file compressors among others.

May 18, 04:00pm

Hezekiah Carty and Chris Donaher

Distrest - REST access to distributed services

Distrest (distributed REST) is a lightweight toolkit for distributed services with a core written in OCaml. Distrest provides a simple proxy and group of service libraries supporting data-agnostic, scalable services with minimal code and configuration boilerplate. It allows developers to focus on their domain by automating the distribution of RESTful calls across suites of potentially replicated services. We use Distrest in our malware processing pipeline to ingest, extract information from and store a growing training software corpus. The services support malware analysis and generate training data for software classification machine learning models. Distrest is useful across several problem domains including basic database CRUD and bulk binary data processing. Due to its general utility, we are open sourcing Distrest.

Our talk will cover the requirements that led to Distrest’s development, how Distrest works internally, and a few demonstrations of Distrest’s functionality.

May 19, 09:30am

Nikita Volkov

New Hasql - a simpler, safer and faster Postgres client

This talk will present the upcoming release of Hasql with a renovated and polished API, which makes mapping simpler and provides for more safety by introducing such features as compile-time checking of SQL. Hasql is already known as the fastest driver around, and it keeps getting optimised further. In this talk I will present a detailed introduction to the library, core ideas behind it and a tutorial on how to use it.

May 19, 03:30pm

Edmund Cape

Multiplying by 1 - an important form of computation and how it reveals distinctions between kleislis

This talk will explore the meaning of information and how the type signatures provide an effective way to assess where our design and design layers encode and generate new information. How quickly we can identify isomorphisms, the same information in a different shape, is clearly a source for simplifying our code, improved encapsulation and exploiting the benefits of our libraries. How products (components, factors, and), coproducts (examples of, lists, or), exponentials, the identity and constant functors can quickly be shuffled around to reveal isomorphisms, core idioms including when and where we can expect to have access to the constructor (e.g., functor does not have access to constructors a nor b; nor does f have access to that of the functor) and/or are essentially multiplying by 1 (e.g, 3 vs 3 * 1; same information, different shape).

Category theory and the isomorphic algebras explain what to expect working through the type system. Exploiting the benefits of clearly delineated computations that generate side-effects requires understanding how, if ever, the values in our multi-layered constructs depend on each other. A review of adjoints and how they relate to monads and functors (and functor's twin brothers applicative) will highlight distinctions between data structuring, computation and the kleisli's that can be manufactured with composition (f :: a -> b and the monad's unit (return)). Not until we identify kleislis that cannot pass through b are we actually relying on the interaction between the layers of our constructs to generate a unique feature that requires and impacts both m b simultaneously. Thinking through this distinction may be particularly useful in how to consider 'functions as values' (e.g., a fixed value as a function that points to the head of a list; or a value that depends on State).

May 19, 02:00pm

Enzo Alda, Monica Figuera, Juan Andrés Escalante, Richard Lares Mejías

Reactive Sheets: an intuitive approach to functional‑reactive computing

As the world experiences an exponential growth in the amount of generated real-time data, it is not surprising that reactive computing services, like AWS Lambda, as well as stream processing frameworks, like Apache Storm and Apache Kafka, are becoming increasingly popular. The IT world has been consistently shifting from a request-response paradigm to one of continuous data processing pipelines. Moreover, data rates, volumes, and latency requirements keep getting more stringent, as vendors compete to deliver a better consumer experience.

This talk will first provide some general insights about the theoretical foundations of functional programming, stream processing, and reactive computing. Then, after briefly mentioning some enabling technologies and popular technology stacks, which make possible to build advanced event processing pipelines, the talk will introduce a simple, yet powerful, approach for modeling reactive computations.

The presentation will conclude with a live demonstration of a Web-enabled functional reactive system, showcasing the use of higher order functions to perform real-time calculations and screen rendering transformations over high rate data streams.

May 18, 11:15am

Stuart Popejoy

Smart Contracts and Formal Verification with Z3 with Pact

We present Pact, a new open-source language for authoring smart contracts, built in Haskell. Smart contract languages like Ethereum’s Solidity have taken a maximalist approach to functionality, in no small part because the slow execution speed of public blockchains emphasizes “feature-rich” transactions that compose multiple invariants into a single transaction. Resulting logic is complex, brittle, and often incorrect. With Pact, a high-performance blockchain ensures that transactions can closely model business invariants, and “fail fast” on invalid cases or retry scenarios. Logic is constrained to Turing-incomplete (terminating) execution and single-assignment (immutable) variables. We discuss the unique hybrid of strict OLTP workload and limited key-value querying needed for blockchain applications, and how this informs Pact’s database model. We also discuss the influence of Bitcoin scripts on Pact’s design as well as its integration of public-key authorization schemes. We demonstrate various Pact smart contracts running both in a standalone interpreter as well as in the ScalableBFT blockchain. Finally, we give a demo of static analysis and verification using the Z3 theorem prover, and show the new development environment with a sample application.