Applied Functional Programming Theory

winitzki

This tutorial implements a simple throttling (or "rate limiter") function for the Chemical Machine.

- Use systematic, logical reasoning to derive the implementation of the throttling functionality from the requirements
- Package the throttling code as a generic function
- Test the code
- Compare with throttling implementations for Akka, Monix, and ZIO
- How the Chemical Machine enables programmers to write declarative ("obviously correct") concurrent code

Code for the presentation: https://github.com/Chymyst/Chymyst/blob/master/src/test/scala/io/chymyst/lab/ChymystThrottler.scala

Main repository for the `Chymyst` library: https://github.com/Chymyst/chymyst-core/

"Concurrency in Reactions", a tutorial book on `Chymyst` and Chemical Machine programming: https://winitzki.gitbooks.io/concurrency-in-reactions-declarative-multicore-in/content/

SoftwareMill blog post, comparing Akka, Monix, and ZIO: https://blog.softwaremill.com/scalaz-8-io-vs-akka-typed-actors-vs-monix-part-1-5672657169e1

What would be a good domain-specific language (DSL) for expressing concurrent and parallel computations in a natural and declarative manner?

The goal is to design a programming language where the programmer can simply say "this computation with this data here needs to be made concurrent" - and obtain automatically parallelized, concurrent code, safe from race conditions.

Starting from examples and proceeding systematically, I derive precisely such a DSL for concurrent programming.

I show that, in order to achieve this kind of high-level, purely declarative concurrency, a programming language needs just two features:

1. A construction that labels data values as "concurrent data", using locally scoped "labels" (which are values of a special type).
2. A construction to define "concurrent functions" that can take labeled "concurrent data" as input and will emit new "concurrent data" as output.

The need for these two features is a logical consequence of our requirement to be able to denote concurrency declaratively, and to achieve automatic yet safe parallelism.

A programming language with these two features is equivalent to the "Chemical Machine", also known as "join calculus" in the academic literature. I demonstrate working test code in Scala using the Chemical Machine via the `Chymyst` library.

I explain how the "chemical metaphor" provides a more visual terminology that helps us understand how "concurrent data" and "concurrent functions" actually work.

Code for the presentation: https://github.com/Chymyst/Chymyst/blob/master/src/test/scala/io/chymyst/lab/ChymystPresentation.scala

Main repository for the `Chymyst` library: https://github.com/Chymyst/chymyst-core/

"Concurrency in Reactions", a tutorial book on Chymyst and Chemical Machine programming: https://winitzki.gitbooks.io/concurrency-in-reactions-declarative-multicore-in/content/

The main topic of this presentation is to illustrate the use of the "free monad" as a design pattern. The free monad can replace imperative code by declarative data structures that are composable and can be "run" or "interpreted" later.

This session shows a straightforward implementation of the free monad and explains how it works in more detail. I also show how to use the `Free` type constructor as implemented in the `cats` library.

Contents:

How to transform an imperative API into a sequence of instructions
Specific example: a subset of API for Apache HDFS file system client (create / read / write / delete files)
Using case classes and a trait with a type constructor `HdfsOps[A]` to represent an imperative API
Showing why the result is not a monad and not even a functor
Motivating a monad (rather than, say, a `List`) as the data structure for a sequence of instructions
Defining the `pure` and the `flatMap` methods on a free monad
Transforming the free monad into an arbitrary target monad `M`, generically
Examples of "interpreters" for the `HdfsOps` free monad: one interpreter for `Writer` monad, another for the `Try` monad
Doing the same thing with the `cats` library
Final example: Encoding some Akka-Http routing directives as a free monad, and what advantages this could bring

Source code: https://github.com/winitzki/scala-examples/blob/master/chapter08/src/test/scala/example/FreeMonadPresentation.scala
https://github.com/winitzki/scala-examples/blob/master/chapter08/src/test/scala/example/AkkaHttpFreeMonad.scala

This short summary gives an overview of the material presented in detail in the corresponding chapter of the functional programming tutorial.

The summary is designed to help you decide whether you want to spend time on the full tutorial, and also to refresh the main points of the tutorial after you already listened to it.

The full recording of chapter 7, part 2 is here: https://www.youtube.com/watch?v=p0fH_adTCnQ

Split into parts:
1 of 2: https://www.youtube.com/watch?v=u_XH7XkvFWM
2 of 2: https://www.youtube.com/watch?v=rKQqdAF9ecA

This short summary gives an overview of the material presented in detail in the corresponding chapter of the functional programming tutorial.

The summary is designed to help you decide whether you want to spend time on the full tutorial, and also to refresh the main points of the tutorial after you already listened to it.

The full recording of chapter 8, part 1 is here: https://www.youtube.com/watch?v=NVlFZYxgXDw

This short summary gives an overview of the material presented in detail in the corresponding chapter of the functional programming tutorial.

The summary is designed to help you decide whether you want to spend time on the full tutorial, and also to refresh the main points of the tutorial after you already listened to it.

The full recording of chapter 5 is here: https://www.youtube.com/watch?v=QhqsBgJ8lm8

This short summary gives an overview of the material presented in detail in the corresponding chapter of the functional programming tutorial.

The summary is designed to help you decide whether you want to spend time on the full tutorial, and also to refresh the main points of the tutorial after you already listened to it.

The full recording of chapter 3 is split into three parts:

Part 1 (The types of higher-order functions): https://www.youtube.com/watch?v=Z_1s36ba4EY

Part 2 (Disjunction types): https://www.youtube.com/watch?v=MTViank6L24

Part 3 (The Curry-Howard correspondence): https://www.youtube.com/watch?v=sSDGjdfFQ-Y

The main topic is to illustrate how several `fold` operations can be combined automatically into a single traversal. In Chapter 8, part 1, the central pieces of code were implemented automatically using the `curryhoward` library. This live coding session shows the implementation and explains how it works in more detail.

Defining a `fold` operation as a data structure and running it afterwards
Combining several `fold` operations into one
Implementing the applicative `zip` operation is possible on `fold`s despite `fold` not being a functor
Adding a final transformation to a `fold`, to make it into a functor
Implementing a DSL for `fold`s so that running average and standard deviation can be expressed concisely
Illustrating the difference between applicative and monadic combinators for `fold`s

Source code: https://github.com/winitzki/scala-examples/blob/master/chapter08/src/test/scala/example/FoldsPresentation.scala

Functional programming in the mathematical spirit.

Long and difficult, yet boring explanations given in excruciating detail.

Start by reading the slides, go through the worked examples and exercises. Watch the video when you cannot fully understand something in the slides.

Chapter 8: Applicative functors and profunctors. Part 1: Practical examples

Why monads do not usually describe effects that are independent or commutative
Intuitions behind the `map2` function, coming from monads
Generalize map, map2, to map3 and mapN
How to implement map2 and map3 for `Either` to collect multiple errors from computations
Why the Future and the Reader monads already have commutative and independent effects
How to transpose a matrix by using map2 with `List`
Profunctors and their distinction from functors and contrafunctors
How to use profunctors to combine several `fold` passes into one
The distinction between applicative `fold` combinator and the monadic combinator: running average of running average
The distinction between applicative parser combinator and the monadic parser combinator: stopping at errors
Exercises

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/08-applicatives-part1.pdf

Code examples: https://github.com/winitzki/scala-examples/tree/master/chapter08/src

Functional programming in the mathematical spirit.

Long and difficult, yet boring explanations given in excruciating detail.

Start by reading the slides, go through the worked examples and exercises. Watch the video when you cannot fully understand something in the slides.

Chapter 7: Computations in a functor context II. Monads and semimonads. Part 2: Laws and structure of monads

How to derive the laws for flatMap from our intuitions about functor block computations
Deriving the laws for flatten from the laws for flatMap
Why flatten is equivalent to flatMap, and what it means to be "equivalent"
Why flatten has one law fewer than flatMap
How parametricity assures naturality laws
Worked examples showing how to verify the associativity law for all standard monads
Examples of incorrect implementation of flatten that violates the associativity law
Motivation for full monads and laws for the `pure` method
Deriving the laws for `pure` in terms of `flatten`
Reformulating the monad laws in terms of Kleisli functions
A simplified definition of "category" and "morphism"
How category theory provides a conceptual generalization of "lifting"
Deriving the laws of `pure`, `flatten`, and `flatMap` from the laws of Kleisli category
Structure of semigroups and monoids: how to build up semigroups and monoids from parts
Structure of semimonads and monads: building up new monads from previously given monads, functors, and contrafunctors

The recording of the full lecture of Chapter 7, Part 2 is https://www.youtube.com/watch?v=p0fH_adTCnQ but it was too long for YouTube to generate the subtitles. For convenience, I split it into two parts, each now with subtitles. This is the first part of the recording.

Functional programming in the mathematical spirit.

Long and difficult, yet boring explanations given in excruciating detail.

Start by reading the slides, go through the worked examples and exercises. Watch the video when you cannot fully understand something in the slides.

Chapter 7: Computations in a functor context II. Monads and semimonads. Part 2: Laws and structure of monads

How to derive the laws for flatMap from our intuitions about functor block computations
Deriving the laws for flatten from the laws for flatMap
Why flatten is equivalent to flatMap, and what it means to be "equivalent"
Why flatten has one law fewer than flatMap
How parametricity assures naturality laws
Worked examples showing how to verify the associativity law for all standard monads
Examples of incorrect implementation of flatten that violates the associativity law
Motivation for full monads and laws for the `pure` method
Deriving the laws for `pure` in terms of `flatten`
Reformulating the monad laws in terms of Kleisli functions
A simplified definition of "category" and "morphism"
How category theory provides a conceptual generalization of "lifting"
Deriving the laws of `pure`, `flatten`, and `flatMap` from the laws of Kleisli category
Structure of semigroups and monoids: how to build up semigroups and monoids from parts
Structure of semimonads and monads: building up new monads from previously given monads, functors, and contrafunctors
Worked examples with full derivations of laws for most of the constructions
Why certain constructions can be only semimonads but not full monads
Why there cannot be a contravariant monad
Exercises, with examples and counter-examples of semimonads and monads

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/07-monads-part2.pdf

Code examples: https://github.com/winitzki/scala-examples/tree/master/chapter07/src

This is an extended version of the talk given at Scale by the Bay 2017 talk video

Chymyst Core main code repository: https://github.com/Chymyst/chymyst-core

Abstract: Chymyst is a new open-source framework for industry-strength declarative concurrent programming in Scala. Chymyst implements the Abstract Chemical Machine (a.k.a. Join Calculus) concurrency paradigm, which radically improves upon the well-known Actor model by making actors type-safe, stateless, and automatically managed. I show concise and fully declarative Chymyst solutions for classic concurrency problems such as the "dining philosophers" or parallel "merge sort". Chymyst is in active development; next steps on the roadmap include providing comprehensive industry-friendly features such as APIs for unit testing, performance monitoring, and fault tolerance.

Functional programming in the mathematical spirit.

Long and difficult, yet boring explanations given in excruciating detail.

Start by reading the slides, go through the worked examples and exercises. Watch the video when you cannot fully understand something in the slides.

Chapter 3, part 2.

Scala's "case classes" understood as tuples with names
Pattern-matching syntax for case classes
Motivation for introducing disjunction types
First example of disjunction type: Either[A, B]
Implementing disjunction types via "sealed traits" and case classes
Using disjunction types to model complicated domains
Understanding Option[T] as disjunction type and as a collection type
Worked examples and exercises

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/03-logic-of-types-2.pdf

Code examples: https://github.com/winitzki/scala-examples/tree/master/chapter03/src

Title:

Introduction to the Curry-Howard correspondence: The logic of types in functional programming languages

Contents:

