Applied Functional Programming Theory

channel image

Applied Functional Programming Theory

winitzki

subscribers

My thoughts about what "declarative programming" really is, and where functional programming stands in relation to declarative programming.

Talk slides: https://github.com/winitzki/sofp/blob/master/talk_slides/fp_and_declarative.pdf

Outline:

Functional programming is interesting, but in a weird way
- FP is (almost) engineering
- Other programming paradigms are (almost) artisanship
A definition of declarative programming:
- A language for problem requirements, understandable to people
- The same language is mechanically translated into code
- The only known “silver bullet” of programming
Declarative programming must be domain-specific (DSL)
- We get a productivity boost as long as we avoid the pitfalls
Implementing DSLs is a “killer app” for functional programming
- FP is declarative for working with recursive data structures, such as labeled trees
- Requires learning some programming language theory

What did category theory ever do for us (functional programmers)? - An extreme pragmatic and un-academic approach. Examples are in Scala.

Talk given at Scale by the Bay 2019.

Slides: https://github.com/winitzki/sofp/blob/master/sofp-src/what-did-category-theory-do-for-us.pdf

Summary:

- Main features that functional programmers use to write better code; no category theory required
- Examples of typeclasses with laws, and why laws are important in practice
- Formulating typeclasses and laws via a generalized "lifting" type signature with "twisted" function types
- Definition of Category and Functor as generalizations that cover the laws of functors, contrafunctors, filterable functors, monads, applicative functors, comonads, etc.
- Examples of categories that are used to describe functors, monads, applicatives, and filterable functors
- Filterable functors in more detail, with backdrop of category theory
- "Type constructor libraries": free functor / free monad/ etc., and Church encoding as examples
- What the new book ("The Science of Functional Programming") will do
- Conclusion 1: programmers need to learn functional programming and not category theory
- Conclusion 2: basic definitions of category theory (category, functor) are useful as condensed formulations of general laws
- Conclusion 3: category theory will not help us derive or prove laws for specific typeclasses, because category theory only talks about laws that apply generally to a large number of very different typeclasses
- Q & A session. I was corrected by Oscar Boykin who described practical uses of the function "liftOpt" (which I claimed to be useless in practice).

https://www.meetup.com/SF-Scala/events/265169356/

Talk slides: https://github.com/winitzki/sofp/blob/master/sofp-src/reasoning-types-code-sf-scala.pdf

Talk Summary:

Functional programming is unique among programming paradigms because it allows us to reason rigorously about types and computations before we start writing code. In this way, functional programming is the only paradigm that makes the work of a software developer resemble the work of an engineer. I have been working on a new book, "The Science of Functional Programming". This presentation focuses on one of the main themes of the book - the techniques and applications of mathematical reasoning about types and code. I give examples of type and code reasoning tasks that are directly useful to functional programmers. Typical tasks are to determine whether a function with given type signature can be implemented; to write code for a typeclass method that satisfies the laws; and to transform a data type to an equivalent but simpler form. In this presentation, I show in detail two specific examples of mathematical reasoning using a notation I developed in the book. The first example is to derive the equivalence between three different formulations of the free monad. The second example is a proof (in 5 lines of calculations) that a certain complicated monad transformer satisfies its laws, - a proof that a recent academic paper failed to complete because such calculations are too hard when written in the syntax of code in a programming language.

I have been writing up my functional programming tutorials as chapters for a new book, "The Science of Functional Programming". This presentation focuses on one of the main themes of the book - the techniques and applications of mathematical reasoning about types and code.

I give examples of type and code reasoning tasks that are useful to practitioners of functional programming. Typical tasks are to determine whether a value of a given type can be computed, to implement a typeclass method that satisfies the laws, and to transform a type constructor to a mathematically equivalent but simpler form.

While working on my functional programming tutorials, I had to work through many derivations that were difficult to perform using the Scala syntax. To make this work easier, I have developed a condensed notation for calculations with types and code, which appears to be well adapted to reasoning tasks. In this presentation, I show the advantages of the condensed notation on two examples. First, I derive the equivalence between three different formulations of the free monad. Second, I prove (in 5 lines of calculations) the monad associativity law for the selector monad transformer, - a proof that a recent academic paper failed to carry out because such calculations are often unmanageable when written in the syntax of a programing language.

In the forthcoming free book, "The Science of Functional Programming", I will present detailed explanations and examples of the available techniques for type and code reasoning. The book's source code and current draft versions are available at https://github.com/winitzki/sofp

The current draft of the book can be downloaded as PDF at https://github.com/winitzki/sofp or purchased on paper at http://www.lulu.com/content/paperback-book/the-science-of-functional-programming/24915714

Slides for this talk: https://github.com/winitzki/sofp/blob/master/sofp-src/reasoning-types-code.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.

This part covers slides 1 to 11.

