Automatic Differentiation via Effects and Handlers: An Implementation in Frank

Do be do be do

We explore the design and implementation of Frank, a strict functional programming language with a bidirectional effect type system designed from the ground up around a novel variant of Plotkin and Pretnar's effect handler abstraction. Effect handlers provide an abstraction for modular effectful programming: a handler acts as an interpreter for a collection of commands whose interfaces are statically tracked by the type system. However, Frank eliminates the need for an additional effect handling construct by generalising the basic mechanism of functional abstraction itself. A function is simpl…

验证基于效应处理程序的按定义运行反向模式自动微分库

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library

本文研究基于效应处理程序的按定义运行反向模式自动微分库的验证，通过分离逻辑提供机器检查的正确性证明。

Composable Effects for Flexible and Accelerated Probabilistic Programming in NumPyro

NumPyro is a lightweight library that provides an alternate NumPy backend to the Pyro probabilistic programming language with the same modeling interface, language primitives and effect handling abstractions. Effect handlers allow Pyro's modeling API to be extended to NumPyro despite its being built atop a fundamentally different JAX-based functional backend. In this work, we demonstrate the power of composing Pyro's effect handlers with the program transformations that enable hardware acceleration, automatic differentiation, and vectorization in JAX. In particular, NumPyro provides an iterati…

有效语言的反向传播 I：有限概率和离散输出代数效应

Backpropagation for Effectful Languages I: Finite Probability and Discrete Output Algebraic Effects

研究离散概率程序的反向模式自动微分，基于CHAD框架，以有限原子分布单子为例，定义反向模式代码变换并证明其正确性，为离散输出代数效应微分提供可复用模式，是扩展CHAD的基础步骤。