The commonality of type constructions in functional programming languages: Scala, OCaml, Haskell
Defining the propositions that correspond to types
What are "sequents" and how they are used to describe logical inference from premises
How logical derivations correspond to expressions in the programming language; how to convert one to the other and back
What is the "logic of types" defined by the common type constructions in the functional programming languages: it is the intuitionistic propositional logic (IPL)
Examples that contrast the IPL with the classical Boolean logic
Example of using Gentzen's calculus LJ to search for a proof
The advantage of the Vorobieff-Hudelmaier-Dyckhoff's calculus LJT over Gentzen's calculus LJ, and why people are using LJT for proof search
Example of what mathematicians mean when they say "it is trivial"
How to transform proofs back to code: proof transformer functions that correspond to derivation rules in LJ/LJT
Example of deriving code automatically from a proof of a sequent
How to use the "arithmetical Curry-Howard correspondence" to decide which types are equivalent
What are polynomial data types and exponential-polynomial data types
Summary: What are the practical uses of the CH correspondence
Limitations of the propositional logic: what it can and cannot do
Using the CH correspondence as a guide in programming language design

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/curryhoward-2018-tutorial.pdf

Functional programming in the mathematical spirit.

Long and difficult, yet boring explanations given in excruciating detail.

Start by reading the slides, go through the worked examples and exercises. Watch the video when you cannot fully understand something in the slides.

Chapter 3, part 3.

How types are interpreted using propositional logic
How to write type expressions in the shorthand notation
The four-point correspondence between propositions/proofs and types/code
How to verify or to refute isomorphism (equivalence) relationships between types
Identities in logic vs. identities in arithmetic: the two sides of the CH correspondence
Deriving the code of functions based on types of those functions
Exponential-polynomial types vs. "algebraic" types
Recursive polynomial type (List) and its type formula
Worked examples and exercises

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/03-logic-of-types-3.pdf

Code examples: https://github.com/winitzki/scala-examples/tree/master/chapter03/src

The "curryhoward" project: https://github.com/Chymyst/curryhoward

Sample code: https://github.com/winitzki/scala-threads-futures-intro
• The backbone of Java concurrency: thread pool executors
• How and when do Futures run? (On thread pools.)
• What does it mean to be “thread safe” and “nonblocking”?
– nonblocking = uses multi-core CPU optimally
– thread safe = permits easy concurrent nonblocking code
• Some typical “gotchas” when using Futures in the real world
• Converting other async APIs to Futures and back

Abstract:

I implemented a library for compile-time code generation from Scala type signatures. The library uses (compile-time) reflection, the Curry-Howard correspondence, and a theorem prover for the constructive propositional logic. Using this library, I illustrate how the Curry-Howard correspondence maps types into propositions and proofs into code. I will also explain some details of the algorithm I used for automatic code generation from type signatures. As an illustration of using this library for automatic code generation, I demonstrate working examples such as implementing map and flatMap for the Reader and State monads.

Contents:

How types are interpreted using propositional logic
Deriving the code of functions by hand, based on types of those functions
Using the "curryhoward" library to do the same automatically
The features of the "curryhoward" library
How the theorem prover works: the calculus LJ of Gentzen and the calculus LJT of Vorobieff-Hudelmaier-Dyckhoff
How to interpret the derivation rules for sequents
Building the lambda-calculus proof term from the proof tree
The "obvious" theorem of Vorobieff

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/curryhoward-2017.pdf

Code repository of the "curryhoward" project: https://github.com/Chymyst/curryhoward

Functional programming in the mathematical spirit.

Long and difficult, yet boring explanations given in excruciating detail.

Start by reading the slides, go through the worked examples and exercises. Watch the video when you cannot fully understand something in the slides.

Chapter 3, part 1.

The types of functions that return functions
"Curried" functions: their syntax e.g. f(x)(y) and how they work
"Curried" type expressions (A ⇒ B ⇒ C)
Scala type inference: how to give the type annotations
How to infer the most generic (parametric) types for higher-order functions
Worked examples and exercises

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/03-logic-of-types-1.pdf

Code examples: https://github.com/winitzki/scala-examples/tree/master/chapter03/src

Note: There was an error in the last exercise as shown in the video. The last exercise had no solution. Please download the updated version of the slides.

Functional programming in the mathematical spirit.

Long and difficult, yet boring explanations given in excruciating detail.

Start by reading the slides, go through the worked examples and exercises. Watch the video when you cannot fully understand something in the slides.

Chapter 2.

Tuples and pattern matching
Using tuples with Map[] and Seq[] collections (zip, map, flatMap, etc.)
Writing functions with type parameters
Implementing mathematical induction with recursion
Tail recursion and the accumulator trick
Using fold, foldLeft, scan, iterate instead of writing recursion by hand
Worked examples and exercises

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/02-functional-collections.pdf

Code examples: https://github.com/winitzki/scala-examples/tree/master/chapter02/src

Functional programming in the mathematical spirit.

Long and difficult, yet boring explanations given in excruciating detail.

Start by reading the slides, go through the worked examples and exercises. Watch the video when you cannot fully understand something in the slides.

Chapter 1.

Values, types, and functions in Scala
Named functions and anonymous functions
Examples of collections, `map`, `filter`, `sum`, etc.
Higher-order functions
How to translate mathematical formulas into Scala code
Examples and exercises

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/01-values-types-expressions.pdf

Code examples: https://github.com/winitzki/scala-examples/tree/master/chapter01/src

Functional programming in the mathematical spirit.

Long and difficult, yet boring explanations given in excruciating detail.

Start by reading the slides, go through the worked examples and exercises. Watch the video when you cannot fully understand something in the slides.

Chapter 4. Functors: their laws and structure

Abstracting the properties of a "data container"
Motivation for the functor laws
Examples of functors and non-functors
Examples of deriving a functor's fmap from its type and checking the laws
Contrafunctors; covariance and contravariance
How to decide whether a type constructor is a functor, a contrafunctor, or neither
Building up the structure for exponential-polynomial functor types: functor product, disjunction, implication, composition, recursion
How to prove the functor laws for each build-up step
Worked examples and exercises

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/04-functors.pdf

Code examples: https://github.com/winitzki/scala-examples

Functional programming in the mathematical spirit.

Long and difficult, yet boring explanations given in excruciating detail.

Start by reading the slides, go through the worked examples and exercises. Watch the video when you cannot fully understand something in the slides.

Chapter 6: Computations in a functor context I. Filterable functors, their laws and structure. Part 2. Filterable functors in depth

Equivalent definition of filterable type class via `deflate` or `mapOption` instead of `withFilter`
How to simplify the laws of filterable functors by using a Kleisli category
Detailed derivations of laws for `mapOption`
Intuitions behind natural transformations and naturality laws
What category theory does for us, and what it does not do
Constructions of filterable functors from other functors
Intuitions behind filterable contrafunctors vs. filterable functors
Fiilterable contrafunctors: their laws and structure (in brief)
Worked examples and exercises

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/06-filterable-functors.pdf (Part 2 covers only slides 9 to end)

Code examples: https://github.com/winitzki/scala-examples/tree/master/chapter06/src

Functional programming in the mathematical spirit.

Long and difficult, yet boring explanations given in excruciating detail.

Start by reading the slides, go through the worked examples and exercises. Watch the video when you cannot fully understand something in the slides.

Chapter 7: Computations in a functor context II. Monads and semimonads. Part 1: Practical work with monads and semimonads

Using "functor blocks" (for/yield syntax) for nested iteration
The difference between semimonads and monads
Visual explanation of how flatMap operates on sequences
Intuitions behind using several generator arrows with sequences
The different kinds of monads: list-like, pass/fail, tree-like, single-value
Examples of working with list-like monads: permutations, 8 queens, and other tasks
Using recursion in a functor block
Pass/fail monads: Option, Either, Try, Future
Examples of working with pass/fail monads to achieve safety and to sequence computations
How to make Futures parallel even though they are sequenced within a functor block
Examples of functor-shaped tree constructions
Visual explanation of how flatMap grafts subtrees on trees, and what "flattening" means for trees
Single-value monads: Writer, Reader, Eval, Cont, State; representing a "single value with context"
Using Writer as a semimonad, to keep track of elapsed time
Using the continuation monad to avoid "callback hell"
A systematic derivation of the Writer, Reader, Cont, State type constructors from the type signature of flatMap
Worked examples and exercises

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/07-monads-part1.pdf (Part 2 covers only slides 9 to end)

