FP

FP Jargon Reference all morphisms chart

Misc+

• Szulc, "Let's write some FP code", youtube
• Course of Advanced Functional Programming (youtube)
• Functional Programming Jargon
• J. de Goes, Glossary of FP
• All Kiselyov's stuff
• Kiselyov etc, Extended Effects
• Kiselyov et al, Finally Tagless, Partially Evaluated
• Kiselyov, Typed Tagless Final Interpreters
• Bauer, Pretnar, Programming with Algebraic Effects and Handlers
• Describing Data...with free applicative functors (and more)—Kris Nuttycombe
• Capriotti, Free Applicative Functors
• Functional Design Patterns
• VARMO VENE, CATEGORICAL PROGRAMMING WITH INDUCTIVE AND COINDUCTIVE TYPES
• Data.Functor.Foldable
• Bird, Patterson, Generalised Folds for Nested Datatypes
• J.Reynolds, Using category theory to design implicit conversions and generic operators
• Gibbons, Comprehending Ringads
• Hinze, Kan Extensions for Program Optimisation
• The Essence of Iterator Pattern
• Torre-Borre, Essence of Iterator Pattern
• Three Popular FP Myths
• Neural Networks, Types, and Functional Programming
• Tony Morris, Flip-Cons (youtube)
• Tony Morris, Zippers
• Altenkirch, Categories for the lazy functional programmer
• Stream Monad
• Erik Meijer on FP
• Winitzki, Science of Functional Programming
• gist of applicative functor not a monad, in Scala
• Chris Penner, Optics by Example

Lambda

• [Federico Aschieri, Francesco A. Genco, ⅋ means Parallel: Multiplicative Linear Logic Proofs as Concurrent Functional Programs)
• Xiaojuan Cai, Yuxi Fu, The λ-calculus in the π-calculus
• Barendregt, Lambda Calculus (pdf)
• Барендрегт, Ламбда-исчисление (пдф)
• History of Lambda-calculus and Combinatory Logic
• Lambda for dummies
• Y-combinator
• Augustss, "Lambda, polymorphic lambda, etc"
• Linear Lambda Calculus
• Mogensen-Scott encoding
• A Theory of Changes for Higher-Order Languages - Incrementalizing λ-Calculi by Static Differentiation
• Fokkinga, Data Type Laws without Signatures

Some Combinators

• ι = λf.((fS)K)
• C = λfλgλx f(gx) // just composition
• L = λxλf = f x x // lifting (?)
• S = λcLc // e.g.

Languages

Haskell

• Where did bind come from
• tio.run
• Adventures in Classical-Land, by Dan Piponi
• The Mother of All Monads
• Д.Шевченко, Хаскель pdf
• Макеев, Haskell
• djinn: Generate Haskell code from a type
• nponeccop/haskell-exercises
• Write you a Haskell
• A Haskell monad for infinite search in finite time
• Set in Haskell
• Higher-order Type-level Programming in Haskell
• Kowalnik
• Ben Rudiak-Gould, Alan Mycroft, and Simon Peyton Jones, Haskell Is Not Not ML
• clintonmead/haskell_bits
• Milewski, Recursion Schemes for Higher Algebras
• Conal Elliott, Can functional programming be liberated from the von Neumann paradigm?
• Haskell programmer evolution

Coq

• Logical Verification Course Notes

Other

• Eta - modern Haskell for JVM
• Gherkin, a dialect of Lisp
• F* language
• Verse (SPJ)

Types

• Inheritance is not Subtyping
• Reynolds, Types, Abstraction, and Parametric Polymorphism
• Programming in Martin-Löf ’s Type Theory
• CATEGORICAL PROGRAMMING WITH INDUCTIVE AND COINDUCTIVE TYPES, VARMO VENE
• Typestate-Oriented Programming
• Impredicative Encodings of Inductive Types in HoTT
• Substructural type systems
• Oregon 2014, "Types, Logic, Semantics, and Verification"
• The Little Typer
• The Little Typer: Pie, github
• A simple type-theoretic language: Mini-TT
• On Understanding Data Abstraction, Revisited
• Final data types and their specification
• Tarmo Uustalo, Types for Proofs and Programs
• Luca Cardelli, Peter Wegner, On Understanding Types, Data Abstraction, and Polymorphism
• A tour of some useful recursive types
• Principal Type Schemes for Functional Programs with Overloading and Subtyping

