Minh Nguyen

Minh Nguyen

PhD Student researching Programming Languages at University of Bristol

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:

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:

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:

  • 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:

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: