Typelevel Summit Philadelphia

Keynote: Shared Session Types for Safe, Practical Concurrency

at 9:00

Message-passing concurrency abstracts over the details of how programs are compiled to machine instructions and has been adopted by various practical languages, such as Erlang, Go, and Rust. For example, Mozilla's Servo, a next-generation browser engine being written in Rust, exploits message-passing concurrency to parallelize loading and rendering of webpage elements, done sequentially in existing web browsers. Messages are exchanged along channels, which are typed with enumeration types. Whereas typing ensures in this setting that only messages of the appropriate type are communicated along channels, it fails to guarantee adherence to the intended protocol of message exchange.

In this talk I show how session types can be used to type communication channels to check protocol adherence at compile-time. Session types were conceived in the context of process calculi, but made their ways into various practical languages using libraries. A key restriction of prior session type work is linearity. Whereas linear session types enjoy strong properties such as race freedom, protocol adherence, and deadlock-freedom, their insistance on a single client rules out common programing scenarios, such as multi-producer-consumer queues or shared databases or output devices. I report on my work on shared session types, which accommodates those programing scenarios, while upholding the guarantees of linear session types. First, I introduce manifest sharing, a discipline in which linear and shared sessions coexist, but the type system ensures that clients of shared sessions run in mutual exclusion from each other. Manifest sharing guarantees race freedom and protocol adherence, but permits deadlocks. Next, I introduce manifest deadlock freedom, which makes shared and linear sessions deadlock-free by construction. Finally, I give an overview of my current and future research plans.

About Speaker

Stephanie Balzer is a research faculty in the Principles of Programming group in the Computer Science Department at Carnegie Mellon University. Stephanie obtained her PhD from ETH Zurich under the supervision of Thomas R. Gross. In her PhD work, Stephanie developed the object-based programming language Rumer, which uses the abstraction of a relationship to make explicit the collaborations between objects, rather than representing them implicitly in terms of references. Stephanie demonstrated the benefits of relationships for program verification, by developing an invariant-based, visible-state semantics verification technique for Rumer. During her postdoc, Stephanie enriched her expertise with a more theoretical approach to programming language research based on type theory and logic, which resulted in her work on manifest sharing and manifest deadlock freedom.

Systematic Software with Scala

at 10:10

Scala is a very flexible language, and this flexibility can make it difficult to know how to effectively design Scala code. In the nearly ten years I've been using Scala, my approach to using the language has coalesced around a ten or so strategies, which are similar to OO design patterns but broader in scope and borrow many ideas from functional programming. Using these strategies I can create code in a systematic and repeatable way. In this talk I will present the majority of my strategies, and illustrate their use by live coding a simple graphics system where the majority of the code is systematically derived by applying strategies. The strategies allow me to work at a higher-level of abstraction, and the coding itself becomes formulaic. This means I can get more work done and my code is simpler to read and use. I hope that my strategies will also enable you to design better code in Scala.

About Speaker

Adam Rosien is a Principal at Inner Product, focused on building systems using functional programming. He previously helped various startups in many domains develop back-end systems and implement continuous deployment practices, and also spent five years as a developer at Xerox PARC.

Journey to an FP Test Harness

at 10:45

The hardest part of the pure-FP journey for many people is taking that first real step. Even after you’ve read all the books and done all the exercises, you need to start committing real code to truly grok the FP mindset.

This little case study will trace my journey over that line, in building a new test harness to an existing Play application. In the course of it, we’ll explore how my assumptions evolved:

• From stateful members to consistent use of StateT;
• From Play’s native Future-centricity to IO;
• Becoming a little more nuanced about test state using IndexedStateT;
• Moving away from an ever-growing cake to focus on imports instead;
• And the payoff, being able to refactor the test code to be modular, readable and robust.

The goal here is to show that, while there are a bunch of parts, none of this is rocket science. In the end, the resulting code is delightfully elegant, and the general approach should work for many Play applications.

About Speaker

I’m a second-generation programmer, starting out on my father’s PDP-8 back in the mid-70s, and I’ve been a language geek ever since, working professionally in everything from LISP to Ada to assembly to C# to JavaScript to C++ to (heaven help me) COBOL, and pretty much everything in between. I picked up Scala back in 2007 (after trying to build a company in Java and winding up in a rage over its limitations); I’ve been working in Scala full-time since 2012. I’ve been doing “light FP” since picking up the style from Ruby around 2002, but am just now getting into the pure stuff. During the day, I work at Artima, doing Scala training and consulting and helping with ScalaTest. In my spare time, I’m the CEO and Architect of Querki, a wiki/database hybrid designed to make it easier for individuals and communities to manage and collaborate on their data.

The Monoiad: an epic poem on monoids

at 11:35

Monoids provide a vast landscape of concepts that we rely on in FP. Applicatives, monads, categories – all of them are monoids, as is much else. The epic takes us on a journey with this fundamental structure. We’ll move between everyday Scala, some niche areas of the language, and category theory.

About Speaker

Greg Pfeil is a compiler writer and programming language designer. At this point they have written four recursion scheme libraries in three languages, with the goal of getting to half a recursion scheme library for all languages. Greg works at Formation, writing Haskell, using only the purest artisanal FP.

Keynote: Higher Inductive Types in Homotopy Type Theory

at 13:45

Homotopy type theory is a new field of mathematics based on the recently-discovered correspondence between constructive type theory and abstract homotopy theory. Higher inductive types, which form a crucial part of this new system, generalize ordinary inductive types such as the natural numbers to higher dimensions. We will look at a few different examples of higher inductive types such as the integers, circles, and the torus, and indicate how we can use their associated induction principles to reason about them, e.g., to prove that the torus is equivalent to the product of two circles.

About Speaker

Kristina Sojakova is a postdoctoral researcher at Cornell University working with Greg Morrisett on the verification of cryptographic protocols. She received her PhD in 2016 from Carnegie Mellon University, where she worked on homotopy type theory, developing a universal mapping characterization of higher inductive types.

Telling the Truth with Types

at 14:55

There are many problems one faces when building effective solutions.

1. Outlining proper behavior, such that desired outcomes are achieved.
2. Simplifying the problem space, such that solutions are extensible and maintainable.
3. Interfacing with existing code.

Together we will walk through typical problems, and apply a set of processes to more effectively meet these criteria. We will identify what information we need to make available and how we can consume that information to build out systems which behave as we expect. We will use the type system as our guide, to lift our reasoning directly into our codebases.

Whether you are just starting out, or an experienced functional programmer this talk will deliver a set of tools to approach the next set of challenges.

About Speaker

Chris is a Senior Software Engineer at Banno. He is a firm advocate of Functional Programming. He maintains http4s and cats-effect libraries and contributes regularly to the Open Source Community.

Composable concurrency with Ref + Deferred

at 15:30

fs2 offers a very powerful and composable set of concurrent combinators and data structures, which are all built out of two deceptively simple primitives: Ref and Deferred.

This talk will explain what they are, the design principles behind them, and how to use them to build your own business logic abstractions. In the process, we will discover a general pattern in the form of concurrent state machines, and see how it integrates with final tagless on one hand, and streaming control flow on the other.

If you have ever wondered how to translate that complicated piece of actor logic in pure FP, or how fs2’s Queues, Topics and Signals work under the hood, this is the talk for you.

About Speaker

I'm a Principal Software Engineer at Ovo Energy in London, specialised in distributed systems and purely functional programming. I'm also an Open Source author and speaker as SystemFw: I'm one of the maintainers of fs2, cats-effect and http4s, and a contributor to cats, shapeless and several other libraries in the Scala FP ecosystem. Passionate about learning and teaching.

Extending your HTTP library with monad transformers

at 16:20

A tour of monad transformers and how stacking various effects onto IO can extend our HTTP library in new and interesting ways. We’ll review OptionT from last year’s talk, derive something akka-http like with EitherT, and demonstrating tracing with TraceT.

About Speaker

Ross is a Senior Software Engineer at Takt. He began his open source journey on the Scalatra project in 2009, and has gotten purer, more functional, and more typeful with each passing year. He now contributes to http4s and cats among others, and is a member of Typelevel. He is a co-organizer of IndyScala.

Portable, type-fancy multidimensional arrays

at 16:55

Zarr is a multidimensional-array container format that's gaining momentum in several scientific domains. It hails from the Python world, and primarily caters to numpy- and xarray-wielding scientists. It shines as a more remote- and parallel-processing-friendly HDF5 replacement. I implemented the Zarr spec in portable Scala, leveraging dependent- and higher-kinded-types. The resulting arrays have a unique type-safety profile. In this talk I'll: contextualize Zarr's use in the single-cell-sequencing domain, examine the freewheeling DSLs that scientific-Python exposes for array processing (including remote and distributed), discuss possibilities for Scala (and types!) to make inroads in these ecosystems, and show what worked well and poorly about my attempt.

About Speaker

Ryan develops software for analyzing genome- and single-cell-sequencing data at the Icahn School of Medicine at Mount Sinai Hospital in NYC. He has been pushing a snowball of increasingly portable, typelevel, and FP Scala OSS libraries for several years, from dependency-management and testing DSLs to collections algorithms for Spark RDDs and genomic-analysis tools.