ADT

• Algebraic Data Types in JS (package)
• The Algebra of Algebraic Data Types BY TONY MORRIS
• Scott encoding of Algebraic Data Types

Dependent Types

• Andrej Bauer Philipp G. Haselwarter Peter LeFanu Lumsdaine, A general definition of dependent type theories
• Linear Dependent Types for Differential Privacy
• Checking Dependent Types with Normalization by Evaluation: A Tutorial
• Checking Dependent Types with Normalization by Evaluation: A Tutorial (Haskell Version)
• Adam Chlipala, Certified Programming with Dependent Types
• Marcin Rzeźnicki, Path dependent types: Modeling algebraic structures has never been easier

Optics

• Optics by Example, book
• An Intuition for Optics BY TONY MORRIS
• Morris, An Intuition for Optics
• Keno Fischer, Terminology, autodifferentiation, optical functors, Julia

Concurrency

• Non-blocking transaction atomicity
• Existential Type Blog, Parallelism is not Concurrerncy

Monadic

• Okmij, Continuations and Delimited Control
• Partiality is an effect (they discovered Kleisli?)
• The Continuation Passing Transform and the Yoneda Embedding
• Oleg Kiselyov, Hiromi Ishii, "Freer Monads, More Extensible Effects"
• Zippers and Comonads
• Tim Perrett, Understanding the State Monad
• Simon PEYTON JONES, Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell
• Greg Meredith, CtrlShift
• Монады и Аппликативы (monads and applicatives, in Russian
• De Goes, No More Transformers: High-Performance Effects in Scalaz 8
• Yokota, Stacking Futures with Either
• Yokota, Monad Transformers
• Oleksandr Manzyuk, Calculating monad transformers with category theory
• [Lucius Gregory Meredith, Beyond the monadic API for delimited continuations(https://drive.google.com/file/d/0B5I9qM5f_1cfeGlMRUllMnRsZGc/view)
• Leinster, Where Do Monads Come From

Other links

• Railway-oriented programming
• Zraffer, linvect
• Exceeder, Presheaf.js
• de Goes, Tagless Horror
• de Goes, Effects without Transformers
• Shapeless Party Tricks in the Enterprise
• A.Konovalov
• A.Konovalov tweets
• The Scalable Commutativity Rule: Designing Scalable Software for Multicore Processors
• Styles of config propagation: Manual, Implicits, DynamicVariable, Reader
• Milewski, Tambara Modules
• Milewski, Profunctor Optics
• Tardis. Программируем на машине времени
• Theory of concatenative combinators
• Partial Evaluation and Automatic Program Generation
• adaptive lock-free maps
• From monoids to near-semirings: the essence of MonadPlus and Alternative
• Fun with semirings: a functional pearl on the abuse of linear algebra
• Ralf Hinze, Lifting Operators and Laws
• Extensibility for the Masses. Practical Extensibility with Object Algebras
• thedeemon. колдунство реификации
• The exp-log normal form of types
• Combining algebraic effects with continuations
• Y.Lafont, The linear abstract machine
• Pierre-Evariste Dagand, Conor McBride, Elaborating Inductive Definitions
• union types in C++
• Conor McBride, Turing-Completeness Totally Free
• functional TV
• S^m_n theorem (also called the translation lemma, parameter theorem, and the parameterization theorem) for a given programming language and positive integers m and n, there exists a particular algorithm that accepts as input the source code of a program with m + n free variables, together with m values. This algorithm generates source code that effectively substitutes the values for the first m free variables, leaving the rest of the variables free.
• Abstract Syntax and Variable Binding
• APLicative Programming with Naperian Functors - Jeremy Gibbons (video)
• Peeling the Banana: Recursion Schemes from First Principles - Zainab Ali (video)