Code examples: https://github.com/winitzki/scala-examples/tree/master/chapter07/src

Functional programming in the mathematical spirit.

Long and difficult, yet boring explanations given in excruciating detail. Start by reading the slides, go through the worked examples and exercises. Watch the video when you cannot fully understand something in the slides.

Chapter 6: Computations in a functor context I. Filterable functors, their laws and structure. Part 1. Examples. Working with filterable functors.

"Functor blocks" (Scala's "for/yield" syntax) and filterable functors
Examples of polynomial filterable functors
Intuitions behind the notion of "filtering" the data in a container
Deriving the filterable functor laws from the intuitions
Examples of functors that are not filterable, and reasons why
Defining the Filterable type class and checking the laws with Scalacheck
Example of a filterable contrafunctor
Worked examples and exercises

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/06-filterable-functors.pdf (Part 1 covers only slides 1 to 8)
Code examples: https://github.com/winitzki/scala-examples/blob/master/chapter06/
I have added a more detailed explanation of "type lambdas" here, https://github.com/winitzki/scala-examples/blob/master/chapter06/src/test/scala/example/Chapter06_01_workedExamplesSpec.scala#L240-L251

A video tutorial about how to begin using IntelliJ for Scala development:
- Download and install IntelliJ on a Mac
- Configure IntelliJ plugins
- Create a new Scala project based on SBT
- Write new code and run unit tests
- Navigate around the code
- Configure IntelliJ for more convenience

SHOW MORE

Created 3 months, 3 weeks ago.

26 videos

CategoryScience & Technology

This is a series of extensive tutorials on functional programming.

The tutorials cover both the theory and the practice of functional programming.

Applied functional type theory (AFTT) is what I call the subdomain of computer science that should serve the needs of functional programmers who are working as software engineers.

It is these practitioners, rather than the academic researchers, who need to examine the incredible wealth of functional programming inventions over the last 30 years, -- such as these "functional pearls" papers -- and to determine which theoretical material has demonstrated its pragmatic usefulness and thus belongs to AFTT, and which material may be tentatively omitted. This tutorial series is therefore also an attempt to define the proper scope of AFTT.

In the videos, I demonstrate code examples in Scala using the IntelliJ editor because this is what I am most familiar with. However, most of this material will work equally well in Haskell and some other FP languages. This is so because AFTT is not specific to Scala or Haskell, -- a serious user of any other functional programming language will have to face the same questions and struggle with the same practical issues.

Uncopyright

All lecture content is authored by Sergei Winitzki, Ph.D.

The lecture materials are released into the public domain under a CC-0 license, which is an "uncopyright".

Intended audience

The material is presented here at medium to advanced level. It is not suitable for people unfamiliar with school-level algebra, or for people who are generally allergic to mathematics, or for people unwilling to learn new and difficult concepts through prolonged mental concentration.

The first two chapters are introductory and may be suitable for beginners in programming. Starting from chapter 4, the material becomes unsuitable for beginners.

Main features and goals of this tutorial series

an emphasis on the mathematical principles that guide the practice of functional programming
the presentation is self-contained -- introduces and explains all required concepts and Scala features
an emphasis on clarity and understandability of all explanations, derivations, and code
some terminology and notations are non-standard -- this is in order to achieve a clearer and more logically coherent presentation of the material
all mathematical developments are thoroughly motivated by practical programming issues
avoid developing abstract theory for theory's sake
examples must show how each mathematical construction is used in practice for writing code
mathematical generalizations are not pursued beyond either practical usefulness or immediate pedagogical usefulness
each new concept or technique has sample code and unit tests to illustrate its usage and check correctness
currently the libraries cats and scalacheck are used throughout the sample code
each new concept or technique is fully explained via "worked examples" and drilled via provided exercises
answers to exercises are not provided, but it is verified that the exercises are doable and free of errors