Having an Effect

http://okmij.org/ftp/Computation/having-effect.html

https://www.youtube.com/watch?v=GhERMBT7u4w

This research has been a journey following the tantalizing lead: the founding papers on monads, monad transformers, free monads, and extensible-effects were all about extensible interpreters. Along the way, we have realized that the expression problem, stable denotations, and extensible interpreters are all different names for the same thing. We have eventually found the organizing principle: interaction -- between a client and a server, an interpreter, and the interpreted code, expression and its context.

It may well be that interaction is best expressed in a process calculus. In sequential calculi, Cartwright and Felleisen's ``Extensible Denotational Language Specifications'' is the earliest fully worked-out rigorous presentations of effects as interactions.

The talk gives the modern reconstruction of Cartwright and Felleisen's approach. Our reconstruction is simpler, aided by the tagless-final presentation, and immediately executable.

Developing further, we make the effect handlers themselves modular and extensible -- be part of a program rather than permanently stationed outside. This makes possible the following step:

Cartwright and Felleisen had to bake the variable environment into the basic semantic framework, even though integers, or first-order sub-languages in general, make no use of it. We avoid postulating the variable environment and any special treatment of higher-order. After all, we treat Lambda on par with the State, in the same uniform formalism. Dynamic or lexical binding or various calling conventions boil down to different ways of handling the effect of dereferencing a bound variable.

Revisiting the origins of the field and recovering the insights and forgotten alternatives help make our programs have the intended effect.

Effects for Efficiency

https://www.dhil.net/research/papers/effects_for_efficiency-draft-march2020.pdf

Asymptotic Speedup with First-Class Control

As Filinski showed in the 1990s, delimited control operators can express all monadic effects. Plotkin and Pretnar’s effect handlers offer a modular form of delimited control providing a uniform mechanism for concisely implementing features ranging from async/await to probabilistic programming.

We study the fundamental efficiency of delimited control. Specifically, we show that effect handlers enable an asymptotic improvement in runtime complexity for a certain class of programs. We consider the generic search problem and define a pure PCF-like base language λb and its extension with effect handlers λh. We show that λh admits an asymptotically more efficient implementation of generic search than any λb implementation of generic search. We also show that this efficiency gap remains when λb is extended with mutable state.

To our knowledge this result is the first of its kind for control operators.

Substructural Simple Type Theories for Separation and In-place Update

https://bentnib.org/thesis.pdf

This thesis studies two substructural simple type theories, extending the “separation” and “number-of-uses” readings of the basic substructural simply typed λ-calculus with exchange.

The first calculus, λsep, extends the αλ-calculus of O’Hearn and Pym by directly considering the representation of separation in a type system. We define type contexts with separation relations and introduce new type constructors of separated products and separated functions. We describe the basic metatheory of the calculus, including a sound and complete type-checking algorithm. We then give new categorical structure for interpreting the type judgements, and prove that it coherently, soundly and completely interprets the type theory. To show how the structure models separation we extend Day’s construction of closed symmetric monoidal structure on functor categories to our categorical structure, and describe two instances dealing with the global and local separation.

The second system, λinplc, is a re-presentation a of substructural calculus for in-place update with linear and non-linear values, based on Wadler’s Linear typed system with non-linear types and Hofmann’s LFPL. We identify some problems with the metatheory of the calculus, in particular the failure of the substitution rule to hold due to the call-by-value interpretation inherent in the type rules. To resolve this issue, we turn to categorical models of call-by-value computation, namely Moggi’s Computational Monads and Power and Robinson’s Freyd- Categories. We extend both of these to include additional information about the current state of the computation, defining Parameterised Freyd-categories and Parameterised Strong Monads. These definitions are equivalent in the closed case. We prove that by adding a commutativity condition they are a sound class of models for λinplc. To obtain a complete class of models for λinplc we refine the structure to better match the syntax. We also give a direct syntactic presentation of Parameterised Freyd-categories and prove that it is soundly and completely modelled by the syntax. We give a concrete model based on Day’s construction, demonstrating how the categorical structure can be used to model call-by-value computation with in-place update and bounded heaps.