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:

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:

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:

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:

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:

Resources:

Type Programming in Haskell

Papers:

Resources:

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:

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 Classes and Constraints

Haskell papers:

Haskell resources:

Generics

Papers:

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:

Programming Language Foundations

Resources:

Type Theory

Resources:

Lambda Calculus

Resources:

(Universal) Algebra

Resources:

Category Theory

Resources:

Statistics

Resources: