LambdaConf
Interview with Jonathan Blow at LambdaConf 2024
updated
(Other resources) sacrideo.us/dyalog-tooling-resources-list-lambdaconf-talk-2020
Modern APL as a language is known to produce exceptionally high performance, high level code that is concise and scales in a variety of dimensions, including the human factors of time to market and time to iterate. However, many new users of APL struggle to make sense of the wide array of integrations and tooling support provided by the Dyalog ecosystem, and often feel lost about how to architect their systems, deploy them, and integrate their APL code into new and existing products. This talk addresses these confusions by providing straightforward guidance and best practices, as well as providing a clear roadmap to navigating the wide array of APL tooling and products available. These ideas are demonstrated through recently developed APL applications that are designed to not only deliver value to the APL community, but also to showcase design and architectural models and frameworks that can be used to simplify your APL deployments and improve the ease with which you can integrate APL with external software by reducing boilerplate and focusing on the core business value of the application instead of complex systems design. We will further connect these practices with the philosophical and theoretical elements of APL and how these principles drive our integration and architecture choices.
Wix has finally released to open-source its Kafka client SDK wrapper called Greyhound.
Completely re-written using the Scala functional library ZIO.
Greyhound harnesses ZIO's sophisticated async and concurrency features together with its easy composability to provide a superior experience to Kafka's own client SDKs.
It offers rich functionality including:
- Trivial setup of message processing parallelisation,
- Various fault tolerant retry policies (for consumers AND producers),
- Easy plug-ability of metrics publishing and context propagation and much more.
This talk will also show how Greyhound is used by Wix developers in more than 1000 event-driven microservices.
"Phantom types are a way to carry (possibly domain-specific) information in types.
Existential types are a way to hide information from places where those types are used.
This talk will develop a small application that:
- parses and validates user input
- uses phantom types to
- turn validated data into types that carry ""proofs"" of that validation
- call functions that require those proofs
- uses existential types to
- hide the state of pure computations from the IO layer that must pass that state
back into the pure layer later
- ensure the app can only make valid state transitions (a.k.a., ""type-aligned sequences"")
By the end of the talk you should understand the often used phrases
- ""make illegal values unrepresentable"" -- via phantom types
- ""enforce abstraction boundaries in the type system"" -- via existential types"
Software transactional memory (STM) is an abstraction analogous to database transactions used to build safe, composable, and modular code dealing with concurrency. Attendees of this workshop will learn how to use STM and its accompanying data structures (e.g., TMap and TQueue) by solving some of the well-known concurrency challenges. In addition to that, we'll dive into the library implementation details, and discuss the impact of STM on program semantics and performance.
github.com/jakubjanecek/lambdaconf2020-demo
Resources: github.com/avast/scala-server-toolkit
"The world of Scala is full of many options but it is very hard for new Scala developers or teams to know which path to choose. We were dealing with the very same issue with our teams at Avast so after many years of Scala development we codified our best practices into a ""toolbox"" called Scala Server Toolkit (github.com/avast/scala-server-toolkit). SST was designed to help with delivering backend microservices written in FP style more quickly and in unified way. It gives your application the necessary structure and leads you to proper tools such as effect data types (ZIO, Monix), resource safety, type safe configuration and composition. Overall you and your team should become more productive.
In this talk I will shortly introduce Scala Server Toolkit and explain why and how it was created. Then I will show you how to write a full-blown microservice using SST."
"Functional Programming (FP) is an emerging mainstream in the software development world. However, the success of FP has come not from programming languages, but frameworks. React - the dominant framework for building web apps today - emphasizes immutability and composing smaller functional components to build a UI. Spark emphasizes immutable data transformations and treats functions as first-class concepts (e.g., UDFs). In machine learning, research is moving towards higher-order derivatives with functional programming - such as Google JAX - because the defaults for FP are more flexible and expressive.
There are many more examples that you have likely encountered in some form. And while this could be seen as cause for celebration, something is off. Haskell, Scala, F#, OCAML, Clojure, and other beloved programming languages are still seen as niche in working environments. You can utilize functional programming concepts in your daily work, but not always in a functional language. There is no shortage of fascinating and useful concepts, libraries, and tools that occupy these languages' ecosystems, but they have all seen little adoption in the broader programming community.
This talk will cover the framing that was previously mentioned and offer hypotheses about how FP languages can rise in adoption without abandoning all the things that make them so great. Topics discussed include editor tooling, debuggers, profiling and analysis tools, scripting and visualization, library design, and library ecosystem focus. Every FP language has strengths in some areas over others, but all have objective deficiencies when compared to mainstream programming languages like Java, JavaScript, C++, C#, and so on. But not all is lost! There are some novel concepts, libraries, and tools in FP language ecosystems that could propel the use of FP languages if some deficiencies are addressed. This is the central proposition of this talk.
Attendees can walk away with ideas worth testing and, perhaps, advocating for. They can make measured arguments for adopting FP and FP languages in the workplace, addressing very real concerns about FP language deficiencies while advocating for novel solutions to problems they face. Advocacy can also be directed inwards, so that discussions about refocusing efforts with aims towards broader adoption can be had."
"Working with external APIs can be hard. As functional programmers we want to write our business logic with simple, composable functions. But that logic can result in actual execution of API calls that is highly inefficient, forcing us to make unpleasant trade-offs between design and performance.
In this talk Adam Fraser, the author of ZIO Query, will show how users can build a purely functional description of a computation using all the same combinators they are used to for functional effects, with operations that can potentially be executed in parallel automatically batched together and operations that must be performed sequentially automatically pipelined. Adam will show how ZIO Query takes advantage of Scala's type system to maintain type safety even when batching API calls returning different types. He will also discuss how this implementation helps us solve a variety of other problems when working with external data sources, including caching, deduplication, query metrics, logging, and pre-processing and post-processing of data.
Come learn how you can use the solution that is powering groundbreaking applications such as Caliban's GraphQL library to optimize your code!"
You can fold a list by converting its elements to monoidal values and then appending them together. The folding itself is agnostic of the monoid, so you can hide it inside an existential type. But folding is just a special case of a catamorphism. When you combine the two you get a monoidal catamorphism.
Machine learning and visualization operations typically require multiple transformations of input data. Entropy tends to increase with the number of transformations, expanding the likelihood of errant behavior that drains system resources and is challenging to identify because it is difficult to reproduce. Isomorpisms may be used to reduce the resources required and increase the explainability of transformations data undergo. We will discuss several examples, examining pragmatic and theoretical implications along the way. By the end you will have a better idea of how isomorphic operations may be used in your own code.
GitHub: github.com/morganthomas/streamly-test
We will look at and practice strategies for achieving fast, reliable concurrency in Haskell using Streamly streams, threads, TVars, MVars, STM containers, and ReaderT IO. Familiarity with Haskell is required and some familiarity with these concepts is helpful but not required.
Actors are one of the most popular concurrency models in nowadays software systems.
In this talk, Mateusz will present ZIO-Actors - a small, strongly typed actor library backed by ZIO.
He will explain library design, demonstrate its usage and point out the differences and similarities with Akka.
Many advocates of functional programming are frustrated that we haven't taken over the entire industry. It can be surprising to see (in our minds) inferior technologies regularly selected over the solid, maintainable, productive, and performant approaches provided by techniques like functional programming.I'd like to provide a bit of an outsider's view into how these decisions happen. I have been working in management instead of hands-on programming for years now, and have an extensive background in economics and finance. I believe many of these subpar technical decisions can be explained through factors that we, as programmers, rarely look at.Understanding these trade-offs will help programmers better advocate for good technologies, and understand when a worse technology may still be the better value for the business.
Part 1: youtu.be/xsk61FNEGmM
Part 3: youtu.be/Z7oU3Sh8MMg
In Asynchronous and Concurrent Programming with Scala, you will become an expert in using ZIO, a new library for building high-performance, leak-free Scala applications that are asynchronous and concurrent. The material you learn will be broadly applicable to other effect systems in Scala, as well as the Haskell Async package and concurrency model.
In this workshop, you will cultivate the following skills:
Asynchronous Programming. Writing non-blocking, asynchronous code, as easily as synchronous code.
Error Management. Detecting and responding to errors locally, without losing any errors; and using the Scala compiler to ensure the right errors are handled in the right places.
Resource-Safety. Building applications that never leak resources, including threads and fibers.
Thread Management. Keeping the right code executing in the right place, optimizing for throughput, minimizing blocked threads, and terminating unused computation.
Parallelism. Safely and trivially execute computations in parallel to minimize application latency, with automatic error propagation and early termination.
Concurrency. Build high-performance fiber-based concurrent code, and safely and trivially share data between fibers without races or deadlocks using Software Transactional Memory (STM); leverage asynchronous, concurrent, high-performance queues, streams, promises, and semaphores.
Testability. Test all code in fast, deterministic unit tests, which do not need to interact with external systems.
Interop. Interop with Future, the broader Cats Effect ecosystem, and all the standard data types in Scala.
By the end of the day, you will feel confident using ZIO either stand-alone or with Future or Cats Effect, and will have built your own application in a graduation project that ties together everything you learn in the workshop.
Part 1: youtu.be/xsk61FNEGmM
Part 2: youtu.be/SeBkLDRVZYI
In Asynchronous and Concurrent Programming with Scala, you will become an expert in using ZIO, a new library for building high-performance, leak-free Scala applications that are asynchronous and concurrent. The material you learn will be broadly applicable to other effect systems in Scala, as well as the Haskell Async package and concurrency model.
In this workshop, you will cultivate the following skills:
Asynchronous Programming. Writing non-blocking, asynchronous code, as easily as synchronous code.
Error Management. Detecting and responding to errors locally, without losing any errors; and using the Scala compiler to ensure the right errors are handled in the right places.
Resource-Safety. Building applications that never leak resources, including threads and fibers.
Thread Management. Keeping the right code executing in the right place, optimizing for throughput, minimizing blocked threads, and terminating unused computation.
Parallelism. Safely and trivially execute computations in parallel to minimize application latency, with automatic error propagation and early termination.
Concurrency. Build high-performance fiber-based concurrent code, and safely and trivially share data between fibers without races or deadlocks using Software Transactional Memory (STM); leverage asynchronous, concurrent, high-performance queues, streams, promises, and semaphores.
Testability. Test all code in fast, deterministic unit tests, which do not need to interact with external systems.
Interop. Interop with Future, the broader Cats Effect ecosystem, and all the standard data types in Scala.
By the end of the day, you will feel confident using ZIO either stand-alone or with Future or Cats Effect, and will have built your own application in a graduation project that ties together everything you learn in the workshop.
Part 1: youtu.be/xsk61FNEGmM
Part 2: youtu.be/SeBkLDRVZYI
Part 3: youtu.be/Z7oU3Sh8MMg
In Asynchronous and Concurrent Programming with Scala, you will become an expert in using ZIO, a new library for building high-performance, leak-free Scala applications that are asynchronous and concurrent. The material you learn will be broadly applicable to other effect systems in Scala, as well as the Haskell Async package and concurrency model.
In this workshop, you will cultivate the following skills:
Asynchronous Programming. Writing non-blocking, asynchronous code, as easily as synchronous code.
Error Management. Detecting and responding to errors locally, without losing any errors; and using the Scala compiler to ensure the right errors are handled in the right places.
Resource-Safety. Building applications that never leak resources, including threads and fibers.
Thread Management. Keeping the right code executing in the right place, optimizing for throughput, minimizing blocked threads, and terminating unused computation.
Parallelism. Safely and trivially execute computations in parallel to minimize application latency, with automatic error propagation and early termination.
Concurrency. Build high-performance fiber-based concurrent code, and safely and trivially share data between fibers without races or deadlocks using Software Transactional Memory (STM); leverage asynchronous, concurrent, high-performance queues, streams, promises, and semaphores.
Testability. Test all code in fast, deterministic unit tests, which do not need to interact with external systems.
Interop. Interop with Future, the broader Cats Effect ecosystem, and all the standard data types in Scala.
By the end of the day, you will feel confident using ZIO either stand-alone or with Future or Cats Effect, and will have built your own application in a graduation project that ties together everything you learn in the workshop.
Part 1: youtu.be/9Ty2nGZtPjg
Part 2: youtu.be/xgsVm2iIUek
Eta-lang is a GHC based Haskell implementation for the JVM. We will start from practical exercises showing how to combine Haskell with JVM languages. Then we will dig into details such as performance, jvm bytecode specifics (like JIT, GC) . Finally we will get into the eta compiler internals (fun!). At least two types of developers might be very interested in eta-lang:
- those that work with Haskell /GHC and want (or have to) port their solution to JVM,
- those that are familiar with JVM based languages (Scala/Kotlin/Java.. ) and want to learn/ try Haskell easier way, or possibly combine Haskell with existing code/libraries.
In the first part ("What is eta-lang") I will try to present eta-lang from both perspectives and give the practical hints:
- How to use existing Haskell code,
- How to mix both worlds.
There will be exercise (classical Conway's game of life)
In the second part ("Important details") I will concentrate on potential problems:
- GC impact,
- JVM/ JIT specifics,
- TCO and other optimizations,
- performance,
- profiling,
The goal of this part is to give attendees the possibility to evaluate eta in their projects.
JVM details should be also interesting for Scala, Kotlin, Clojure developers.
Exercise here will be a JVM benchmark based on JMH framework.
The last part ("Into the core") will be a show of eta compiler internals (partially applies to GHC/Haskell) :
- STG,
- Compiler Extensions,
- Bytecode generation,
Debugging and testing of the compiler.
This part should be also interesting for people interested in developing their own languages.
In this part we will try to resolve one of the issues from Eta-lang github (solution prepared before talk).
Part 1: youtu.be/9Ty2nGZtPjg
Part 3: youtu.be/y3aR3EcgmuQ
Eta-lang is a GHC based Haskell implementation for the JVM. We will start from practical exercises showing how to combine Haskell with JVM languages. Then we will dig into details such as performance, jvm bytecode specifics (like JIT, GC) . Finally we will get into the eta compiler internals (fun!). At least two types of developers might be very interested in eta-lang:
- those that work with Haskell /GHC and want (or have to) port their solution to JVM,
- those that are familiar with JVM based languages (Scala/Kotlin/Java.. ) and want to learn/ try Haskell easier way, or possibly combine Haskell with existing code/libraries.
In the first part ("What is eta-lang") I will try to present eta-lang from both perspectives and give the practical hints:
- How to use existing Haskell code,
- How to mix both worlds.
There will be exercise (classical Conway's game of life)
In the second part ("Important details") I will concentrate on potential problems:
- GC impact,
- JVM/ JIT specifics,
- TCO and other optimizations,
- performance,
- profiling,
The goal of this part is to give attendees the possibility to evaluate eta in their projects.
JVM details should be also interesting for Scala, Kotlin, Clojure developers.
Exercise here will be a JVM benchmark based on JMH framework.
The last part ("Into the core") will be a show of eta compiler internals (partially applies to GHC/Haskell) :
- STG,
- Compiler Extensions,
- Bytecode generation,
Debugging and testing of the compiler.
This part should be also interesting for people interested in developing their own languages.
In this part we will try to resolve one of the issues from Eta-lang github (solution prepared before talk).
Part 2: youtu.be/xgsVm2iIUek
Part 3: youtu.be/y3aR3EcgmuQ
Eta-lang is a GHC based Haskell implementation for the JVM. We will start from practical exercises showing how to combine Haskell with JVM languages. Then we will dig into details such as performance, jvm bytecode specifics (like JIT, GC) . Finally we will get into the eta compiler internals (fun!). At least two types of developers might be very interested in eta-lang:
- those that work with Haskell /GHC and want (or have to) port their solution to JVM,
- those that are familiar with JVM based languages (Scala/Kotlin/Java.. ) and want to learn/ try Haskell easier way, or possibly combine Haskell with existing code/libraries.
In the first part ("What is eta-lang") I will try to present eta-lang from both perspectives and give the practical hints:
- How to use existing Haskell code,
- How to mix both worlds.
There will be exercise (classical Conway's game of life)
In the second part ("Important details") I will concentrate on potential problems:
- GC impact,
- JVM/ JIT specifics,
- TCO and other optimizations,
- performance,
- profiling,
The goal of this part is to give attendees the possibility to evaluate eta in their projects.
JVM details should be also interesting for Scala, Kotlin, Clojure developers.
Exercise here will be a JVM benchmark based on JMH framework.
The last part ("Into the core") will be a show of eta compiler internals (partially applies to GHC/Haskell) :
- STG,
- Compiler Extensions,
- Bytecode generation,
Debugging and testing of the compiler.
This part should be also interesting for people interested in developing their own languages.
In this part we will try to resolve one of the issues from Eta-lang github (solution prepared before talk).
The influence of category theory on statically-typed functional programming is undeniable. The liberal usage of terms such as “functor” and “monad” seems to prove this point. Category theory is certainly a rich source of ideas, but one gets the impression that it is more than just that. Proficiency in category theory appears to enable software developers to explore new concepts and abstractions in a more far-reaching and systematic way.
On closer inspection, this should not come as a surprise. Category theory can be seen as being about defining concepts by their relationships to one another. Sometimes, this allows finding and exploring new ideas by just “following the arrows,” which is one of the many useful exploration techniques to be found in a category theorist’s toolbox.
In this talk, I will try to demonstrate some of these exploration techniques by developing and analyzing examples from the world of functional programming phrased in the language of category theory. We will see how this enables us to systematically tackle concepts by deconstructing them and deriving new ideas from them. That is, we will use category theory as a tool—a tool for thought.
TLA+ is a formal specification language developed by Leslie Lamport, designed to specify, model, document, and verify concurrent systems. It empowers your ability to clearly specify your design choices in the form of a formal specification, but also (even more importantly) can formally verify that your design choice is correct—meaning that it is both safe (does not break any rules) and live (over time it converges toward the result).
We will start with simple distributed algorithms and slowly move toward more complex ones. In each section, a bit of TLA+ notation will be introduced, followed by the description of the algorithm that we will specify. Lastly, we will run the model checker to look for potential errors in our design. Each section will end with an exercise. This will be an intensive six hours, but at the end of the day it will be hard not to notice that your core engineering skills will have improved significantly.
We will use well known distributed algorithms as examples (such as Two Phase Commit or Paxos), but the knowledge you gain can be applied to any of your daily routines. The objective of this workshop is to equip attendees with powerful tools that will allow them to better design their systems and have stronger guarantees it will be correct. Lastly, working with TLA+ will also allow you to think more abstractly about your system—and that is a value of its own.
*We regret that the later parts of this workshop are unavailable due to camera malfunction.
Part 1: youtu.be/ApHFidwNypE
Part 2: youtu.be/UScWv37aJhY
*We are aware of the sound issue for parts 2 and 3, but have chosen to leave the video as-is for you to follow along as desired.
Slides for this talk: github.com/cohomolo-gy/Isomorphic-Reasoning/blob/master/main.pdf.
Blog post by Alex that explains much of his portion: alexknvl.com/posts/counting-type-inhabitants.html
FP developers know that ∀ a. a → a has only one inhabitant, but how? Using the language of category theory (Yoneda, representable and Naperian functors, etc.), we can show that there is a secret type-level arithmetic embedded in languages that support parametric polymorphism, allowing us to reason about types and even manipulate them as you would basic arithmetic.
It is a common theme among developers beginning to study parametrically polymorphic type systems in functional programming that they come across blog posts or tutorials that make analogies between types and arithmetic in order to express how easy it is to reason about type signatures. Often, one will find algebraic data types (ADTs) expressed in terms of polynomials, coproducts in terms of addition, products in terms of multiplication, etc., applying seemingly magical arithmetic using this language to simplify and prove properties about the types. As often, these transformations are poorly motivated or cryptically taken to be axiomatic and soon forgotten as a curiosity of the type system. But there is more to these transformations than meets the eye.
In this talk, we will explain how one can reason about type signatures arithmetically and count the number of inhabitants of polymorphic types using a simple arithmetic derived from the language of category theory. From category theory, we will use the (Double, co-) Yoneda Lemma, representable, Naperian, and Container Functors, products, coproducts, initial and terminal objects, and nominal results surrounding these as points of study to build a theory, which we will call “Isomorphic Reasoning”– because that is really what it all comes down to: exploiting isomorphisms to achieve simple and elegant transformations that we are all familiar with. We will also discuss the fundamental topic of observational equality (identity of indiscernibles) and its relation to isomorphisms on types, and work our way towards parametricity and free theorems.
We will discuss System F, its type-level language and its encoding using de Brujin indices. Taking a short break from the theory, we will implement this type algebra in Haskell / Scala / Idris, together with a minimal parser & printer. By lifting our search from individual types to sequences of isomorphisms ending with types, we will be able to explicitly enumerate all of its inhabitants. We will talk about further improvements to the tool that we could add: support for functor fixpoints, double-negation translation, and System Fω.
Requirements
While we will cover a lot of advanced topics, we will attempt to explain things in the simplest possible terms. Basic knowledge of functional concepts will be assumed. Bring pen & paper as well as your laptop.
Part 1: youtu.be/ApHFidwNypE
Part 3: youtu.be/kKZTd7D33KY
*We are aware of the sound issue for parts 2 and 3, but have chosen to leave the video as-is for you to follow along as desired.
Slides for this talk: github.com/cohomolo-gy/Isomorphic-Reasoning/blob/master/main.pdf.
Blog post by Alex that explains much of his portion: alexknvl.com/posts/counting-type-inhabitants.html
FP developers know that ∀ a. a → a has only one inhabitant, but how? Using the language of category theory (Yoneda, representable and Naperian functors, etc.), we can show that there is a secret type-level arithmetic embedded in languages that support parametric polymorphism, allowing us to reason about types and even manipulate them as you would basic arithmetic.
It is a common theme among developers beginning to study parametrically polymorphic type systems in functional programming that they come across blog posts or tutorials that make analogies between types and arithmetic in order to express how easy it is to reason about type signatures. Often, one will find algebraic data types (ADTs) expressed in terms of polynomials, coproducts in terms of addition, products in terms of multiplication, etc., applying seemingly magical arithmetic using this language to simplify and prove properties about the types. As often, these transformations are poorly motivated or cryptically taken to be axiomatic and soon forgotten as a curiosity of the type system. But there is more to these transformations than meets the eye.
In this talk, we will explain how one can reason about type signatures arithmetically and count the number of inhabitants of polymorphic types using a simple arithmetic derived from the language of category theory. From category theory, we will use the (Double, co-) Yoneda Lemma, representable, Naperian, and Container Functors, products, coproducts, initial and terminal objects, and nominal results surrounding these as points of study to build a theory, which we will call “Isomorphic Reasoning”– because that is really what it all comes down to: exploiting isomorphisms to achieve simple and elegant transformations that we are all familiar with. We will also discuss the fundamental topic of observational equality (identity of indiscernibles) and its relation to isomorphisms on types, and work our way towards parametricity and free theorems.
We will discuss System F, its type-level language and its encoding using de Brujin indices. Taking a short break from the theory, we will implement this type algebra in Haskell / Scala / Idris, together with a minimal parser & printer. By lifting our search from individual types to sequences of isomorphisms ending with types, we will be able to explicitly enumerate all of its inhabitants. We will talk about further improvements to the tool that we could add: support for functor fixpoints, double-negation translation, and System Fω.
Requirements
While we will cover a lot of advanced topics, we will attempt to explain things in the simplest possible terms. Basic knowledge of functional concepts will be assumed. Bring pen & paper as well as your laptop.
Part 2: youtu.be/UScWv37aJhY
Part 3: youtu.be/kKZTd7D33KY
*We are aware of the sound issue for parts 2 and 3, but have chosen to leave the video as-is for you to follow along as desired.
Slides for this talk: github.com/cohomolo-gy/Isomorphic-Reasoning/blob/master/main.pdf.
Blog post by Alex that explains much of his portion: alexknvl.com/posts/counting-type-inhabitants.html
FP developers know that ∀ a. a → a has only one inhabitant, but how? Using the language of category theory (Yoneda, representable and Naperian functors, etc.), we can show that there is a secret type-level arithmetic embedded in languages that support parametric polymorphism, allowing us to reason about types and even manipulate them as you would basic arithmetic.
It is a common theme among developers beginning to study parametrically polymorphic type systems in functional programming that they come across blog posts or tutorials that make analogies between types and arithmetic in order to express how easy it is to reason about type signatures. Often, one will find algebraic data types (ADTs) expressed in terms of polynomials, coproducts in terms of addition, products in terms of multiplication, etc., applying seemingly magical arithmetic using this language to simplify and prove properties about the types. As often, these transformations are poorly motivated or cryptically taken to be axiomatic and soon forgotten as a curiosity of the type system. But there is more to these transformations than meets the eye.
In this talk, we will explain how one can reason about type signatures arithmetically and count the number of inhabitants of polymorphic types using a simple arithmetic derived from the language of category theory. From category theory, we will use the (Double, co-) Yoneda Lemma, representable, Naperian, and Container Functors, products, coproducts, initial and terminal objects, and nominal results surrounding these as points of study to build a theory, which we will call “Isomorphic Reasoning”– because that is really what it all comes down to: exploiting isomorphisms to achieve simple and elegant transformations that we are all familiar with. We will also discuss the fundamental topic of observational equality (identity of indiscernibles) and its relation to isomorphisms on types, and work our way towards parametricity and free theorems.
We will discuss System F, its type-level language and its encoding using de Brujin indices. Taking a short break from the theory, we will implement this type algebra in Haskell / Scala / Idris, together with a minimal parser & printer. By lifting our search from individual types to sequences of isomorphisms ending with types, we will be able to explicitly enumerate all of its inhabitants. We will talk about further improvements to the tool that we could add: support for functor fixpoints, double-negation translation, and System Fω.
Requirements
While we will cover a lot of advanced topics, we will attempt to explain things in the simplest possible terms. Basic knowledge of functional concepts will be assumed. Bring pen & paper as well as your laptop.
1. Given a parser written using finally tagless applicative parser combinators, produce an EBNF grammar and check if a particular non-terminal is nullable.
2. Given an expression in logical circuit DSL, simplify it and produce a final circuit schematic.
Both problems are tricky in a pure functional setting because referential transparency prohibits us from observing common subexpressions. But what if we are willing to go down the road of reference equality (of course guarded by the `IO` monad)? Turns out that then there is a very straightforward way to reify any recursive data structure into a graph *and* back. And once we have a graph representation, solving both problems is a piece of cake.
What is "algebra"? Why do people use this term both in the context of recursion schemes and finally tagless?
Are typeclasses like `Monoid a` algebras? In this talk I will derive the core ideas behind them from scratch, and connect all the dots. First, I will give you a short introduction to type algebra and isomorphisms. Most people in FP have an intuitive understanding of the topic, but it will be useful to refresh the memory.
Then we will take simple recursive data structures and explore various `fold`-like operations on them and how we can massage them into different forms using isomorphisms: finally tagless, recursion schemes, `foldMap`-like operations, and direct `foldr`-style.
We will talk about algebraic data types, `Recursive` typeclass, fixpoint data types, continuations, catamorphisms, F-algebras, initial algebras, and their categorical underpinnings. We will lightly touch on Lambek lemma.
The purpose of this talk is primarily to give you a solid intuition and understanding of these concepts and how they are connected to each other.
After achieving this on a machine I built, using a functional language (F#), I then reminisce about the players that made this odyssey possible by providing important contributions to computer science (and functional programming in particular). I also consider existential elements of their contributions: what must it have been like to pioneer the underpinnings that set the stage, when it must have been difficult to foresee (and justify to stakeholders) what their contributions would ultimately lead to.
I also look ahead and conjecture a bit on what I think is ahead.
Conseil (yes, from 20,000 Leagues Under the Sea) is a Scala platform that tackles this problem by abstracting away the technical specifics of interacting with any chain by storing the data in a database, and allowing users to create complex queries by exporting a simple REST API. However, an issue arises with this approach: Blockchains fork, so maintaining your database’s integrity and internal consistency is a nontrivial task.
In this talk, I will describe Lorre, a complementary module to Conseil that fetches blockchain data and writes to our database, and I will describe the algorithm we use to handle fork detection and database consistency checking, as well as the technical challenges that arose from this problem.
We often need to batch many operations together to optimize for performance or quotas, but our business logic makes this seemingly impossible. Let’s implement an interpreter that can rip apart monads and stitch them together again, batching intermediate steps across many monadic actions. You’ve integrated your application with an external API, great! But now you find yourself receiving many requests and are now hitting your usage quotas and getting throttled. You discover that there’s a batch API and decide to just use that. But as you start updating your code to use the batch API, you realize that your current business logic is making this impossible!
Our business logic is very monadic in nature (i.e. sequential, dependent actions) and as such, we aren’t able to know ahead of time which requests will need to be batched. What we need is a specialized runtime system which can handle such a problem.
While both free monad and free applicative exist, neither fully address our problem as we need sequential business logic (possible via monad) and batchability (possible via applicative). However, because our system is getting many requests, we can batch across those actions, evaluating many monads in parallel and batching their intermediate requests together. This requires writing an algebra that supports our monadic business logic, and applicative requests, and an interpreter that can evaluate that algebra, optimizing requests in batches to the fullest extent possible.
We’ll describe how to implement such an interpreter, reviewing along the way the limitations of free monad and free applicative, touching on some prerequisite concepts such as natural transformations and monoids, all while discussing a real world problem solved elegantly with pure functional programming.
What's the secret to success? Let’s explore the techniques you'll need to successfully lead your team into doing FP at work. How do you convert your shop into a Scala shop? What about turning your team into a Haskell team? Or perhaps an incremental change—introduce immutability to your C# shop?
Conventional thinking teaches us that a well-reasoned presentation of the facts is a fool-proof way to change people's minds. Wrong! If software engineers made decisions based on rational choices, everyone would be already writing Haskell.
What does it take? During this talk, you'll learn how to build your influence among your teammates, and lead your team to FP greatness.
As companies grow, and as teams become more distributed, it’s becoming more difficult to coordinate expectations across teams and companies. At every part of the process, from the initial inception of an idea all the way to being released as a new product, communication remains critical.
By using tools like OpenAPI (formerly Swagger) to document APIs, teams can collaborate through all stages of development, which is excellent. That being said, if the API specification isn’t brought into the build pipeline, there are no guarantees ensuring adherence to the proposed specification. This doesn’t just create rework, but in extreme cases, it’s the customer who discovers the mistake!
By generating principled code from the specification directly, we can leverage the typesystem to write better software.
If your documentation is wrong, your code doesn’t compile.
## Workshop Format
1. GraphQL core concepts overview
2. Elm GraphQL Overview
3. Making your first GraphQL query
4. Get it compiling, then get it right
5. Using your editor to help you build queries quickly
6. Combining fields together
6. Basics of modularizing queries - using Elm constructs instead of GraphQL Variables
7. Mapping into meaningful data structures
8. Pipelines versus map2, map3..., functions
## Highlight of `elm-graphql` Features
* Provides a high-level DSL for making queries, which allows you to use Elm language constructs to build and abstract your GraphQL queries (Apollo queries are built with plain strings with a JSON object passed in for variables)
* Rather than just grabbing raw JSON data, you build up your data into meaningful data structures (much like you do with JSON decoding in Elm)
* You get Elm compiler errors if your query is invalid
* You get documentation in your editor as you build up queries (the autogenerated functions have doc comments with the docs from your GraphQL API)
* You can do exhaustive onType ... selections for unions and interfaces (the compiler will tell you if you add a new type on the back-end that you don’t handle on the client-side, and you don’t get a Maybe something back because it knows you’ve handled every possibility)
* It handles creating aliases for you to prevent collisions automatically
Plug-ins change the behavior of an underlying map. For example, a Bloom Filter can be layered above a base map to enable fast membership queries. The bloom filter can avoid many lookups in the underlying map.
Many other plug-ins are possible such as caches and/or provers and verifiers for authenticated data structures.
Although this session uses a map as an example, the techniques shown may be applied to any data structure and its API.
Type classes in Haskell are used to solve a variety of problems and are a central idea in many design patterns. GHC also provides a significant number of language extensions for working with them. In order to work with type classes proficiently, a developer needs to be aware of each extension and understand its use cases.
For example, say you’re developing a smooth, polished application when suddenly management throws a new-requirement-shaped wrench into your beautiful code. You had a wonderful type class that could turn any data type into a nice, clean, text value. But suddenly, they don’t want strings to look like a list of each character in that string: `”[‘h’,’e’,’l’,’l’,’o’,...]”` but rather a cohesive string `”hello”`. It should be simple, right? Just add a new type class instance for `String` that calls `Data.Text.pack`. But wait, `String` is actually a type synonym for `[Char]` and you already have an instance for `[a]` so you can’t write another one in the same scope. How do you proceed?
This contrived example comes up fairly frequently when developing applications and leads many developers to reach for various language extensions to solve their compiler errors. GHC is “helpful” and may even suggest which ones to turn on to make the error go away. However, without a solid understanding of the fundamentals, language extensions can cause quickly cause your programs to quickly become opaque. This talk is centered on what each of these instance language extensions does, what the trade off they create is, and how to design around them when needed. We'll look at real-world, practical examples of when to use various extensions, and when to stay away.
At the end of this talk, you should have a clear understanding of how http4s can make it easier to build modern, runtime-safe services in Scala.
The content covered will be:
- Intro to lattices and recap of vector spaces
- Short Vectors in lattices and the shortest vector problem.
- Cryptosystems based on hard lattice problems: NTRUEncrypt, GGH signature scheme.
- (Tentative): Lattice reduction algorithms
In this workshop, you will learn to write simple logic proofs in the natural deduction style. You will learn why these proofs are actually functional programs.
We will check the correctness of the proofs using a verifier library that the speaker has written in Haskell. Using the verifier, you can write your proofs within Haskell code and get helpful error messages when they are incorrect. You can also generate LaTeX source for nicely typeset proofs.
* A modern APL perspective on the outer product, using the powerful array programming technique known as *function rank*
* How we can use Haskell functors to generalize the outer product to other data structures, and how the `(-(angled bracket; not allowed by YouTube)a)` functor gives rise to some useful combinators
* Fractals and other curiosities generated with the outer product, and why doing it this way gives us extra theoretical insight into these objects
* How to implement lightning-fast outer products, and how to take advantage of them to write Dyalog APL code that runs as fast as or faster than compiled languages
* How to use APL!
No knowledge of APL is assumed, but general programming and mathematics experience will be helpful.
In Haskell, we have a more powerful tool: software transactional memory (STM). STM allows you to write mutating code that would terrify anyone experienced with the horrors of non-STM mutation. We automatically gain resilience against many classes of bugs that plague the world in general. We also get powerful tools for handling techniques like message passing, when the situation calls for it.
In addition to covering how to use STM, we’ll discuss how STM’s rollback mechanism works and how this affects both semantics and performance. We’ll also analyze how Haskell’s purely functional nature allows STM to be as powerful and reliable as it is. And finally, we’ll point out some corner cases that may potentially trip up newcomers.
“Coeffects,” informally dual to effects, are the dependencies a computation has on the environment that are not the input of the computation. Delightfully, just as effects can be modeled using monads, coeffects can be modeled using indexed comonads. This term was first coined by Thomas Petrieck and others in his PhD thesis. In this talk, I give a gentle introduction to the definition of coeffects, and how they are modeled using indexed comonads, and then show how they can be used to give better type safety to your programs. Examples of coeffects include API versioning, implicit parameters, data flow computations, and bounded resource management.
In this workshop we will build a simple AR application, covering the basics such as building an interactive virtual environment (VR), binding virtual objects to markers in the real world. We will then use a simple client-server architecture to share the same AR environment among several users. All participants will be able to test their AR applications right away with just a mobile browser on their smartphones and easily share it with friends!
Along the way we will look at how Haskell — an advanced purely-functional programming language — can help when building AR applications. Specifically, we will rely on Haskell's type system (especially typed holes) to guide our implementation and get substantial help from GHC. We will also observe how Haskell allows us to safely and easily compose AR components and reuse foreign components (such as A-Frame components written in JavaScript). Furthermore we will discuss how Haskell allows us to separate pure logic from the intricacies of managing a virtual environment, working with a camera, and client-server communication for better composability and testing.
To build the application, we will go through a series of stages, starting from scratch in a prepared development environment.
Some materials such as 3D models and third-party components will be prepared and available in that environment, but you will be free to use your own.
To participate in this workshop you will need a laptop with a few gigabytes of available space (to install the development environment) and a smartphone with a camera and a modern mobile browser.
As it turned out, once we took a step back, we started to see a clearer picture and in a few days came up with an elegant solution that not only had solved our problem but offered helpful insights into our data processing.
In this talk, I will walk you through a process of designing a DSL to solve a repetitive practical problem in Haskell gaining readability, maintainability, and type-safety in the process!
We will start by analyzing the problem, recognizing patterns, and formulating properties that any solution should have. Then, we will find a suitable type to represent our domain and define operations on it. We will explore common abstractions such as monoid, functor, and monad to see if we can leverage them for a nicer API. Finally, we will arrive at a first iteration of a DSL to solve the initial problem. At the end of the talk we will discuss possible generalizations of this DSL as well as everyday tasks that may be simplified with a DSL.
* Compatibility is king. The language, core library, and tools must be built such that code you wrote 10 years ago can still compile and run today. This immediately rules out breaking changes and can also present intense difficulty when implementing a larger feature that spans the whole codebase.
* Performance is also king. Ensuring that a feature emits performant code at runtime is critical. Even more critical is that the implementation of a feature and tooling performs well if it is repeatedly executed in a long-running process. This forces us to write things in a different way than you may expect.
* People can come and go, but the product remains. Code that can be quickly understood and worked with is incredibly valuable in the long-term. However, this does present a danger of reducing new code you write to be a “lowest common denominator.”
* Today’s programmers inherit the mistakes of yesterday’s programmers. A large and long-lived codebase that has undergone many organizational changes carries the artifacts of past teams’ priorities. Some choices that made sense five years ago are now irrelevant, but the code cannot simply be ripped out.
* Change is the only constant. Visual Studio and .NET evolve faster and expand their capabilities. F# and the F# tools must keep up and innovate in the midst of this change, forcing difficult re-prioritization and tension with certain parts of the F# community.
* Impedance mismatches are everywhere. Although F#, being a .NET and Visual Studio language, is a boon, a primary tradeoff is that there are numerous non-FP pieces that must be plugged into. Reigning this in is not often straightforward, especially since not all concepts are something you can merely interface with.
By the end of this talk, you should have a strong understanding of some of the challenges we face when evolving F# and F# tools. Approaches to solving these challenges may also be applicable to the broader functional programming community, especially as functional programming languages breach further into the mainstream.
In large scale customer focused distributed systems with asynchronous programming involved, it becomes extremely hard to provide tracing and monitoring for the products. As it scales with high request counts with multiple pipelines involved, having proper distributed logging, tracing, monitoring, and metric system setup for the product is important from the product, development as well as from an operations perspective.
Our products have extremely high request rates per minute, and is one of the top most used apps in India.
Asynchronous programming is an integral part of lot of different programming languages.
In this talk, I run the setup and describe everything used while implementing the distributed computing setup.
This talk will guide the attendee through the notion of types as specifications and describe how to embed invariants about program runtime behavior into the Haskell type system. Using a collection of language extensions introduced at a steady interval, this talk will cover topics ranging from statically checking the length of lists to defining and applying higher order type-level functions. It will conclude with an example of embedding program behavior specifications as type-level state machines through the culmination of all prior material presented, in addition to indexed monads.
If you are an intermediate Haskell developer striving to understand how to bend GHC and the Haskell type system to your will more effectively, or a beginner Haskell tinkerer desiring to expand your knowledge of the benefits of modern Haskell language extensions, then you should attend this talk!
The Nix package manager and NixOS—a Linux distribution built on top of Nix—are a declarative way of setting up a system. Package rollbacks are trivial, making bad updates nothing more than a nuisance. Packages are accompanied by their dependencies and statically linked, allowing for multiple versions of the same library or application to live side-by-side. Finally, since the entire system (including installed applications) is configured from a single place, hunting through /etc and ~/.config is finally a thing of the past.
We define TTG & contrast to classy lens/prism. Trees That Grow *(Najd, Shayan and Peyton-Jones, Simon, 2016)* is proposed as a solution to a problem that regularly affects authors of deep and detailed algebraic structures. A data structure denoting a syntax tree for a programming language is typically very intricate and a small alteration deep in the tree can affect all siblings and parents of that tree. For example, adding a minor language feature to a syntax tree can have flow-on effects for the remainder of the tree. Classy lenses & prisms are a very powerful tool to overcome this common issue, which we will look at in this talk, but we will primarily look at another more recent proposal in Trees That Grow (TTG) to contrast and explore.
Although this general problem is canonically explained in terms of a programming language syntax tree (such as lambda calculus), we will also look at another application in aviation where TTG has been used to implement a flexible data structure tree in aviation documentation. The outcome of the talk is to provoke a discussion about this common programming problem, and the methods and trade-offs by which it might be overcome. TTG is also proposed as a solution to extending the Haskell programming language in the Glasgow Haskell Compiler (GHC).
Overall, the audience will get a good feel for the details of the problem that we are dealing with, then we explore some of the methods by which we can mitigate the problem, with an emphasis on gaining an understanding for Trees That Grow.