Chapter 11: Computations in a functor context III. Monad transformers

Combining Future and Option as an example of combining monadic effects "by hand" (without transformers)
Deriving the desired laws for lifting monads into a combined monad
Difficulties in combining monads in general: what does and what does not work
Examples of monads that compose and that do not compose with other monads
Simplifying the two identity laws of a monad into a single identity law for "lifting"
Deriving the composition law for "lifting" in terms of `flatten`, `flatMap`, and in terms of the Kleisli composition
Definition of "monadic morphism" and a proof that monadic morphisms are always natural transformations
Monad transformers as a way of reducing the programmer's work as opposed to combining monads by hand
What is a "monad transformer stack" and how it is different from a stack of nested type constructors
Formal requirements for a monad transformer: it must have two "liftings" and two "runners"
First examples: the monad constructions that lead to monad transformers (EitherT, ReaderT, WriterT)
The "zoology" of monad transformers: to each monad its own
The list of all known monad transformer constructions: "composed-inside", "composed-outside", "recursive", "product", "contrafunctor-choice", "free pointed", and "irregular" (StateT, ContT, SelectorT, CodensityT)
Why the continuation monad (as well as Codensity) do not actually have a full monad transformer (they do not have one of the "liftings" and they do not have any "runners")

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/11-monad-transformers.pdf

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

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 10 is split into 4 parts:
Part 1 of 4: https://www.youtube.com/watch?v=32Rs0xCHiqc
Part 2 of 4: https://www.youtube.com/watch?v=zNx-DORLfNY
Part 3 of 4: https://www.youtube.com/watch?v=m8oNzlbsAjI
Part 4 of 4: https://www.youtube.com/watch?v=BXBv3wOHi1Q

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.

This part covers slides 20 to 26.

Chapter 10: Free type constructions

Properties of existential types; why ∃Z.Z × (Z ⇒ A) is observationally equivalent to A, and why do we need "observational equivalence" of these values
Free functor in tree encoding
Free functor: Derivation of the reduced encoding from tree encoding
Preparation for Church encoding of a free functor
Church encoding of types and type constructors, in depth
How Church encoding makes recursive types apparently non-recursive
What needs to be done for Church encoding of a parameterized type
Examples: Church-encoded List[Int], Option[A], and List[A]
How the Church encoding of type classes such as Semigroup gives rise to the notion of "inductive typeclass"
A few general formulas for free typeclass instances in Church encoding
What properties we expect from free type constructions
Recipes for encoding arbitrary inductive type classes
Why the product type and the function type are compatible with inductive type classes (e.g. product of two monads is a monad), but disjunction type is not (e.g. disjunction of two monads is not a monad)
Examples of typeclasses that do not have tree-encoded free instances: non-inductive type classes (e.g. traversables)
The difference between inductive and co-inductive typeclasses
Stack-safe implementations of a free functor in tree and reduced encodings
Why the method `andThen` in standard Scala is not stack-safe, and how to fix that

Exercises

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/10-free-constructions.pdf

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

This tutorial is a continuation of the previous one, devoted to illustrating Chemical Machine programming using the example of "asynchronous guess-a-number game". In this game, the player can ask questions and the machine will answer all questions asynchronously, out-of-order. However, the machine should not print any answers while the player is typing a next question.

I show that the code in the previous tutorial has a deficiency: threads can be starved if the player sends too many questions quickly enough. I show how to reason about this problem in the chemical machine paradigm, and how to improve the previous solution. The new code is not longer than the previous one; the main difference is to create a separate reaction site for reactions that may take a long time.

Sample code in this tutorial:
https://github.com/Chymyst/Chymyst/blob/master/src/test/scala/io/chymyst/lab/ChymystGuessGame.scala

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

This tutorial illustrates Chemical Machine programming using the example of "asynchronous guess-a-number game". In this game, the player can ask questions and the machine will answer all questions asynchronously, out-of-order. However, the machine should not print any answers while the player is typing a next question.

I show how to determine the data that needs to be carried by molecules, and to come up with the code for the reactions. I explain how the chemical machine models contention and asynchronous requests. Contention is modeled straightforwardly by introducing an extra molecule that serves as a "contention token". In this way, contention is modeled separately from data.

Sample code in this tutorial:
https://github.com/Chymyst/Chymyst/blob/master/src/test/scala/io/chymyst/lab/ChymystGuessGame.scala

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

The chemical machine paradigm can be understood as a modification of the Actor model where the "chemical actors" are type-safe and are automatically managed by the runtime system.

I show that all the features of the chemical machine logically follow from this single requirement, together with the idea of waiting for messages from multiple mailboxes at once. In particular, it is necessary that the actors become stateless (all data resides on messages); that mailboxes become unordered multisets of messages, rather than ordered queues; and that the parallelism of the computations become an automatic feature provided by the runtime, rather than being managed explicitly by the programmer.

