PaperlayerView exact revision on arXiv

Source-linked AI summary

Do be do be do

Sam Lindley, Conor McBride, Craig McLaughlin

arXiv:1611.09259v2cs.PL

TL;DR

Frank addresses how purity and effects can be managed locally in functional programming. It generalizes function application into operators that handle effects, then gives Core Frank a small-step semantics and type-soundness result.

  • Problem

    How to make purity a local choice when writing programs involving effects?

    Source: §1 · p. 1

  • Method

    Frank uses operators to generalize function application for locally managed effects, with effect polymorphism based on ambient abilities.

    Source: §2.6 · p. 4, §10 · p. 14

  • Results

    Core Frank is given a small-step operational semantics with a type-soundness theorem.

    Source: §1 · p. 1, §5 · p. 11

  • Takeaways & Limitations

    Programmers rarely need to read or write effect variables in Frank's lightweight effect polymorphism.

    Source: §2.4 · p. 3, §10 · p. 14

    Pattern matching elaboration is not optimized, and column reordering is not generally valid because forwarding order is left-to-right.

    Source: §4.1 · p. 10

Abstract

from arXiv · show

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 simply the special case of a Frank operator that interprets no commands. Moreover, Frank's operators can be multihandlers which simultaneously interpret commands from several sources at once, without disturbing the direct style of functional programming with values. Effect typing in Frank employs a novel form of effect polymorphism which avoid mentioning effect variables in source code. This is achieved by propagating an ambient ability inwards, rather than accumulating unions of potential effects outwards. We introduce Frank by example, and then give a formal account of the Frank type system and its semantics. We introduce Core Frank by elaborating Frank operators into functions, case expressions, and unary handlers, and then give a sound small-step operational semantics for Core Frank. Programming with effects and handlers is in its infancy. We contribute an exploration of future possibilities, particularly in combination with other forms of rich type system.

1. Introduction

Frank makes purity a local choice in a strict functional language with a bidirectional effect type system. Its operators unify functions and effect handlers, while its effect polymorphism avoids explicit effect variables and its Core Frank semantics is proved type sound.

1. Introduction

  • Frank operators generalize functions by interpreting commands, and multihandlers can interpret commands from several computations simultaneously.A function is the special case whose handled command set is empty; n-ary functions similarly handle no commands.Source: §1 · p. 1
  • Frank combines a bidirectional effect type system with effect handlers in a strict functional language, building on algebraic effects and handler abstractions.Abilities denote permission to invoke specified commands; handlers interpret effects while keeping interfaces separate from implementations.Source: §1 · p. 1
  • Ambient abilities enable effect polymorphism without requiring effect variables in source code.An operator's effects are instantiated with the ambient ability: the effects permitted by the current typing context.Source: §1 · p. 1
  • The paper elaborates Frank operators into Core Frank and gives that language a small-step operational semantics with a type-soundness proof.Core Frank uses functions, case expressions, and unary handlers.Source: §1 · p. 1
  • The paper explores future combinations of effect-handler programming with substructural typing, dependent types, and totality.Source: §1 · p. 1
  • Unlike Eff's original version, Frank statically tracks effects; other compared languages either lack effect typing or do not omit effect variables to the same extent.The paper also contrasts Frank's bidirectional typing and multihandlers with other languages' Hindley-Milner inference and lack of multihandlers.Source: §1 · pp. 1–2

2. A Frank Tutorial

Frank separates values from computations and uses effect-polymorphic operators to support direct-style programming. Its tutorial develops ordinary functional programming, ambient-ability typing, and evaluation control.

2. A Frank Tutorial

  • Frank distinguishes concrete values from computations, representing suspended computations with braces and separating computation types from value types.Its type system is inspired by call-by-push-value.Source: §2 · p. 2, §2.2 · p. 2

2.1 Data Types and First-Order Functions

  • Pattern matching over inductive data types supports ordinary first-order functions, with signatures requiring parametric polymorphism over free type variables.Constructors are distinct from functions and must be fully applied.Source: §2.1 · p. 2

2.2 Effect Polymorphism in Ambient Silence

  • An empty ability bracket denotes the ambient ability, allowing `map` to pass that ability to its element operator without explicit effect variables.This makes the example `map` effect-polymorphic while retaining control over effects.Source: §2.2 · p. 2

2.3 Controlling Evaluation

  • Frank’s left-to-right call-by-value evaluation requires explicit suspension when an operator must avoid evaluating an argument before choosing it.For a conditional, the branches are suspended so only the selected computation is run.Source: §2.3 · pp. 2–3

2.4 Abilities Collect Interfaces; Interfaces Offer Commands

Frank abilities collect interfaces that specify available commands, and the ambient ability determines which commands computations may use. This supports direct-style effectful programs, while the language’s fixed evaluation order supplies the sequencing that avoids explicit monadic plumbing.

2.4 Abilities Collect Interfaces; Interfaces Offer Commands

  • An ability is a collection of parameterized interfaces offering commands, and a computation’s type specifies the ability it requires.Effect polymorphism lets `map` pass its ambient ability to its computation argument; a computation whose peg omits a required ability does not typecheck.Source: §2.4 · p. 3

2.5 Direct Style for Monadic Programming

  • Frank permits direct application and case analysis across effectful computations, avoiding explicit sequencing and value plumbing in examples such as recursively concatenating received lists.This relies on Frank’s fixed evaluation order; the text notes that effectful code in Haskell must be explicitly sequentialized.Source: §2.5 · pp. 3–4

2.6 Handling by Application

Frank makes effect handling part of ordinary function application: operators can interpret commands offered by their arguments while retaining direct-style value programming. Its multihandlers coordinate multiple computations at once, as illustrated by a pipe that routes sends and receives between producer and consumer.

2.6 Handling by Application

  • Frank operators handle effects through ordinary application, with functions as the special case that handles no commands.The state example shows an operator receiving a state value and a computation that may issue state commands.Source: §2.6 · p. 4
  • Frank’s shallow continuations capture only the remaining subordinated computation, letting the state operator update state before explicitly reinvoking the continuation.Unlike deep continuations, invoking them does not implicitly reinvoke the handler.Source: §2.6 · p. 4

2.7 Handling on Multiple Ports

  • N-ary operators offer different ambient-ability adjustments at different ports, allowing a pipe to handle producer sends and consumer receives simultaneously.The pipe type advertises Send X on its first port and Receive X on its second.Source: §2.7 · p. 4
  • The pipe routes each send to the receiver and resumes both continuations with the sent value; if the producer stops before a receive, it invokes Abort for a broken pipe.If the consumer returns first, the producer can be discarded.Source: §2.7 · pp. 4–5
  • In the spacer example, the outer pipe handles receives and the inner pipe handles sends, and reversing the composition also works, making pipe associative.The example composes a spacer with producer and consumer computations.Source: §2.7 · p. 5
  • Simultaneous handling adds no capability beyond mutually recursive unary handlers, but Frank’s pipe definition is more direct than the compared implementations.The cited comparison says those implementations require suspended computations, and the deep implementation also uses a mutually recursive data type.Source: §2.7 · p. 5
  • A port adjustment specifies exactly which effects the operator handles there, so pipe cannot intercept Abort unless a port advertises it.Unadvertised commands are forwarded transparently; the pipe may still ignore a continuation to prevent an action.Source: §2.7 · p. 5

2.8 The Catch Question

Frank’s catch handler makes the alternative computation’s permission to abort depend on whether catch itself may abort, while trapping abort only in its first input. More generally, Frank writes operator handling directly over values and commands, with forwarding machinery handled by the semantics.

2.8 The Catch Question

  • Unlike a typical prioritized-choice type for exceptions, Frank does not require the ambient ability to include Abort when catch runs.The cited comparison says the Haskell mtl type makes abort non-local, and notes a similar observation for Koka [29].Source: §2.8 · p. 5
  • Frank’s catch permits the alternative computation to abort if and only if catch itself is permitted to abort, while trapping abort only in its first input.The alternative is suspended so it can be chosen only on failure, and its tail call runs outside catch’s scope.Source: §2.8 · p. 5

2.9 The Disappearance of Control

  • Frank handlers do not abstract over computations or use computation-to-computation handler types distinct from value-to-computation function types.The passage contrasts this with free-monad variations [6].Source: §2.9 · p. 5
  • Frank operators act on values directly, while the semantics maps computation trees to computation trees and forwards unhandled commands with wrapped continuations.The forwarding machinery is made explicit in the later elaboration and operational semantics.Source: §2.9 · p. 5

3. A Frank Formalism

The formal account distinguishes value and computation types and describes operator inputs with ports and outputs with pegs. Its bidirectional rules track commands through ambient abilities, while invisible effect-variable syntax keeps source signatures concise.

Types

  • Frank computation types combine input ports, whose adjustments specify handled effects, with an output peg that specifies the result value and its possible effects.All ports are handled simultaneously.Source: §3.1 · p. 6

3.1 Syntax

  • The implicit effect variable ε is fresh for each type signature and omitted from Frank source code, though effect variables remain explicit in the abstract syntax and type system.The source convention avoids writing ε in a program.Source: §3.1 · p. 6
  • Abilities may be open or closed, permit repeated interfaces with the rightmost instance overriding earlier ones, and can be modified by adjustments that extend them.A closed ability can be used to enforce purity.Source: §3.1 · p. 6

Terms

  • Frank’s syntax distinguishes values, computations, patterns, and operators’ command-request patterns, with request patterns binding command arguments and a continuation.A catch-all computation pattern can match any value or handled command.Source: §3.1 · p. 6, Terms · p. 6

3.2 Typing Rules

  • The POLYVAR rule instantiates type and effect variables by substitution, while COMMAND looks up a command in the ambient ability.Applications require the operator’s output ability to match the ambient ability and check each argument under its adjusted ability.Source: §3.2 · p. 7
  • Frank’s computation rule requires clauses to cover all possible values at the ports, and pattern elaboration supplies an algorithm for checking that coverage.Request patterns must use commands included in the port adjustment; catch-all patterns apply the adjustment to the ambient ability.Source: §3.2 · p. 8
  • The revised POLYVAR rule permits multiple effect variables in data types because exact ambient matching in the application rule makes relaxing the earlier restriction safe.An earlier draft restricted the implicit effect variable to the ambient ability and limited data types to one effect variable.Source: §3.2 · pp. 7–8

4. Core Frank

Core Frank provides a target language for implementing Frank operators with call-by-value functions, case analysis, and unary handlers. Its elaboration supplies ambient abilities to computations and compiles pattern matching into those constructs, while the procedure also exposes coverage, redundancy, and efficiency constraints.

4.1 Elaboration

  • Deep pattern matching across multiple computations elaborates to trees of unary handlers and case statements, while shallow computation and value patterns elaborate to handlers and case analysis respectively.Other pattern types produce neither eliminator, and empty pattern lists return the clause body.Source: §4 · p. 8, §4.1 · p. 9

4. Core Frank

  • Core Frank replaces operators with n-ary call-by-value application, lambda abstractions, case statements, and unary handlers, while making polymorphic instantiation explicit.Its computation types take value types to a peg, unlike Frank computation types, which take ports to a peg.Source: §4 · p. 8

4.1 Elaboration

  • Computation types are translated by supplying the ambient ability to each port, and each port becomes a suspended computation with that ability extended by its adjustment.Computation translation also supplies the ambient ability to the translated computation.Source: §4.1 · pp. 8–9
  • Pattern matching elaboration is not optimized for efficiency, and column reordering is invalid in general because implicitly forwarded ambient commands are forwarded left-to-right.The elaboration procedure is described as direct, with standard optimization techniques requiring care.Source: §4.1 · p. 10

