# Literature Of Interest

A non-exhaustive ongoing stack of literature that I've found interesting/helpful, or that I wish to absorb at some point in the future.

#### 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]
- 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 - Nicolas Wu and Tom Schrijvers (MPC '19) [Wu and Schrijvers. 2019] & Effect Handlers in Scope - Nicolas Wu, Tom Schrijvers, Ralf Hinze (Haskell '14) [Wu et al. 2014]. 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:

- Backtracking, Interleaving, and Terminating Monad Transformers (LogicT) - Functional Pearl (ICFP '05) [Kiselyov et al. 2005]
- 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)