In this way, the chemical machine paradigm improves upon the Actor model, freeing the programmer from the need to manage the actors' lifecycles and mutable states, and making the code more purely functional and more declarative. The programmer can design a chemical machine program by reasoning directly in terms of data that resides on messages in mailboxes, rather than having to handle multiple running processes and their mutable states, as it is still necessary in the Actor model.

I also show how programs written in the Actor model can be directly and straightforwardly simulated by chemical machine programs.

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

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

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 9 is here:
https://www.youtube.com/watch?v=OnaHcVBbCGQ

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 9: Traversable functors

Motivation for the `traverse` operation
Deriving the `sequence` operation to simplify `traverse`
How to implement `sequence` for any polynomial functor
Motivation for laws of `traverse` from category theory
Deriving the laws for `sequence`
Constructions for traversable functors and bitraversable bifunctors
Deriving `foldMap` by specializing to a constant applicative functor
Reasons to introduce the `Foldable` type class
Implementing `foldLeft` via `foldMap`
Traversable contrafunctors and profunctors exist, but are not useful
Examples of using traversable and foldable: decorating trees
Implementing `scanLeft` as a traversal with respect to a State monad
Why breadth-first tree traversal or depth level computation cannot be represented via a traversal with a State monad
Naturality with respect to an applicative functor
Exercises

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/09-traversables.pdf

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

How to make callback APIs composable using the continuation monad
Examples with synchronous and asynchronous APIs
Example: converting Java NIO2 to continuation monad
How to use the continuation monad to handle extra information after callbacks are called
Using the monad (A ⇒ Future[R]) ⇒ Future[R] to handle asynchronous callbacks with error recovery (the "transaction monad"), not described in detail in this talk, see sample code
What is a "monadic DSL", what are its costs and benefits
Difference between using Scala Futures and using a monadic DSL

Commented code for the presentation: https://github.com/winitzki/scala-examples/blob/master/chapter07/src/test/scala/example/ContinuationMonadPresentation.scala

Commended code for the "transaction monad": https://github.com/winitzki/scala-examples/blob/master/chapter08/src/test/scala/example/TransactionMonad.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 8, part 2 is split into three portions:
(1 of 3) https://www.youtube.com/watch?v=xBDkBriX7Uk

(2 of 3) https://www.youtube.com/watch?v=sEaT0vbTnx8

(3 of 3) https://www.youtube.com/watch?v=G5Y7sqydEXo

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 2: Laws and structure

Portion 3 of 3 covers slides 17 to 22.

Implementing and checking the laws for applicative contrafunctor constructions
Why all exponential-polynomial contrafunctors with monoid coefficients are applicative
Definition and properties of profunctors
Why all exponential-polynomial type constructors are profunctors
Example of a non-profunctor type constructor: a partial type function
Definition and laws of applicative profunctors
Constructions of applicative profunctors; verifying the laws
Commutative applicative functors, their interpretation, and examples
A unified category theory-based picture of "standard" functor classes (functor, contrafunctor, filterable, monad, applicative)
How to use this picture to find laws and to discover new type classes, such as the comonads
Exercises

Slides: https://github.com/winitzki/talks/blob/master/ftt-fp/08-applicatives-part2.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 8: Applicative functors and profunctors. Part 2: Laws and structure

Portion 2 of 3 covers slides 15 to 17.

Implementing and checking the laws for applicative functor constructions
Examples of applicative functors that disagree with their monad instances
Examples of non-applicative functors
Monoid constructions: why all non-parameterized types are monoids
Why all polynomial functors with monoid coefficients are applicative
Definition and laws of applicative contrafunctors
How applicative contrafunctors are different from applicative functors

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

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

I show how to implement a simple multi-threaded (not distributed) consensus algorithm in the Chemical Machine, using the Chymyst library in Scala.

I derive the implementation by reasoning about the necessary molecules and data to be handled.

I then introduce a simple error that seems to be made frequently in chemical machine programming. I show how to debug the contents of the reaction site in order to diagnose and fix the error. I also show how to enable various log levels and trace the scheduling of reactions as it is performed by the chemical machine runtime.

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

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

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

I show how use the Chemical Machine, implemented by the Chymyst library in Scala, to create concurrency patterns that depend on parameters known at run time, rather than defined statically.

Two main examples are described here:
- the "dining philosophers" problem with `n` philosophers
- a parallel simulation of Conway's "game of life" on a wrap-around rectangular board

In the code, the necessary molecules and reactions are first defined and stored in arrays, and only later activated. This allows us to implement a concurrent application that requires an _a priori_ unknown number of molecules and reactions.

I start from an implementation of "dining philosophers" with a statically defined number (5) of philosophers, to an implementation where the number of philosophers is given at run time.

I implement the "game of life" using a single reaction for all cells on the entire board for all time steps; using a single reaction per time step; and using a single reaction per cell.

I show that the performance of the program is greatly improved if we reorganize the "chemistry" to avoid certain performance-killing anti-patterns:

- defining a large number of quick reactions in a single reaction site; this prevents the reactions from being scheduled concurrently
- defining a reaction with a cross-molecule guard condition, while emitting a large number of molecules for which that condition will have to be evaluated; this leads to a very slow scheduling of each reaction

The best performance for the "game of life" simulation is achieved when using a separate, single-reaction reaction site for each cell on the board and for each time step.

Code for this presentation: https://github.com/Chymyst/Chymyst/blob/master/src/test/scala/io/chymyst/lab/ChymystDinPhil.scala
https://github.com/Chymyst/chymyst-core/blob/master/core/src/test/scala/io/chymyst/test/DiningPhilosophersSpec.scala
https://github.com/Chymyst/chymyst-core/blob/master/core/src/test/scala/io/chymyst/test/DiningPhilo..

I show how to implement the recursive fork/join pattern in the Chemical Machine, using the Chymyst library, and compare this implementation with a standard Scala Future-based code.

I show two Chemical Machine recursive fork/join implementations, which are concise and very similar in their approach.

The first implementation is derived from straightforward reasoning about usage of molecules for handling concurrent data. However, this implementation creates a large number of new reaction sites (one per fork branch point), which leads to slow performance since the Chymyst library incurs significant overhead when creating a new reaction site. Nevertheless, this example illustrates how Chemical Machine code can declare new molecules and reaction sites within a reaction, which results in a recursively defined concurrent logic.

The second implementation of fork/join is based on the idea of replacing one of the molecules with a _continuation_, a function having the same type as the molecule emitter call. In this way, we avoid having to declare new reaction sites, and also avoid thread-switching: all reactions are scheduled through a single molecule within a single reaction site, and the "join" stage is executed on the same thread as the last of the "forked" subtasks. This implementation turns out to be significantly faster than the Scala Future-based benchmark.

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

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

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

I show how to implement the broadcast publish/subscribe pattern in the Chemical Machine, using the Chymyst library.

I derive the code by reasoning about what molecules need to be introduced to implement the desired functionality.

The resulting code is declarative - it is just a few lines of reactions, and these reactions directly describe what the publish/subscribe functionality must do.

The test creates a publisher and two subscribers, and shows that we can subscribe, unsubscribe, and stop the publisher concurrently, at chosen times.

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

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

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

This tutorial shows how to use the Chemical Machine to implement all the concurrency primitives of the Go language: the "goroutines", the "channels", and the "select" construction.

The main similarity between the Chemical Machine paradigm and the CSP paradigm (as implemented in the Go language) are that channel "send" action is somewhat similar to emitting a molecule. When a message is "sent on a channel", it waits until someone "receives" it. This is similar to how an emitted molecule remains at the reaction site until some reaction consumes it.

At that point, similarities end and differences begin:

- Sending and receiving are blocking operations by default, while emitting a molecule is a non-blocking operation in the chemical machine
- Reactions start automatically on the chemical machine, while "goroutines" need to be started manually
- The Chemical Machine encourages data-driven reasoning, while the Go language requires reasoning about processes that run and send messages to each other at a given time
- Contention on which reaction can consume a molecule is defined statically in the chemical machine, while the Go language allows the developer to define new code that contends on reception from previously defined channels
- The chemical machine helps the programmer to expose potentially ambiguous and non-deterministic code, which the Go language does not make apparent

I illustrate these differences by running example code:

- the "select" construction
- the "ping-pong" example from https://talks.golang.org/2013/advconc.slide#6

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

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

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

This is a basic conceptual introduction into the Chemical Machine programming paradigm, using the `Chymyst` library for Scala.

Contents:

Explanation of the "chemical metaphor" of concurrent programming
How molecules and reactions model concurrent computations
First example: concurrent counter
Different versions of producer/consumer
Debugging and typical errors in chemical machine programming
Discussion of indeterminism
Simple declarative implementation for the "dining philosophers" problem
Comparison with implementations of the "dining philosophers" problem in other programming languages

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

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

This is a basic introduction into the Chemical Machine programming paradigm, using the `Chymyst` library for Scala.

This tutorial is for people who prefer to dive into code, without much discussion of the underlying concepts.

Here I explain only the bare minimum necessary to be able to start using the Chemical Machine and the `Chymyst` library for Scala. I emphasize the basic, practical aspects of creating molecules, reactions, and reaction sites when writing concurrent programs.

I give several examples, such as a concurrent counter with read access, a counter with blocking access, and a parallel `map` operation.

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

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

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/

SHOW MORE

Created 6 years, 1 month ago.

49 videos

Category Science & 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