4.2 Incomplete and Ambiguous Pattern Matching as Effects

  • PE checks pattern coverage and redundancy: incomplete coverage makes it undefined on three empty lists, while redundancy occurs when its final defining case is invoked with clauses remaining.Incomplete or ambiguous pattern matching mediated by effects is proposed as a possible extension.Source: §4.2 · p. 10

5. Small-Step Operational Semantics

The paper gives Core Frank a small-step semantics for n-ary call-by-value evaluation with shallow handlers, and proves subject reduction and type soundness. Well-typed closed computations either reach a value or stop at an unhandled command permitted by the ambient ability.

5. Small-Step Operational Semantics

  • Core Frank uses n-ary call-by-value evaluation and shallow handlers, whose continuations do not reinvoke the handler; this differs from the call-by-push-value calculus λeff with deep handlers.The difference in evaluation style also gives Core Frank more kinds of evaluation context.Source: §5 · p. 10
  • Handler reductions substitute returned values into the return clause and dispatch commands to clauses after capturing the continuation up to the current handler.The command rule selects the nearest enclosing handler with a clause for that command.Source: §5 · p. 11
  • Both uses and constructions preserve their inferred or checked type under reduction, respectively.This is the subject-reduction theorem.Source: §5 · p. 11
  • A normal construction is either a value or an evaluation context containing an unhandled command instance permitted by the ambient ability.The semantics therefore treats an unhandled permitted command as a stopping form.Source: §5 · p. 11
  • Well-typed closed Core Frank constructions either are normal with respect to the ambient ability or can take a type-preserving step; with an empty ability, normal forms are values.This is the stated type-soundness result.Source: §5 · p. 11

6. Computations as Data

Ability-parameterized data types let Frank store suspended computations, enabling a log-based rollback handler for a parser. The example also exposes limits in controlling command access and configuring top-level interfaces.

Computations as Data

  • Ability-parameterized data types let Frank store suspended computations, with the log implicitly parameterized by the ability of those computations.The log stores the parser computation and, after input, its continuation so that it can be replayed if the character changes.Source: §6 · p. 11
  • The rollback log records input continuations but need not store output continuations, because output returns Unit and cannot affect parser behavior.Rollback undoes output with backspace, a blank, and another backspace; after a first peek, it clears the buffer and reinvokes the old continuation after a new peek.Source: §6 · pp. 11–12
  • A one-character buffer and log let a handler implement modular rollback while interpreting parser lookahead, abort, and console commands.The parser may reject input by aborting, and the handler then rejects the character that caused the rejection.Source: §6 · p. 12
  • The example parser counts zeros until a space and aborts on other input, using one-step lookahead to inspect and then accept characters.The top-level built-in Console handler interprets input and output as actual character I/O.Source: §6 · pp. 11–12
  • Frank currently supports only a limited range of built-in top-level interfaces, though adding more and connecting them to external APIs is envisioned.The program's external ability can configure the runtime to its execution context.Source: §6 · p. 12
  • Frank cannot currently prevent the parser from accessing Console commands because ability adjustments can add or shadow interfaces but not remove them.Negative adjustments could express the desired restriction, but their effect on effect polymorphism remains unclear.Source: §6 · p. 12

7. Implementation

The authors implemented a Frank prototype in Haskell that matches the paper's design, using existing parsing and type-inference technologies. Its backend translates to Shonky rather than the formal Core Frank calculus.

Implementation

  • A Haskell prototype implements the Frank design described in the paper, building on existing parsing, type-inference, and Shonky technologies.The prototype was developed to build rapidly.Source: §7 · p. 12
  • Frank's indentation-sensitive parser uses Trifecta with an extension that gives indentation-sensitive parsing a formal semantics.The extension separates indentation handling as much as possible from parsing.Source: §7 · p. 12
  • Bidirectional typechecking uses type-inference-in-context, which tracks term and unification variables and restricts later bindings to depend only on earlier ones.The technique has also been shown to scale to dependently typed settings.Source: §7 · p. 12
  • The prototype backend translates Frank to Shonky, an untyped version of Frank, rather than to the formal Core Frank calculus.Shonky executes code directly through an abstract machine.Source: §7 · p. 12

8. Related Work

Related work spans effect-handler implementations, alternative effect abstractions, and applications of handlers. The approaches differ in implementation efficiency, programming style, and the effect systems they support.

Efficient Effect Handler Implementations

  • Free monads are a natural handler implementation, but direct use can be inefficient; other approaches optimize deep or shallow handlers and continuations.Examples include fusion for deep handlers, optimized operation sequences for shallow handlers, and stack-based continuations in Multicore OCaml.Source: §8 · p. 13

Layered Monads and Monadic Reflection

  • Monadic reflection composes effects by interpreting monadic computations in other monadic computations, unlike handlers that interpret operations.Swamy et al. provide direct-style effectful programming for a strict language using monad transformers rather than handlers.Source: §8 · p. 13

Variations and Applications

  • Comparative studies examine handler expressiveness against monad transformers, and handlers against monadic reflection and delimited control.Source: §8 · p. 13
  • Other work adapts handlers to idioms and arrows, studies scoped handlers, and applies handlers to logic programming.Scoped handlers address modularly weaving handlers through computations whose commands may themselves be parameterized by computations.Source: §8 · p. 13

9. Future Work

The paper outlines future work spanning semantics, language design, and richer disciplines for effects and computation. Proposed directions include improving control over effects and addressing termination, productivity, and interaction protocols.

Direct Semantics

  • A direct semantics could improve implementation efficiency or generated code, while clarifying how multihandlers relate to multiple dispatch and join patterns remains open.Source: §9 · p. 13

Verbs versus Nouns; Data as Computations

  • The language could add syntax conveniences and encode data types as interfaces, with constructors represented by commands.The paper sketches list encoding and a map operation over that representation.Source: §9 · p. 13

Failure and Choice in Pattern Matching

  • Failure and choice in pattern matching could be effects, letting custom handlers choose how to navigate the resulting search space.Source: §9 · p. 13

Scaling by Naming; Dynamic Effects; Negative Adjustments

  • Future effect work includes naming multiple State components, supporting dynamic reference allocation, and adding negative ability adjustments.The impact of negative adjustments on effect polymorphism remains unclear.Source: §9 · pp. 13–14

Controlled Snooping; Indexed Interfaces; Session Types as Interface Indices

  • Possible interaction features include transparent command trapping, state-indexed interfaces, and session-state indices that enforce matching requests in coordinating multihandlers.Source: §9 · p. 14

Substructural Typing for Honesty with Efficiency

  • Substructural typing could control continuation use, avoiding unnecessary continuation construction or storage and constraining message dropping or resending.For example, an aborted computation will not resume, while State handlers usually invoke continuations exactly once.Source: §9 · p. 14

Modules and Type Classes

  • The formal relationship between Frank's effect interfaces and modularity mechanisms such as ML modules and Haskell type classes remains to be established.Source: §9 · p. 14

Totality, Productivity, and Continuity

  • A totality and continuity discipline for computation trees could address termination and productivity, including deadlock and livelock risks.The paper identifies guarded recursion as a promising way to capture these requirements.Source: §9 · p. 14

10. Conclusion

Frank generalizes function application to effect-handling operator application, with a type system that tracks permitted effects and syntax supporting lightweight effect polymorphism. The authors hope it will support real-world programs involving interaction and control structures.

10. Conclusion

  • Frank generalizes function application to n-adic operator application, allowing an operator to handle effects performed by its arguments.Source: §10 · p. 14
  • Its effect type system tracks permitted effects, while syntactic sugar lets programmers use effect polymorphism without often handling effect variables directly.Source: §10 · p. 14
  • The authors hope Frank can support real-world programs involving interaction and control structures, including language elaborators, educational websites, and multi-actor systems.Source: §10 · p. 14
Loading 1611.09259v2…