Ambient Values, Functions, and Control

Shonan, March 2019

Daan Leijen
Microsoft Research
Jonathan Brachthäuser
Universität Tübingen

Overview

We show three new language features, namely ambient values, functions, and control.

  • All three can be expressed by algebraic effect handlers.

  • We argue that these concepts merit study by themselves to make it easier to reason about programs and provide efficient implementations.

ambients relate to effect handlers as “while” to “goto” ;-)

The Problem

We assume a pretty printing library that produces pretty strings from documents: 

fun pretty( d : doc ) : string

Unfortunately, it has a hard-coded maximum display width deep within the code: 

... if (line.length ≤ 78) then ...

To abstract over the maximum display width, we can:

  • make the width into a global mutable variable,
  • or add an extra explicit width parameter to nearly every function in the library and thread it around manually.

We need something that is neither global nor local.

Ambient Values

We can declare the type of an explicit value as: 

ambient val width : int

and can refer to it deep inside the library: 

... if (line.length ≤ width) then ...

Tracking Ambient Values

The type system tracks the use of ambient values in row types denoted between angled brackets: 

fun pretty( d : doc ) : 〈width〉 string

signifying that pretty can only be used in a context that binds the ambient width value.

Binding Ambient Values

Ambient values are bound using with expressions: 

fun pretty-thin( d : doc ) : 〈〉 string {
  with val width = 40 in pretty(d)
}

Here the ambient value width is dynamically bound to 40 for the dynamic extent evaluating the body expression pretty(d). The scope of the with-binder is not limited to its lexical closure.

With as a Statement

There is also a statement form of the with expression that scopes over the rest of the current lexical block scope. Using this form we can write the previous example as: 

fun pretty-thin(d) {
  with val width = 40
  pretty(d)
}

Rebinding

we can also re-bind ambient values. For example we might want to pretty print part of a document in half the available display width: 

fun pretty-wide( d : doc ) : 〈width〉 string {
  with val width = width * 2
  pretty(d)
}

Here, the type of pretty-wide reflects that even though it binds width, it also still depends on a width binding in its own context.

Semantics of Ambient Values

\[\begin{mdmathpre}%mdk \gray{\mathkw{with}~\mathkw{val}~\mathid{p}~=~\mathid{v}~\mathkw{in}~\mathsf{\mathsf{E}}}[\mathid{p}]~~{\longrightarrow}~~\gray{\mathkw{with}~\mathkw{val}~\mathid{p}~=~\mathid{v}~\mathkw{in}~\mathsf{\mathsf{E}}}[\mathid{v}]~\quad\textrm{if}~\mathid{p}\notin \mathkw{bp}(\mathsf{\mathsf{E}})~~ \end{mdmathpre}%mdk \]

Where an ambient binding $\mathpre{\mathid{p}}$ finds its bound value $\mathpre{\mathid{v}}$ in the dynamic evaluation context $\mathpre{\mathsf{\mathsf{E}}}$ (i.e. the stack). The innermost binding is used due to the side condition $\mathpre{\mathid{p}\notin \mathkw{bp}(\mathsf{\mathsf{E}})}$ which ensures that $\mathpre{\mathid{p}}$ is not bound in $\mathpre{\mathsf{\mathsf{E}}}$ itself.

The semantics for ambient values as exactly the same as of dynamic binding described by Moreau (1998) and Kiselyov, Shan, and Sabry (2006).

Dynamic Binding

We can see that ambient values cannot be freely α-renamed, as they are bound dynamically at evaluation time by the innermost binding. Consider the following function: 

fun scope() {
  with val width = 78 
  val g = fun() { with val width = 80 in width + 1 }
  val h = with val width = 80 in (fun(){ width + 1 })
  g().println
  h().println
}

Ambient Function Values

Of course we can bind functions as an ambient value. For example, 

ambient val emit-naive : ((s : string) → 〈〉 ())

