Literature Of Interest
This is a non-exhaustive, ongoing list of literature relevant to my research, of interest to me, or simply those I've found helpful as learning resources.
Algebraic Effect Calculus
Effect handler calculus by Sam Lindley, Ohad Kammar, and Daniel Hillerstrom:
- Row-based Effect Types for Database Integration - Sam Lindley, James Cheney (TLDI '12) [Lindley and Cheney 2012]. This presents the language Links, a call-by-value variant of System F with row polymorphism, row-based effect types, and implicit subkinding.
- Handlers in Action - Ohad Kammar, Sam Lindley (ICFP '13) [Kammar et al. 2013]. This presents a higher-order calculus of deep effect handlers called 𝜆_eff which extends Levy’s call-by-push-value [Levy 1999] as an underlying paradigm to include effect operations and effect handlers.
- Liberating Effects with Rows and Handlers - Daniel Hillerstrom, Sam Lindley (TyDe '16) [Hillerström and Lindley 2016]. This describes a calculus for extensible deep handlers called 𝜆^ρ_eff.
- Shallow Effect Handlers - Daniel Hillerstrom, Sam Lindley (APLAS '18) [Hillerström and Lindley 2018]. This describes a calculus called 𝜆^†, an extension of 𝜆^ρ_eff but with shallow handlers and recursive functions.
Effect handler calculus by Andrej Bauer and Matija Pretnar:
- Programming with Algebraic Effects and Handlers - Andrej Bauer, Matija Pretnar (JLAMP '12) [Bauer and Pretnar 2012]. This presents the programming language Eff based on the algebraic approach to computational effects, in which effects are modeled as algebraic operations of a suitably chosen algebraic theory, and effect handlers as homomorphisms induced by the universal property of free algebras. Eff supports first-class effects and handlers. This uses direct-style operation application.
- An Effect System for Algebraic Effects and Handlers - Andrej Bauer, Matija Pretnar (CALCO '13) [Bauer and Pretnar 2013]. This presents an effect system for the core of the language Eff , a simplified variant of Eff which is an ML-style language with first-class algebraic effects and handlers.
- An Introduction to Algebraic Effects and Handlers - Matija Pretnar (ENTCS '15) [Pretnar 2015]. This presents a tutorial on algebraic effects and handlers; it explains algebraic effects and handlers, defines an operational semantics and type & effect system, and shows how one can reason about effects.
- Algebraic Effects and Handlers - Andrej Bauer (OPLSS '18) [Bauer 2018]. These are notes and materials for lectures on algebraic effects and handlers at OPLSS 2018.
Effect handler calculus by Daan Leijen:
- Algebraic Effects for Functional Programming/Type Directed Compilation of Row-typed Algebraic Effects - Daan Leijen (POPL '17) [Leijen 2017], which defines rows based on Extensible Records with Scoped Labels [Leijen 2005]. This presents an overview of practical algebraic effects in the context of the language Koka, a strongly typed functional-style language with effect types and handlers. The language separates pure values from side-effecting computations, and implements effects as row-types.
- Effect Handlers, Evidently - Ninging Xie, Daan Leijen (ICFP '20) [Xie and Leijen, 2020]
Other effect calculus:
- Abstracting Algebraic Effects - Dariusz Biernacki et al. (POPL '19) [Biernacki et al. 2019]
- Handler Calculus - Sam Lindley ('21) [Lindley, 2021]
Theory/Properties of (Algebraic) Effects
Papers:
- Just do it: Simple Monadic Equational Reasoning - Jeremy Gibbons, Ralf Hinze (ICFP '11) [Wu et al. 2014]
- Effect Handlers in Scope - Nicolas Wu, Tom Schrijvers, Ralf Hinze (Haskell '14) [Wu et al. 2014]
- Syntax and Semantics for Operations in Scopes - Maciej Pirog, Tom Schrijvers, Nicolas Wu (PL '17) [Piroj 2017]
- Distributive Interaction of Algebraic Effects - Kwok-Ho Cheung (PhD Thesis, University of Oxford '17) [Cheung, 2017]
- What is Algebraic about Algebraic Effects and Handlers - Andrej Bauer (arXiv Notes '18) [Bauer, 2018]
- Algebraic Effect Handlers go Mainstream - Dagstuhl Seminar Report [2018]
- A Predicate Transformer Semantics for Effects - Wouter Swierstra and Tim Baanen (ICFP '19) [Swierstra and Baanen, 2019]
- Programming and Reasoning with Algebraic Effects and Effect Handlers - Oleg Kiselyov, Sam Lindley, Gordon Plotkin, Nicolas Wu ('19) [Kiselyov et al. 2019]
- Reasoning about Effect Interaction by Fusion - Zhixuan Yang, Nicolas Wu (ICFP '21) [Yang and Wu, 2021]
Effect Systems
Effect systems (and their papers):
- Monad Transformers and Modular Interpreters - Sheng Liang et al. (POPL '95) [Liang et al. 1995]. This is implemented as the transformers library (containing both concrete monad transformers and a type class for monad transformer), which is then followed up by the mtl library containing monad classes using functional dependencies inspired by [Jones. 1995].
- Extensible Effects, an Alternative to Monad Transformers - Oleg Kiselyov et al. (Haskell '13) [Kiselyov et al. 2013] This is implemented as earlier versions of the extensible-effects library.
- Freer Monads, More Extensible Effects - Kiselyov, Oleg, and Hiromi Ishii (Haskell '15). [Kiselyov and Ishii, 2015]. This is implemented as a series of libraries which are inspirations of the previous versions, in the following order: the extensible-effects library, the freer library, the freer-effects library, and then the freer-simple library.
- Fusion for Free: Efficient Algebraic Effect Handlers - Nicolus Wu and Tom Schrijvers (MPC '19) [Wu and Schrijvers, 2019]. This is implemented as the fused-effects library. There is a helpful talk "Building Haskell Programs with Fused Effects" by Patrick Thomson at Strange Loop Conference here.
- Polysemy - Sandy Maguire (2019). This is implemented as the polysemy library.
- Effects for Less - Alexis King (Zurihac '20) [King, 2020] (I've transcribed notes for this talk here). This is under construction, implemented as the eff library. The ghc proposal can be found here. This is inspired by extensible-effects, freer, fused-effects, and polysemy.
Other relevant papers on effect systems:
- Embedding effect systems in Haskell - Dominic Orchard, Tomas Petricek (Haskell '14) [Orchard and Petricek, 2014]
- Monad transformers and modular algebraic effects: what binds them together - Tom Schrijvers, Nicolas Wu et al. (Haskell '19) [Schrijvers et al. 2019].
Probabilistic Programming
General probabilistic programming papers:
- Probabilistic Functional Programming in Haskell (Pearl) - Martin Erwig and Steve Kollmansberger (JFP '06') [Erwig and Kollsmanberger, 2006] [Extended version: Thesis]
- Lightweight Implementations of Probabilistic Programming Languages Via Transformational Compilation - David Wingate, Andreas Stuhlmüller, Noah D. Goodman. (AISTATS '11) [Wingate et al. 2011, updated 2014]
- Particle Gibbs with Ancestor Sampling for Probabilistic Programs - Jan-Willem van de Meent et al. (AISTATS '15) [van de Meent. 2015]
- Semantics for Probabilistic Programming: Higher-order Functions, Continuous Distributions, and Soft Constraints - Sam Staton, Hongseok Yang, Frank Wood, Ohad Kammar (LICS '16) [Staton et al. 2016]
- Design and Implementation of Probabilistic Programming Language Anglican - David Tolpin et al. (IFL '16) [Tolpin et al. 2016]
- Composing Inference Algorithms as Program Transformations - Robert Zinkov and Chung-chieh Shan (arXiv preprint '16) [Zinkov and Shan. 2016]
- Automating Inference, Learning, and Design using Probabilistic Programming - Tom Rainforth (PhD Thesis, University of Oxford, '17) [Rainforth, 2017]
- Functional Probabilistic Programming for Scalable Bayesian Modelling (Probability Monad) - Jonathan Law and Darren J. Wilkinson (Alan Turing Institute '19) [Law and Wilkinson. 2019]
General probabilistic programming resources:
- A More Functional Future for Statistical Computing (Lecture Slides) - Darren Wilkinson (2020)
- Probabilistic Programming (Talk, POPL '20) - Hongseok Yang (2020)
Probability Theory in Probabilistic Programming
- Semantics for Probabilistic Programming: higher-order functions, continuous distributions, and soft constraints - Sam Staton, Chris Heunen, Ohad Kammar . ('16) [Staton, Heunen, Kammar. 2016]
- A Convenient Category for Higher-Order Probability Theory - Chris Heunen, Ohad Kammar, Sam Staton. ('17) [Heunen, Kammar, Staton. 2017]
- Commutative Semantics for Probabilistic Programming - Sam Staton (ESOP '17) [Staton. 2017]
- A Domain Theory for Statistical Probabilistic Programming - Matthijs Vakkar, Sam Staton, Ohad Kammar (POPL '19') [Vakkar, Staton, Kammar. 2019]
- Probabilistic Programs as Measures - Sam Staton (Chapter 2, Foundations of Probabilistic Programming '20) [Staton. 2020]
Probabilistic programming papers by/related to Adam Ścibior:
- Effects in Bayesian inference - Adam Ścibior and Ohad Kammar. (HOPE '15) [Ścibior and Kammar. 2015]
- Practical Probabilistic Programming with Monads - Adam Ścibior et al. (Haskell '15) [Ścibior et al. 2015]
- Composing Inference Algorithms as Program Transformations - Robert Zinkov and Chung-chieh Shan (arXiv preprint '16) [Zinkov and Shan. 2016]
- Combinators for Modeling and Inference - Eli Sennesh, Jan-Willem van de Meent, (PROBPROG '18) [Sennesh and van de Meent, 2018]
- Composing Modeling and Inference Operations with Probabilistic Program Combinators - Eli Sennesh, Adam Ścibior, Jan-Willem van de Meent. (NIPS '18) [Sennesh et al. 2018]
- Denotational Validation of Higher-Order Bayesian Inference - Adam Ścibior, Ohad Kammer, et al. (POPL) [Ścibior et al. 2018]
- Functional Programming for Modular Bayesian Inference - Adam Ścibior, Ohad Kammer, et al. (ICFP) [Ścibior et al. 2018]
- Formally Justified and Modular Bayesian Inference for Probabilistic Programs - Adam Ścibior (PhD Thesis) [Ścibior 2019]
Probabilistic programming papers by/related to Oleg Kiselyov:
- Embedded Probabilistic Programming - Oleg Kiselyov and Chung-chieh Shan. (IFIP DSL '09) [Kiselyov and Shan. 2009]
- Probabilistic Programming Language and its Incremental Evaluation - Oleg Kiselyov (ASPLS '16) [Kiselyov, 2016]
- Probabilistic Inference by Program Transformation in Hakaru - Praveen Narayanan, Chung-chieh Shan et al. (FLOPS '16) [Narayanan et al. 2016]
Effects in probabilistic programming:
- Effects in Bayesian inference - Adam Ścibior and Ohad Kammar. (HOPE '15) [Ścibior and Kammar. 2015]
- Effect Handling for Composable Program Transformations in Edward2 - Dave Moore, Maria Gorinova (PROBPROG '18) [Moore and Gorinova, 2018]
- Composable Effects for Flexible and Accelerated Probabilistic Programming in NumPyro - Du Phan et al. (arXiv preprint '19) [Phan et al. 2019]
- Automatic Reparameterisation of Probabilistic Programs - Maria I. Gorinova, Dave Moore, Matthew D. Hoffman (ICML '20) [Moore et al. 2020]
- Effect Handlers in Pyro - Pyro ('21)
- On Reinforcement Learning, Effect Handlers, and the State Monad - Ugo Dal Lago ('22)
Text books:
- An Introduction To Probabilistic Programming - Jan-Willem van de Meent et al [van de Meent et al. 2018]. This outlines the calculus and semantics for first-order probabilistic languages with graph-based and evaluated-based inference, and then higher-order probabilistic languages with evaluation-based inference. The approaches taken resemble that of Anglican. For graph-based inference, it covers the assignment of addresses (symbols) to nodes, compilation to graphical models, and semantics for evaluation/inference over graphical models. For evaluation-based inference, it covers an addressing transformaton of probabilistic operations, CPS transformations on probabilistic programs, and a message-interface coroutine-style for evaluation-based inference.
- Foundations of Probabilistic Programming - Gilles Barthe et al. (Cambridge University Press) [Barthe et al. 2020].
- Probabilistic Machine Learning: Advanced Topics - Kevin Patrick Murphy [Kevin Patrick Murphy. 2023].
Probability Theory in Programming
Papers:
- Semantics for Probabilistic Programming: Higher-order Functions, Continuous Distributions, and Soft Constraints - Sam Staton, Hongseok Yang, Frank Wood, Ohad Kammar (LICS '16) [Staton et al. 2016]
- Denotational Validation of Higher-Order Bayesian Inference - Adam Ścibior, Ohad Kammer, et al. (POPL '18') [Ścibior et al. 2018]
- Formally Justified and Modular Bayesian Inference for Probabilistic Programs - Adam Ścibior (PhD Thesis) [Ścibior 2019]
- Functional Probabilistic Programming for Scalable Bayesian Modelling (Probability Monad) - Jonathan Law and Darren J. Wilkinson (Alan Turing Institute '19) [Law and Wilkinson. 2019]
- A Domain Theory for Statistical Probabilistic Programming - Matthijs Vakar, Ohad Kammar (POPL '19) [Vakar and Kammar, 2019]
- Symbolic Disintegration with a Variety of Base Measures - Praveen Narayanan, Chung-chieh Shan (2020) [Narayanan and Shan, 2020]
Resources:
- Foundations of the Giry Monad (Probability Monad) - J Tobin (2017)
- Probabilistic Programming with Continuations - Jules Hedges (2020)
Functional Constructs and Abstractions
Papers:
- Applicative Programming with Effects (Pearl) - Conor Mcbride, Ross Paterson (JFP '08) [Mcbride and Paterson, 2008]
- Desugaring Haskell’s do-Notation into Applicative Operations - Simon Marlow, Simon Peyton Jones, Edward Kmett (Haskell '16) [Marlow et al. 2016]
- Capturing the Future by Replaying the Past (Pearl) - James Koppel et al. (ICFP '18) [Koppel et al. 2018]
- Selective Applicative Functors - Andrey Mokhov et al. (ICFP '19) [Mokhov et al. 2019]
Reasoning about Syntax and Semantics of Programs
Papers:
- Notions of Computations and Monads - Eugenio Moggi (IEEE Symposium '91) [Moggi, 1991]
Embedded Domain Specific Languages
Papers:
- Data types a la carte - Wouter Swierstra (JFP '08) [Swierstra, 2008]
- Typed Tagless Final Interpreters - Oleg Kiselyov (Springer '12) [Kiselyov, 2012] (Lecture Notes)
- Folding Domain-Specific Languages: Deep and Shallow Embeddings (Pearl) - Jeremy Gibbons and Nicolas Wu (ICFP '14) [Gibbons and Wu, 2014]
- Combining Deep and Shallow Embedding of Domain-Specific Languages - Josef Svenningsson and Emil Axelsson (CLSS '15) [Svenningsson and Axelsson. 2015]
- Embedding a Full Linear Lambda Calculus in Haskell - Jeff Polakov (Haskell '15) [Polakow, 2015]
Resources:
Type Programming in Haskell
Papers:
- Associated Type Synonyms - Manuel M. T. Chakravarty, Gabriele Keller, Simon Peyton Jones (ICFP '05) [Chakravarty et al. 2005]
- Constrained Type Families - J. Garret Morris and Richard Eisenberg (PACM '17) [Morris and Eisenberg. 2017]
- Higher-order Type-level Programming in Haskell - Csongor Kiss, Simon Peyton Jones et al. (ICFP '19) [Kiss et al. 2019]
- Type Your Matrices for Great Good - Armando Santos, José N. Oliveira (Haskell '20) [Santos and Oliveira. 2020]
Resources:
- Thinking with Types - Sandy Maguire (2019)
- Haskell Type-level Function Shenanigans - Antoine Leblanc (2020)
- Type Families in Haskell: The Definitive Guide - Vladislav Zavialov (2021)
- Haskell/GHC Reading List
Type Systems/Inference
General papers:
- Generalizing Hindley-Milner Type Inference Algorithms (Algorithm W and M) - Bastiaan Heeren, (Utrecht University '02) [Heeren et al. 2002]
- Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism - Jana Dunfield, Neelakantan R. Krishnaswami (ICFP '13) [Dunfield and Krishnaswami. 2013]. (DK type system)
- A Mechanical Formalization of Higher-Ranked Polymorphic Type Inference - Jinxu Zhao, Tom Schrijvers (ICFP '19) [Zhao et al. 2019]. (DK type system)
General resources:
- A Tutorial Implementation of a Dependently Typed Lambda Calculus - Andres Loh, Conor McBridge, Wouter Swierstra (2001)
Haskell papers:
- Functional Programming with Overloading and Higher-Order Polymorphism - Mark P Jones (AFP '95) [Jones. 1995].
- Typing Haskell in Haskell - Mark P Jones (Haskell '00) [Jones, 2000]
- System F with Type Equality Coercions - Martin Sulzmann, Simon Peyton Jones et al. (TLDI '07) [Sulzmann et al. 2007].
- Practical Type Inference for Arbitrary-rank Types - Simon Peyton Jones (JFP '07) [Jones et al. 2007].
- Extensions of Haskell's Type System - Matej Kollár (Masters Thesis, Masarykova University '11) [Kollár, 2011]
- Giving Haskell a Promotion - Brent Yorgey, Simon Peyton Jones et al. (TLDI '12') [Yorgey et al. 2012].
- Type Inference, Haskell and Dependent Types - Adam Michael Gundry (PhD Thesis, University of Strathclyde, '13) [Gundry, 2013].
- System FC, as implemented in GHC - Richard Eisenberg (Report, University of Pennsylvania, '15) [Eisenberg, 2015].
- Dependent Types in Haskell: Theory and Practice - Richard Eisenberg (PhD Thesis, University of Pennsylvania, '16) [Eisenberg, 2016].
- A Specification for Dependent Types in Haskell - Stephanie Weirich, Richard Eisenberg et al. (ICFP '17) [Weirich et al. 2027] (System DC)
- An Existential Crisis Resolved - Richard Eisenberg et al. (ICFP '21) [Eisenberg et al. 2021]
Haskell resources:
- Type Systems, HM Inference - Stephen Diehl, Write You a Haskell
- Haskell Type System Research Papers (Wiki)
- Haskell 2010 Language Report
- Haskell/GHC Reading List
Type Classes and Constraints
Haskell papers:
- Implementing Type Classes - John Peterson, Mark P Jones (ACM SIGPLAN '93) [Peterson and Jones. 1993]
- Type Classes in Haskell - Cordelia V Hall, Simon Peyton Jones et al. (TOPLAS '96) [Hall et al. 1996]
- Type Classes: An Exploration of the Design Space - Simon Peyton Jones et al. (Haskell '97) [Jones et al. 1997]
Haskell resources:
- Implementing and Understanding Type Classes - Oleg Kiselyov (Last updated May 3rd, '21)
- Type Class, Context Inference, & Dictionaries - Niki Vazou (CMSC498V, University of Maryland Lecture Notes)
- Type Class Instances for Type-Level Lambdas in Haskell - Thijs Alkemade and Johan Jeuring
- Type Classes - Tufts University Lecture Notes
- Haskell 2010 Language Report
- Haskell/GHC Reading List
Generics
Papers:
- Type-indexed Data Types - Ralf Hinze, Johan Jeuring, Andres Loh. (MPC '02) [Hinze et al. 2002]
- True Sums of Products - Edsko de Vries, Andrej Loh (WGP '14) [de Vries and Loh, 2014]
- Generic Deriving Of Generic Traversals - Csongor Kiss, Matthew Pickering, Nicolas Wu (ICFP '18) [Kiss et al. 2018]
- Generic Programming of All Kinds - Alejandro Serrano, Victor Cacciari Miraldo (Haskell '18) [Serrano and Miraldo, 2018]
Optics and Lenses
Papers:
- Symmetric Lenses - Martin Hofmann, Benjamin Pierce, Daniel Wagner (ACM SIGPLAN '11) [Hofmann et al. 2011]
- Profunctor Optics - Matthew Pickering, Jeremy Gibbons, Nicolas Wu (arXiv preprint '17) [Pickering et al. 2017]
- Applicative Bidirectional Programming - Kazutaka Matsuda and Meng Wang (JFP '18) [Matsuda and Wang, 2018]
- Introduction to Bidirectional Transformations - Faris Abou-Saleh, James Cheney, Jeremy Gibbons at el. (Springer '18) [Gibbons et al. 2018]
- Lenses and Learners - Brendan Fong, Michael Johnson. (BX '19) [Fong and Johnson. 2019]
- Composing Bidirectional Programs Monadically - Li-yao Xia, Dominic Orchard, and Meng Wang. (ESOP '19) [Xia et al. 2019]
Probabilistic Programming
Resources:
- An Introduction to Probabilistic Programming - Jan-Willem van de Meent, Hongseok Yang, Frank Wood(2018)
- Foundations of Probabilistic Programming - Gilles Barthe, Alexandra Silva (2020)
Programming Language Foundations
Resources:
- Types and Programming Languages - Benjamin Pierce (2002)
- Programming Languages - Harvard Lecture Notes (2015)
- Practical Foundations For Programming Languages 2nd edition - Bob Harper (2016)
- Practical Foundations For Programming Languages Lecture Notes - Bob Harper (2021)
Type Theory
Resources:
- Martin-Lof's Type Theory - Martin-Lof (1980)
- Programming in Martin-Lof's Type Theory - Bengt Nordstrom, Oxford University Press (1990)
- Type Theory & Functional Programming - Simon Thompson (1999)
- Dependent Types at Work - Ana Bove and Peter Dybjer, Chalmers University (2008)
- Dependently Typed Programming in Agda - Ulf Norell and James Chapman, Chalmers University (2008)
- Homotopy Type Theory - The Univalent Foundations Program Institute for Advanced Study (2013)
- Programming Language Foundations in Agda - Philip Wadler, University of Edinburgh (2018)
- An OK Version of Type Theory - Jonathan Sterling (2020)
- Tao of Types - Thorsten Altenkirch, Midlands Graduate School (2021)
Lambda Calculus
Resources:
- On Understanding Types, Data Abstraction, and Polymorphism - Luca Cardelli (1985)
- A Tutorial Implementation of a Dependently Typed Lambda Calculus - Andres Loh, Conor McBridge, Wouter Swierstra (2001)
- Lambda Calculus and Types - Andrew D. Ker, Oxford University (2009)
- Lambda Calculus including Untyped, Simply-Typed, System F, as well as reductions, propositional logic, and curry-howard isomorphism - Peter Selinger, Dalhousie University (2013)
- Simply Typed Lambda Calculus, System F, and System Fω - Cambridge University Lecture Notes (2015)
(Universal) Algebra
Resources:
- A Course in Universal Algebra - Stanley Burris (1981)
- Universal Algebra for Computer Scientists - Eric G Wagner (1992)
- Algebras - Oleg Kiselyov (2019)
Category Theory
Resources:
- Category Theory Lecture Notes - Daniele Turi, University of Edinburgh (2001)
- Category Theory - Steve Awodey, Carnegie Mellon University (2006)
- Category Theory 101 - Gérard P. Michon (2010)
- Introduction to Category Theory - Graham Hutton, University of Nottingham (2014)
- Basic Category Theory - Tom Leinster, University of Edinburgh (2016)
- Category Theory for Programmers [Lectures]- Bartosz Mileswki (2019)
- Categories for the Lazy Functional Programmer (MGS Lecture Notes) - Thorsten Altenkirch, University of Nottingham (2019)
- Monads in Haskell and Category Theory - Samuel Grahn (2019)
- Monads, Algebras, Adjunctons, and Probability Monads - Julian Asilis, Harvard University (Thesis, 2020)
Statistics
Resources:
- Bayesian Theory C: 316 (Wiley Series in Probability and Statistics) - Jose Bernado (1994)
- Biological Sequence Analysis - R. Durbin et al. (1998)
- Bayesian Data Analysis, 3rd Edition - Andrew Gelman et al. (2013)
- Statistical Rethinking - Richard McElreath (2019)
- Bayesian Workflow Analysis - Andrew Gelman et al. (2020)