where the pretty printing library functions can use this to emit partial output: 

  ...
  match(doc) {
    Text(s) → emit-naive(s)

Too Limiting

Unfortunately, the ambient value declaration has a type signature that severely limits the number of possible implementations. For example, we might want to use the display width in an implementation like: 

with val emit-naive = (fun(s : string){ ... s.truncate(width) ... })
...

A Workaround?

We can of course change the type signature of the value declaration to: 

ambient val emit-naive : ((s : string) → 〈width〉 ())

But now the signature exposes accidental details of our particular implementation. Even worse, it might not be the desired semantics, since the width is dynamically bound at the call site of emit-naive, while we usually want to bind it at the definition site and encapsulate this in the definition of emit-naive.

Effects are not Encapsulated

Not only ambient bindings are resolved at the call-site – the same problem extends to other side-effects: 

with val emit-naive = (fun(s){ println(s) })

  • What if println happens to throw an exception?

  • The effects and ambient bindings still leak into the calling context.

Ambient Functions

What we need instead are ambient functions: such functions are bound dynamically, but evaluated in the lexical context of their binding. Similar to ambient values, we can declare an ambient function as: 

ambient fun emit( s : string ) : ()

There is no syntactic difference between calling an ambient functions and calling any other function. The inferred type of pretty now becomes: 

fun pretty( d : doc ) : 〈width,emit〉 ()

Dynamic binding with Lexical Scoping

fun pretty-thin(d) {
  with val width = 40
  with fun emit(s) { println(s.truncate(width)) }
  pretty(d)
}

Note that emit's body executes in the lexical context of pretty-thin and not in its calling context.

  • The ambient value width in the body of emit is now always resolved to 40 no matter if width is rebound inside pretty.
  • Any exception thrown by println is handled by the innermost exception handler around pretty-thin, not by some handler inside pretty.

Semantics of Ambient Functions

\[\begin{mdmathpre}%mdk \gray{\mathkw{with}~\mathkw{fun}~\mathid{p}(\mathid{x})~=~\mathid{e}~\mathkw{in}~\mathsf{\mathsf{E}}}[\mathid{p}(\mathid{v})]~~\\ \mdmathindent{4}{\longrightarrow}~~(\lambda \mathid{y}.~\gray{\mathkw{with}~\mathkw{fun}~\mathid{p}(\mathid{x})~=~\mathid{e}~\mathkw{in}~\mathsf{\mathsf{E}}}[\mathid{y}])(\mathid{e}[\mathid{x}:=\mathid{v}])~\quad\textrm{if}~\mathid{p}\notin \mathkw{bp}(\mathsf{\mathsf{E}}) \end{mdmathpre}%mdk \]

In contrast to the ambient value rule, we first evaluate the function body $\mathpre{\mathid{e}}$ with $\mathpre{\mathid{x}}$ substituted by $\mathpre{\mathid{v}}$ outside the calling evaluation context $\mathpre{\mathsf{\mathsf{E}}}$, and only after that resume in the original context with the result $\mathpre{\mathid{y}}$.

Local State

Continuing with our example, we may want to collect all output using local mutable state: 

fun emit-collect(action) {
  var out := ""
  with fun emit(s) { out := out + s + "\n" } in action()
  out
}

Note how we fully encapsulated the local state. Both the action and emit-collect do not have observable state effects.

Effectively, the ambient provides a secret channel to mutate state in the local lexical scope.

Depth-first Traversal

Example from Lewis, Launchbury, Meijer, and Shields (2000). 

alias vertex = int
type graph { ... } 
type rose  { Rose(v : vertex, sub : list〈rose〉 ) }

ambient fun marked( v : vertex ) : bool
ambient fun mark( v : vertex ) : ()
ambient fun children( v : vertex ) : list〈vertex〉

Depth-first Traversal 2

fun dfs( g : graph, vs : list〈vertex〉 ) : list〈rose〉 {
  var visited := vector(g.bound,False)
  with fun children(v) { g.gchildren(v) }
  with fun marked(v)   { visited[v] }
  with fun mark(v)     { visited[v] := True }
  dfs-loop(vs)
}
fun dfs-loop( vs : list〈vertex〉 ) {
  match(vs) {
    Nil → Nil
    Cons(v,vv) →
      if (marked(v)) then dfs-loop(vv) else {
        mark(v)
        val sub = dfs-loop( children(v) )
        Cons( Rose(v,sub), dfs-loop(vv) )
      }
  }
}

Depth-first Traversal 3

The type of dfs-loop reflects that it only depends on the declared ambient functions and has no other side effects: 

fun dfs-loop( vs : list〈vertex〉 ) : 〈mark,marked,children〉 list〈rose〉

In contrast, Lewis et al. (2000) bind functions by value and thus leak the side-effects of the particular implementation that uses mutable state into the dfs-loop function. The loop needs to be written in a monadic style and has the type: 

dfsLoop :: (?children :: Graph → [Vertex],
            ?marked :: Vertex → ST s Bool,
            ?mark :: Vertex → ST s ()) ⇒ [Vertex] → ST s [Rose]

where the ST effect of the operations leaks into the definition of dfsLoop.

Ambient Control

Ambient control functions are a further extension to ambient functions that return to lexical scope of their definition instead – similar to how exceptions “return” to their innermost try block. For example, let's extend our pretty printing example to stop once a certain amount of output has been produced: 

ambient control stop() : ()

fun pretty-stop(d) {
  with control stop() { "" }
  with emit-collect
  pretty-thin(d)
}

Exceptions

Ambient control also subsumes exception handling, where we can define an ambient control function throw. For example, here is a function that transforms an exception throwing action to a maybe result: 

ambient control throw(msg : string) : ()

fun to-maybe( action : () → 〈throw〉 a ) : maybe〈a〉 {
  with control throw(msg) { Nothing }
  Just(action())
}

Resuming Control

ambient control emit( s : string ): ()

fun emit-collect(action) {
  var out := ""
  with control emit(s) { 
    out := out + s + "\n"
    if (out.length ≥ 100) then () else resume(())
  } in action()
  out
}

Semantics of Ambient Control

\[\begin{mdmathpre}%mdk \gray{\mathkw{with}~\mathkw{control}~\mathid{p}(\mathid{x})~\mathid{r}~=~\mathid{e}~\mathkw{in}~\mathsf{\mathsf{E}}}[\mathid{p}(\mathid{v})]~~\\ \mdmathindent{3}{\longrightarrow}~~(\lambda \mathid{x}.~\lambda \mathid{r}.~\mathid{e})(\mathid{v})(\lambda \mathid{y}.~\gray{\mathkw{with}~\mathkw{control}~\mathid{p}(\mathid{x})~\mathid{r}~=~\mathid{e}~\mathkw{in}~\mathsf{\mathsf{E}}}[\mathid{y}])~\quad\textrm{if}~\mathid{p}\notin \mathkw{bp}(\mathsf{\mathsf{E}}) \end{mdmathpre}%mdk \]

Resuming multiple times

As another example, we can use the resumption to implement backtracking by calling it multiple times: 

ambient control choice() : bool

fun amb( action : () → 〈choice|e〉 string ) : e list〈string〉 {
  with control choice() { resume(True) + resume(False) }
  [action()]
}

Pretty Backtracking

Now, we can use choice in the pretty printing library to produce all possible layouts. For example, if 

fun f() : list〈string〉 {
  with amb
  with emit-collect
  emit("hi")
  if (choice()) then emit("world") else emit("universe")
}

then f() returns: 

["hi\nworld\n","hi\nuniverse\n"]

Local State as Ambient Control

First we α-rename such that local variables are uniquely named. Every binding of a local variable s of some type τ is then translated to a function application of a locals function: 

var s : τ := init  ~>  locals(init,fun(){ ... })
...

and occurrences of s are translated to either gets or sets: 

ambient val gets : τ
ambient control sets(x : τ) : ()
  
s := expr  ~>  sets(expr)
s          ~>  gets

This is similar to the translation by Kammar and Pretnar (2017) from mutable dynamic binding to effect handlers.

Local State as Ambient Control 2

ambient val gets : τ
ambient control sets(x : τ) : ()
  
fun locals(init,action) {
  with val gets = init
  with control sets(x) { mask〈gets〉{
                            with val gets = x
                            resume(())
                          }
                        }
  action()
}

This encoding is the same as described by Biernacki, Piróg, Polesiuk, and Sieczkowski (2017).

Safety

fun escape() {   
  var s := 0
  (fun() { s := s + 1; s }) }

Transforms to: 

fun escape() {   
  locals(0,fun(){
    (fun() { sets(gets() + 1; gets() })
  }) }

it becomes clear that the type of the result function becomes
() → 〈gets,sets〉 int, i.e. it is impossible to use this function as it depends on two (unique and hidden) ambients that cannot be bound by the user.

Defaults

It is safe to assign default implementations to ambient values and functions (but not control!) 

  ambient fun utc() : leapseconds = { [(2017,1,1), ..., (1972,1,1)] }

If main still has unresolved ambients, it binds them implicitly using the default definitions. Due to the unspecified order, the definitions must be total and not control functions.

Formalization

  • The formalization of ambient values coincides exactly with the calculus of dynamic binding $\mathpre{\lambda_\mathid{db}}$, by Moreau (1998) and Kiselyov, Shan, and Sabry (2006).
  • We show how adding row types ensures a term is never $\mathpre{\mathid{bp}}$-stuck.
  • We extend the calculus for ambient functions and control
  • We show a translation into algebraic effect handlers and show it preserves semantics.

Grouping

ambient state〈s〉 {
  fun get() : s
  fun set(x:s) : ()
}

fun state(init : s, action : () → 〈state〈s〉|e〉 a) : e a {
  var s := init
  with { 
    fun get()  { s } 
    fun set(x) { s := x }
  }
  action()
}

Ambient Instances

ambient heap { }

val heap = with〈heap〉{ }

ambient instance ref〈a〉 in heap {
  fun get() : a              // (ref〈a〉) → 〈heap,exn〉 a
  fun set( value : a ) : ()
}

fun new-ref(init : a, action : (ref〈a〉 → e b)) : e b {
  var s := init
  with r = instance {
    fun get()   { s }
    fun set(x)  { s := x }
  }
  action(r)
}

Using References

fun main() {
  with heap
  with r1 = new-ref(40)
  with r2 = new-ref("hi")
  println( r1.get() + r2.get().count)
}

syntax note: 

with x = f(x1,...,xn)    ~>  f(x1,...,xn,fun(x){ 〈body〉 })
〈body〉

But This Goes Wrong..

fun escape() {
  with x = new-ref(42)
  x
}

fun main() {
  with heap
  val y = escape()
  println( y.get() )
}

The y.get() raises an exception as it is outside the scope of the new-ref.

Real References

ambient heap {
  control new-ref(init:a) : ref〈a〉
}

val heap = with control new-ref(init){ withref(init,resume) }  // Yeah!

fun withref(init,action) {
  var s := init
  with r = instance {
    fun get()   { s }
    fun set(x)  { s := x }
  }
  action(r)
}

Real References 2

fun escape() {
  val x = new-ref(42)
  x
}

fun main() {
  with heap
  val y = escape()
  println( y.get() )
}

Questions

Syntax of $\mathpre{\lambda_{\mathid{amb}}}$

Expressions $\mathpre{\mathid{e}}$ $\mathpre{::=}$ $\mathpre{\mathid{v}}$
$\mathpre{\mid}$ $\mathpre{\mathid{e}(\mathid{e})}$
$\mathpre{\mid}$ $\mathpre{\mathkw{with}~\mathid{b}~\mathkw{in}~\mathid{e}~}$
$\mathpre{\mid}$ $\mathpre{\mathid{p}}$
 
Values $\mathpre{\mathid{v}}$ $\mathpre{::=}$ $\mathpre{\mathid{x}}$
$\mathpre{\mid}$ $\mathpre{\lambda \mathid{x}.~\mathid{e}}$
 
Dynamic Binding $\mathpre{\mathid{b}}$ ::= $\mathpre{\mathkw{val}~\mathid{p}~=~\mathid{v}}$
$\mathpre{\mathkw{fun}~\mathid{p}(\mathid{x})~=~\mathid{e}}$
$\mathpre{\mathkw{control}~\mathid{p}(\mathid{x})~\mathid{r}~=~\mathid{e}}$
 
Evaluation Context $\mathpre{\mathsf{\mathsf{E}}}$ ::= $\mathpre{\square{}~\mid \mathsf{\mathsf{E}}(\mathid{e})~\mid \mathid{v}(\mathsf{\mathsf{E}})~\mid \mathkw{with}~\mathid{b}~\mathkw{in}~\mathsf{\mathsf{E}}}$

Bound Parameters

\[\begin{mdmathpre}%mdk \mathkw{bp}(\square)~~&=~\emptyset\\ \mathkw{bp}(\mathsf{\mathsf{E}}(\mathid{e}))~~&=~\mathkw{bp}(\mathsf{\mathsf{E}})~\\ \mathkw{bp}(\mathid{v}(\mathsf{\mathsf{E}}))~~~~~&=~\mathkw{bp}(\mathsf{\mathsf{E}})\\ \mathkw{bp}(\mathkw{with}~\mathid{b}~=~\mathid{v}~\mathkw{in}~\mathsf{\mathsf{E}})~&=~\mathkw{bp}(\mathid{b})\cup \mathkw{bp}(\mathsf{\mathsf{E}})\\ \\ \mathkw{bp}(\mathkw{val}~\mathid{p}~=~\mathid{v})~&=~\{\mathid{p}\}\\ \mathkw{bp}(\mathkw{fun}~\mathid{p}(\mathid{x})~=~\mathid{e})~&=~\{\mathid{p}\}\\ \mathkw{bp}(\mathkw{control}~\mathid{p}(\mathid{x})~\mathid{r}~=~\mathid{e})~&=~\{\mathid{p}\} \end{mdmathpre}%mdk \]

Operational Semantics

$\mathpre{(\beta)}$ $\mathpre{(\lambda \mathid{x}.~\mathid{e})(\mathid{v})}$ $\mathpre{{\longrightarrow}}$ $\mathpre{\mathid{e}[\mathid{x}~{:=}~\mathid{v}]~}$
$\mathpre{(\mathid{dret})}$ $\mathpre{\mathkw{with}~\mathid{b}~\mathkw{in}~\mathid{v}}$ $\mathpre{{\longrightarrow}}$ $\mathpre{\mathid{v}}$
$\mathpre{(\mathid{dval})}$ $\mathpre{\gray{\mathkw{with}~\mathkw{val}~\mathid{p}~=~\mathid{v}~\mathkw{in}~\mathsf{\mathsf{E}}}[\mathid{p}]}$ $\mathpre{{\longrightarrow}}$ $\mathpre{\gray{\mathkw{with}~\mathkw{val}~\mathid{p}~=~\mathid{v}~\mathkw{in}~\mathsf{\mathsf{E}}}[\mathid{v}]}$   if $\mathpre{\mathid{p}~\notin \mathkw{bp}(\mathsf{\mathsf{E}})}$
\[\begin{mdmathpre}%mdk \infer{\mathid{e}~{\longrightarrow}~\mathid{e}'}{\mathsf{\mathsf{E}}[\mathid{e}]~{\longmapsto}~\mathsf{\mathsf{E}}[\mathid{e}']}{\textsc{eval}} \end{mdmathpre}%mdk \]

Operational Semantics Extended

$\mathpre{(\mathid{dfun})}$ $\mathpre{\gray{\mathkw{with}~\mathkw{fun}~\mathid{p}(\mathid{x})~=~\mathid{e}~\mathkw{in}~\mathsf{\mathsf{E}}}[\mathid{p}(\mathid{v})]}$
$\mathpre{{\longrightarrow}}$ $\mathpre{(\lambda \mathid{y}.~\gray{\mathkw{with}~\mathkw{fun}~\mathid{p}(\mathid{x})~=~\mathid{e}~\mathkw{in}~\mathsf{\mathsf{E}}}[\mathid{y}])(\mathid{e}[\mathid{x}{:=}\mathid{v}])}$   if $\mathpre{\mathid{p}\notin \mathkw{bp}(\mathsf{\mathsf{E}})}$
 
$\mathpre{(\mathid{dctl})}$ $\mathpre{\gray{\mathkw{with}~\mathkw{control}~\mathid{p}(\mathid{x})~\mathid{r}~~=~\mathid{e}~\mathkw{in}~\mathsf{\mathsf{E}}}[\mathid{p}(\mathid{v})]}$
$\mathpre{{\longrightarrow}~}$ $\mathpre{\mathid{e}[\mathid{x}{:=}\mathid{v},\mathid{r}{:=}\lambda \mathid{y}.~\gray{\mathkw{with}~\mathkw{control}~\mathid{p}(\mathid{x})~\mathid{r}~=~\mathid{e}~\mathkw{in}~\mathsf{\mathsf{E}}}[\mathid{y}]{}]}$   if $\mathpre{\mathid{p}\notin \mathkw{bp}(\mathsf{\mathsf{E}})}$

with fresh $\mathpre{\mathkw{y}}$

Type Syntax

Types $\mathpre{{\tau}}$ $\mathpre{::=}$ $\mathpre{\mathid{c}}$
$\mathpre{\mid}$ $\mathpre{{\tau}~{\rightarrow}~{\pi}~{\tau}}$
 
Ambient Row $\mathpre{{\pi}}$ $\mathpre{::=}$ $\mathpre{\total{}}$
$\mathpre{\mid}$ $\mathpre{\langle{}\mathid{p}\mid {\pi}\rangle{}}$
 
Constants $\mathpre{\mathid{c}}$ ::= $\mathpre{\mathid{p}~}$ …
 
Type Environment $\mathpre{\Gamma{}}$ $\mathpre{::=}$ $\mathpre{\emptyset \mid \Gamma{},\mathid{x}:{\tau}}$
Ambient Signature $\mathpre{\Sigma{}}$ $\mathpre{::=}$ $\mathpre{\emptyset \mid \Sigma{},\mathid{p}:\mathkw{val}~{\tau}~\mid \Sigma{},\mathid{p}:\mathkw{fun}~\tau_{1}~{\rightarrow}~\tau_{2}}$

Type Rules 1

\[\begin{mdmathpre}%mdk \infer{\Gamma{}(\mathid{x})~=~{\tau}}{\Gamma{}~\!\vdash_{\!\mathid{val}}~\mathid{x}~:~{\tau}~}{\textsc{var}} \end{mdmathpre}%mdk \]

\[\begin{mdmathpre}%mdk \infer{\Gamma{}~\!\vdash_{\!\mathid{val}}~\mathid{v}~:~{\tau}~}{\Gamma{}~\!\vdash_{\!\mathid{amb}}~\mathid{v}~:~{\tau}~|~{\pi}~}{\textsc{val}} \end{mdmathpre}%mdk \]

\[\begin{mdmathpre}%mdk \infer{\Sigma{}(\mathid{p})~=~\mathkw{val}~{\tau}}{\Gamma{}~\!\vdash_{\!\mathid{amb}}~\mathid{p}~:~{\tau}~|~\langle{}\mathid{p}|{\pi}\rangle{}}{\textsc{dval}} \end{mdmathpre}%mdk \]

Type Rules 2

\[\begin{mdmathpre}%mdk \infer{\Gamma{},\mathid{x}:\tau_{1}~\!\vdash_{\!\mathid{amb}}~\mathid{e}~:~\tau_{2}~|~{\pi}}{\Gamma{}~\!\vdash_{\!\mathid{val}}~\lambda \mathid{x}.\mathid{e}~:~\tau_{1}~{\rightarrow}~{\pi}~\tau_{2}~}{\textsc{lam}} \end{mdmathpre}%mdk \]

\[\begin{mdmathpre}%mdk \infer{\Gamma{}~\!\vdash_{\!\mathid{amb}}~\mathid{e}_{1}~:~\tau_{1}~{\rightarrow}~{\pi}~\tau_{2}~|~{\pi}~\quad \Gamma{}~\!\vdash_{\!\mathid{amb}}~\mathid{e}_{2}~:~\tau_{2}~|~{\pi}}{\Gamma{}~\!\vdash_{\!\mathid{amb}}~\mathid{e}_{1}(\mathid{e}_{2})~:~\tau_{2}~|~{\pi}~}{\textsc{app}} \end{mdmathpre}%mdk \]

\[\begin{mdmathpre}%mdk \infer{\Sigma{}(\mathid{p})~=~\mathkw{val}~\tau_{1}~\quad \Gamma{}~\!\vdash_{\!\mathid{val}}~\mathid{v}~:~\tau_{1}~\quad \Gamma{}~\!\vdash_{\!\mathid{amb}}~\mathid{e}~:~\tau_{2}~|~\langle{}\mathid{p}|{\pi}\rangle{}~}{\Gamma{}~\!\vdash_{\!\mathid{amb}}~\mathkw{with}~\mathkw{val}~\mathid{p}~=~\mathid{v}~\mathkw{in}~\mathid{e}~:~\tau_{2}~|~{\pi}}{\textsc{wval}} \end{mdmathpre}%mdk \]

Type Rules 3

\[\begin{mdmathpre}%mdk \infer{\Sigma{}(\mathid{p})~=~\mathkw{fun}~\tau_{1}~{\rightarrow}~\tau_{2}~\quad \Gamma{}~\!\vdash_{\!\mathid{val}}~\mathid{v}~:~\tau_{1}}{\Gamma{}~\!\vdash_{\!\mathid{amb}}~\mathid{p}(\mathid{v})~:~\tau_{2}~|~\langle{}\mathid{p}|{\pi}\rangle{}}{\textsc{dfun}} \end{mdmathpre}%mdk \]

\[\begin{mdmathpre}%mdk \infer{\Sigma{}(\mathid{p})~=~\mathkw{fun}~\tau_{1}~{\rightarrow}~\tau_{2}~\quad \Gamma{},\mathid{x}:\tau_{1}~\!\vdash_{\!\mathid{amb}}~\mathid{e}_{1}~:~\tau_{2}~|~{\pi}~~\quad \Gamma{}~\!\vdash_{\!\mathid{amb}}~\mathid{e}_{2}~:~{\tau}~|~\langle{}\mathid{p}|{\pi}\rangle{}~}{\Gamma{}~\!\vdash_{\!\mathid{amb}}~\mathkw{with}~\mathkw{fun}~\mathid{p}(\mathid{x})~=~\mathid{e}_{1}~\mathkw{in}~\mathid{e}_{2}~:~{\tau}~|~{\pi}}{\textsc{wfun}} \end{mdmathpre}%mdk \]

\[\begin{mdmathpre}%mdk \infer{\Sigma{}(\mathid{p})~=~\mathkw{fun}~\tau_{1}~{\rightarrow}~\tau_{2}~\quad \Gamma{},\mathid{x}:\tau_{1},\mathid{r}:\tau_{2}~{\rightarrow}~{\pi}~{\tau}~\!\vdash_{\!\mathid{amb}}~\mathid{e}_{1}~:~{\tau}~|~{\pi}~\quad \Gamma{}~\!\vdash_{\!\mathid{amb}}~\mathid{e}_{2}~:~{\tau}~|~\langle{}\mathid{p}|{\pi}\rangle{}~}{\Gamma{}~\!\vdash_{\!\mathid{amb}}~\mathkw{with}~\mathkw{control}~\mathid{p}(\mathid{x})~\mathid{r}~=~\mathid{e}_{1}~\mathkw{in}~\mathid{e}_{2}~:~{\tau}~|~{\pi}}{\textsc{wctl}} \end{mdmathpre}%mdk \]

Progress if not stuck

Definition 1. ($\mathpre{\mathid{bp}}$-stuck)
A term is $\mathpre{\mathid{bp}}$-stuck if it has the form $\mathpre{\mathsf{\mathsf{E}}[\mathid{p}]}$ where $\mathpre{\mathid{p}\notin \mathkw{bp}(\mathsf{\mathsf{E}})}$.

Theorem 1. (Progress)
If $\mathpre{\emptyset\!\vdash_{\!\mathid{db}}~\mathid{e}~:~{\tau}}$ and $\mathpre{\mathid{e}}$ is not a value and not $\mathpre{\mathid{bp}}$-stuck, then $\mathpre{\mathid{e}~{\longmapsto}~\mathid{e}'}$ for some term $\mathpre{\mathid{e}'}$.

Extended typing guarantees not stuck

Theorem 2.
If $\mathpre{\Gamma{}~\!\vdash_{\!\mathid{amb}}~\mathid{e}~:~{\tau}~|~\total{}}$ then $\mathpre{\mathid{e}}$ is not $\mathpre{\mathid{bp}}$-stuck.

Theorem 3. (Progress)
If $\mathpre{\emptyset \!\vdash_{\!\mathid{amb}}~\mathid{e}~:~{\tau}~|~\total{}}$ and $\mathpre{\mathid{e}}$ is not a value, then $\mathpre{\mathid{e}~{\longmapsto}~\mathid{e}'}$ for some term $\mathpre{\mathid{e}'}$.

Soundness of Translation

Theorem 4. (Type Preservation)
If $\mathpre{\Gamma{}\!\vdash_{\!\mathid{amb}}~\mathid{e}~:~{\tau}~|~{\epsilon}}$, then $\mathpre{\Gamma{}\!\vdash_{\!\mathid{aeh}}~\tr{\mathid{e}}~:~{\tau}~|~{\epsilon}}$.

Theorem 5. (Semantic Soundness)
If $\mathpre{\mathid{e}~{\longmapsto}~\mathid{e}'}$ then $\mathpre{\tr{\mathid{e}}~{\longmapsto}^*~\tr{\mathid{e}'}}$

References

Dariusz Biernacki, Maciej Piróg, Piotr Polesiuk, and Filip Sieczkowski. “Handle with Care: Relational Interpretation of Algebraic Effects and Handlers.” Proc. ACM Program. Lang. 2 (POPL’17 issue): 8:1–8:30. Dec. 2017. doi:10.1145/3158096. 🔎
Ohad Kammar, and Matija Pretnar. “No Value Restriction Is Needed for Algebraic Effects and Handlers.” Journal of Functional Programming 27 (1). Cambridge University Press. Jan. 2017. 🔎
Oleg Kiselyov, Chung-chieh Shan, and Amr Sabry. “Delimited Dynamic Binding.” In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming, 26–37. ICFP ’06. ACM, New York, NY, USA. 2006. 🔎
Jeffrey R. Lewis, John Launchbury, Erik Meijer, and Mark B. Shields. “Implicit Parameters: Dynamic Scoping with Static Types.” In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 108–118. POPL’00. ACM, Boston, MA, USA. 2000. 🔎
Luc Moreau. “A Syntactic Theory of Dynamic Binding.” Higher-Order and Symbolic Computation 11 (3): 233–279. Sep. 1998. doi:10.1023/A:1010087314987. 🔎

end