From Monads to Effects and Back
Madoko sample – do not distribute
Niki Vazou
UC San Diego
Daan Leijen
Microsoft Research

Abstract. The combination of monads and effects leads to a clean and easy to reason programming paradigm. Monadic programming is easy to reason, but can be cumbersome, as it requires explicit lifting and binding. In this paper, we combine monads and effects within a single programming paradigm: we use monads to define the semantics of effect types, and then, use the effects to program with those monads. In particular, we implemented an extension to the effect type system of Koka [20] with user defined effects. We use a type-directed translation to automatically lift such effectful programs into monadic programs, by inserting bind- and unit operations. As such, these user-defined effects are not just introducing a new effect type, but also enable full monadic abstraction and let us “take control of the semi-colon” in a typed and structured manner. We give examples of various abstractions like ambiguous computations and parsers. All examples have been implemented in the Koka language and we describe various implementation issues and optimization mechanisms.

1. Introduction

Μonads (proposed by Moggi and others [24, 35]) are used in programming languages to wrap effectful computations, but they can be cumbersome to program with as they require explicit lifting and binding. In this paper, we combine monads and effect typing (proposed by Gifford and others [11, 32]) within a single programming paradigm: we use monads to define the semantics of effect types, and then, use the effect types to program with those monads.

We implemented these ideas as an extension of the effect type system of Koka [20] – a strict, JavaScript-like, strongly typed programming language that automatically infers the type and effect of functions. Koka has a type inference system for a set of standard effects like divergence, exceptions, heap operations, input/output, etc. Here we extend the effect system with monadic user defined effects, where we can define our own effect in terms of any monad. As an example, we define an amb effect for ambiguous computations [17]. In particular we would like to have ambiguous operations that return one of many potential values, but in the end get a list of all possible outcomes of the ambiguous computation. Using our new effect declaration we can define the semantics of the amb effect in terms of a concrete list monad:

effect amba = lista {
 function unit( x ) { [x] }
 function bind( xs, f ) { xs.concatMap(f) }
}

where the unit and bind are the usual list-monad definitions.

Using the above effect definition we can write functions that have the ambiguous effect. For example we can write a flip primitive that returns either true or false and use it to compute the truth table of xor:

function flip : () amb bool
function xor() : amb bool {
 val p = flip()
 val q = flip()
 (p||q) && not(p&&q) // p,q : bool
}

Note how the result of flip is just typed as bool (even though amb computations internally use a list monad of all possible results). Furthermore, unlike languages like Haskell, we do not need to explicitly lift expressions into a monad, or explicitly bind computations using do notation.

Translation. Koka uses an automatic type directed translation that translates a program with user-defined effect types into a corresponding monadic program. Internally, the previous example gets translated into:

function xor() : listbool {
 bind( flip(), fun(p) {
  bind( flip(), fun(q) {
   unit( (p||q) && not(p&&q) )
})})}

Here we see how the unit and bind of the effect declaration are used: bind is inserted whenever a monadic value is returned and passed the current continuation at that point.

The capture of the continuation at every bind makes monadic effects very expressive. For example, the amb effect can cause subsequent statements to be executed multiple times, i.e. once for every possible result. This is somewhat dual to the built-in exception effect which can cause subsequent statements to not be executed at all, i.e. when an exception is thrown. As such, this kind of expressiveness effectively let us take “control of the semi-colon”.

The marriage of effects and monads. Translating effectful- to monadic code is not new. Wadler and Thiemann [36] show that any effectful computation can be transposed to a corresponding monad. If $\mathpre{\mathid{x}\llbracket\tau\rrbracket}$ is the call-by-value type translation of $\mathpre{\tau}$ and $\mathpre{\mathid{M}_\mathid{u}}$ is the corresponding monad of an effect $\mathpre{\mathid{u}}$, they show how an effectful function of type $\mathpre{\llbracket\tau_1~{\rightarrow}~\mathid{u}~\tau_2\rrbracket}$ corresponds to a pure function with a monadic type $\mathpre{\llbracket\tau_1\rrbracket {\rightarrow}~\mathid{M}_\mathid{u}{\langle}\llbracket\tau_2\rrbracket{\rangle}}$. In this article, we translate any effectful function of type $\mathpre{\llbracket\tau_1~{\rightarrow}~{\langle}\mathid{u}|\e{\rangle}~\tau_2\rrbracket}$, to the function $\mathpre{\llbracket\tau_1\rrbracket {\rightarrow}~\e\ \mathid{M}_\mathid{u}{\langle}\e,\llbracket\tau_2\rrbracket{\rangle}}$. This is almost equivalent, except for the $\mathpre{\e}$ parameter which represents arbitrary built-in effects like divergence or heap operations. If we assume $\mathpre{\e}$ to be empty, i.e. a pure function like in Wadler and Thiemann's work, then we have an exact match! As we shall see, due to the non-monadic effects as an extra parameter, our monads are effectively indexed- or poly-monads [14] instead of regular monads.

Our contributions are summarized as follows:

2. Overview

Types tell us about the behavior of functions. For example, the ML type $\mathpre{\mathid{int}~{\rightarrow}~\mathid{int}}$ of a function tells us that the function is well defined on inputs of type $\mathpre{\mathid{int}}$ and returns values of type $\mathpre{\mathid{int}}$. But that is only one part of the story, the ML type tells us nothing about all other behaviors: i.e. if it accesses the file system perhaps, or throws exceptions, or never returns a result at all.

Koka is a strict programming language with a type system that tracks effect. The type of a function in Koka is of the form $\mathpre{\tau {\rightarrow}~\e\ \tau'}$ signifying a function that takes an argument of type $\mathpre{\tau}$, returns a result of type $\mathpre{\tau'}$ and may have a side effect $\mathpre{\e}$. We can leave out the effect and write $\mathpre{\tau {\rightarrow}~\tau'}$ as a shorthand for the total function without any side effect: $\mathpre{\tau {\rightarrow}~\empeffect\ \tau'}$. A key observation on Moggi's early work on monads [24] was that values and computations should be assigned a different type. Koka applies that principle where effect types only occur on function types; and any other type, like $\mathpre{\mathid{int}}$, truly designates an evaluated value that cannot have any effect1.

In contrast to many other effect systems, the effect types are not just labels that are propagated but they truly describe the semantics of each function. As such, it is essential that the basic effects include exceptions ($\mathpre{\mathid{exn}}$) and divergence ($\mathpre{\mathid{div}}$). The deep connection between the effect types and the semantics leads to strong reasoning principles. For example, Koka's soundness theorem [20] implies that if the final program does not have an $\mathpre{\mathid{exn}}$ effect, then its execution never results in an exception (and similarly for divergence and state).

Example: Exceptions.

Exceptions in Koka can be raised using the primitive error function:

error : string exn a

The type shows that error takes a string as an argument and may raise an exception. It returns a value of any type! This is clearly not possible in a strongly typed parametric language like Koka, so we can infer from this type signature that error always raises an exception. Of course, effects are properly propagated so the function wrong will be inferred to have the exn type too:

function wrong() : exn int { error("wrong"); 42 }

Exceptions can be detected at run-time (unlike divergence) so we can discharge exceptions using the catch function:

function catch( action : () exn a,
 handler : exception a) : a

To catch exceptions we provide two arguments: an action that may throw an exception and an exception handler. If action() throws an exception the handler is invoked, otherwise the result of the action() is returned. In both cases catch has a total effect: it always returns a value of type a. For example, function pure always returns an int:

function pure() : int { catch( wrong, fun(err){ 0 } ) }
Effect polymorphism.

In reality, the type of catch is more polymorphic: instead of just handling actions that can at most raise an exception, it accepts actions with any effect that includes exn:

function catch( action : () exn|e a,
 handler : exception e a ) : e a

The type variable e applies to any effect. The type expression exn|e stands for the effect row that extends the effect e with the effect constant exn. Effectively, this type captures that given an action that can potentially raise an exception, and perhaps has other effects e, catch will handle that exception but not influence any of the other effects. In particular, the handler has at most effect e. For example, the result effect of:

catch( wrong, fun(err) { print(err); 0 } )

is console since the handler uses print. Similarly, if the handler itself raises an exception, the result of catch will include the exn effect:

catch( wrong, fun(err) { error("oops") } )

Apart from exceptions Koka supplies more built-in effects: we already mentioned div that models divergence; there is also io to model interaction with input-output, ndet to model non-determinism, heap operations through alloc, read, and write, and the list goes on. For all built-in effects, Koka supplies primitive operators that create (e.g. error, random, print, etc) and sometimes discharge (e.g. catch, timeout, or runST) the effect.

The main contribution of this paper is how we extend Koka so that the user can define her own effects, by specifying the type and meaning of new effects and defining primitive operations on them.

2.1. The ambiguous effect

In the introduction we saw how one can define and use the ambiguous amb effect with flip and xor operations. We now discuss the definition and translation in more detail. The amb effect is defined using an effect declaration:

effect amba = lista {
 function unit( x : a ) : lista { [x] }
 function bind( xs : lista, f : a e listb ) : e listb {
  xs.concatMap(f)
 }
}

Defining the amb effect amounts to defining the standard list monad, which can be further simplified by removing the optional type annotations. Given the above definition, a new effect type amb is introduced, and we know:

  1. how to represent (internally) ambiguous computations of a values: as a lista
  2. how to lift plain values into ambiguous ones: using unit, and
  3. how to combine ambiguous computations: using bind.

Moreover, with the above definition Koka automatically generates the to_amb and from_amb primitives, and a monadic type alias:

function to_amb ( xs : lista ) : amb a
function from_amb ( action: () amb a ) : lista
alias M_amba = lista

that allow us to go from monadic values to effect types and vice versa. These are basically typed versions of the reify and reflect methods of Filinski's monadic embedding [8].

We use the above primitives to define the flip function that creates the ambiguous effect and the function main that evaluates the effectful computation:

function flip() : amb bool { to_amb( [False,True] ) }
function main() : console () { print( from_amb(xor) ) }

When we evaluate main we get a list of all possible output values: [False,True,True,False]. One can extend such mechanism to, for example, return a histogram of the results, or to general probabilistic results [17, 31].

Later we discuss the more interesting effect of parsers (§ 2.3), but before that, let's discuss in more detail how we do a monadic translation of effects.

2.2. Translating effects

Koka uses a type directed translation to internally translate effectful to monadic code. As shown in the introduction, the xor function is translated as:

function xor() : amb bool
{
 val p = flip()
 val q = flip()
  
 (p||q) && not(p&&q)
}

$\mathpre{\mathop{\leadsto}}$

function xor() : listbool
{
 bind( flip(), fun(p) {
  bind( flip(), fun(q) {
   unit(
    (p||q) && not(p&&q) )
})})}

In particular, bind is inserted at every point where a monadic value is returned, and passed the current continuation at that point. Since flip has an ambiguous result, our type-directed translation binds its result to a function that takes p as an argument and similarly for q. Finally, the last line returns a pure boolean value, but xor's result type is ambiguous. We use unit to lift the pure value to the ambiguous monad. We note that in Koka's actual translation, xor is translated more efficiently using a single map instead of a unit and bind.

The translation to monadic code is quite subtle and relies crucially on type information provided by type inference. In particular, the intermediate core language is explicitly typed à la System F (§ 3.1). This way, we compute effects precisely and determine where bind and unit get inserted (§ 3.3). Moreover, we rely on the user to ensure that the unit and bind operations satisfy the monad laws [35], i.e. that unit is a left- and right identity for bind, and that bind is associative. This is usually the case though; in particular because the effect typing discipline ensures that both unit and bind are total and cannot have any side-effect (which makes the translation semantically robust against rewrites).

2.2.1. Translating polymorphic effects

One of the crucial features of Koka is effect polymorphism. Consider the function map

function map(xs : lista, f : (a) e b) : e listb {
 match(xs) {
  Nil Nil
  Cons(y, ys) Cons( f(y), map(ys,f) )
 }
}

The function map takes as input a function f with some effect e. Since it calls f, map can itself produce the effect e, for any effect e. This means that we can use such existing abstractions on user defined effects too:

function xor() {
 val [p,q] = map( [1,2], fun(_) { flip() } )
 (p||q) && not(p&&q)
}
// source effectful code
function map(xs, f) {
 match(xs) {
  Nil Nil
  Cons(y, ys)
   val z = f(y)
   val zs = map(ys, f)
   Cons(z, zs)
     
 }
}
     
function xor() {
 val [p,q] =
  map( [1,2],
   fun(_) { flip() })
     
     
 (p||q) && not(p&&q)
     
}
// translated monadic code
function map(d:dicte, xs, f) {
 match(xs) {
  Nil d.unit(Nil)
  Cons(y, ys)
    d.bind( f(y), fun(z) {
     d.bind( map(ys, f),
      fun(zs) {
       d.unit(Cons(z, zs)
 })})}
}
        
function xor() {
 dict_amb.bind(
  map( dict_amb, [1,2],
    fun(_) { flip() }),
 fun([p,q]) {
  dict_amb.unit(
   (p||q) && not(p&&q))
 })
}

Figure 1. Dictionary translation of map and xor

Unfortunately, this leads to trouble when doing a type directed translation: since the function passed to map has a monadic effect, we need to bind the call f(y) inside the map function! Moreover, since we can apply map to any monadic effect, we need to dynamically call the right bind function.

The remedy is to pass Haskell-like dictionaries or monad interfaces to effect polymorphic functions. In our case, a dictionary is a structure that wraps the monadic operators bind and unit. The dictionaries are transparent to the user and are automatically generated and inserted. During the translation, every effect polymorphic function takes a dictionary as an additional first argument. Figure 1 shows how the map function gets translated.

Now that internally every effect polymorphic function gets an extra dictionary argument, we need to ensure the corresponding dictionary is supplied at every call-site. Once again, dictionary instantiation is type-directed and builds upon Koka's explicitly typed intermediate core language. Whenever a polymorphic effect function is instantiated with a specific effect, the type directed translation automatically inserts the corresponding dictionary argument. Figure 1 shows this in action when we call map inside the xor function. We can still use map with code that has a non-monadic effect and in that case the translation will use the dictionary of the primitive identity monad, e.g. map( dict_id, [1,2], sqr ).

A naïve translation is not very efficient though: always using the monadic version of map introduces a performance penalty to all code, even code that doesn't use any monadic effect. As shown in § 4.1, we avoid this by careful translation. For every effect polymorphic function, we generate two versions: one that takes a monad dictionary, and another that has no monadic translation at all. When instantiating map we use the efficient non-monadic version unless there is monadic effect. This way the performance of code with non-monadic effects is unchanged.

Being able to reuse any previous abstractions when using monadic effects is very powerful. If we insert user-defined effects to a function, only the type of the function changes. Contrast this to Haskell: when inserting a monad, we need to do a non-trivial conversion of the syntax to do notation, but also we need to define and use monadic counterparts of standard functions, like mapM for map.

2.2.2. Interaction between user defined effects

Koka allows combination of user defined effects. Consider a behavior user defined effect, which represents computations whose value varies with time, as in functional reactive programs [7]. We encode the beh effect as a function from time to a. Since a behaviour is a function, it may have effects itself: it can diverge or throw exceptions for example. This means that we need to parameterize the beh effect with two type parameters one for the value a and one for the effect e:

effect behe, a = time e a { ... }

With the above definition, Koka automatically creates a type alias for the behavioral monad and the respective unit and bind operators:

alias M_behe, a = time e a;
ub : a e M_behe, a;
bb : (M_behe, a, a e M_behe, b) e M_behe, b
 

As with the amb effect, the user can define primitives that, for example, return the temperature and humidity over time:

temp : () beh int;
hum : () beh int;

We use these primitives to define a function that states that one goes out when temperature is more than 70°F and humidity less than 80%. Koka automatically translates the effectful function to its monadic version:

function go_out() : beh bool
{
 val t = temp()
 val h = hum()
  
 (t 70 && h 80)
}

$\mathpre{\mathop{\leadsto}}$

function go_out() : time bool
{
 bb( temp(), fun(t) {
  bb( hum(), fun(h) {
   ub(
    (t70 && h80)
})})}

Next, we want to insert ambiguity into the above function. Following Swamy et al. [31] we combine the ambiguous and behavioral effects by tupling them

effect amb, behe, a = time e lista { ... }

and Koka creates the appropriate monadic operators

alias M_abe, a = time e lista;
uab : a e M_abe, a;
bab : (M_abe, a, a e M_abe, b) e M_abe, b;

Then, we define morphisms to lift from a single to the joined effect

morphism amb amb, beh{ fun(xs){ fun(t){ xs }} }
morphism beh amb, beh{ fun(b){ fun(t){ [b(t)] }} }

With the above morphism definitions, Koka automatically derives internal morphism functions

a2ab :: M_amb e, a e M_amb, behe, a;
b2ab :: M_beh e, a e M_amb, behe, a;

and use them to automatically translate our modified go_out function that combines the two user defined effects:

function go_out()
{
 val t = temp()
 val h = hum()
 val u = flip()
  
 (u || (t 70 && h 80))
}

$\mathpre{\mathop{\leadsto}}$

function go_out()
{
 bab( b2ab(temp()), fun(t) {
  bab( b2ab(hum()), fun(h) {
   bab( a2ab(flip()), fun(u) {
     uab(
    (u || (t70 && h80))
})})}

This technique for combining monads by tupling is taken from [31]. But, as further discussed in § 5 our current work, though highly inspired, crucially differs from [31] in that the use of effect polymorphism (instead of effect subtyping that was previously used) makes types much simpler.

There are various language design aspects with regard to morphism declarations – due to space restrictions we highlight the most important ones and defer to [31] and [14] for a more in-depth discussion. First of all, since effect rows are equivalent up to re-ordering of labels, we can only declare one combined monad for a specific set of user-defined effects. For example, we can combine amb,beh in only one of the two possible ways (within the scope of a module). Moreover, the compiler rejects duplicate definitions. Finally, if we assume that the morphism laws hold, the compiler could derive morphisms from the existing ones, i.e. morphisms from ma to mb, and mb to mc can be combined to give rise to a morphism from ma to mc. Currently, in our system we assume that the user provides all required morphisms explicitly, but we plan to implement automatic morphism derivation.

2.2.3. Interaction with build-in Koka effects

User-defined effects, like amb, interact with built-in effects like state, divergence, and exceptions. The formal semantics of Koka [20] are unchanged in our system, and we define the semantics of the user-defined effects simply as a monadic transformation. As such, if we viewed the effects as a stack of monad transformers, the user defined effects would be last with all built-in effects transforming it, i.e. something like divstexnamba. These semantics still require careful compilation; for example, it is important when doing the internal monadic translation to properly capture local variables in the continuation functions passed to bind.

Here is an example of a more subtle interaction: if we use mutable variables in the ambiguity monad, we may observe that computations run multiple times:

function strange() : amb bool {
 var i := 0
 val p = flip()
 val q = flip()
 i := i+1
 if (i 4) then True else (p||q) && not(p&&q)
}

In this example, we define and increment the mutable variable i. The function strange itself does not have a stateful effect (sth) because the mutability is not observable from outside and can be discharged automatically through Koka's higher-ranked type system [18, 20]. However, executing run(strange) results in [False,True,True,True] where inside the body of strange we can observe that some statements are executed multiple times. This shows the importance of strong typing: in an IDE one would see that the flip() invocations have an amb effect that causes the following statements to potentially execute more than once. This is similar for exceptions, where statements following invocations of functions that may raise exceptions, may not execute at all.

Under the monadic semantics, the interaction with built-in effects is more or less what one would expect, with one exception: the exception effect does not play nice with certain user defined effects due to the (expected) lexical scoping of catch. Exceptions interact with amb as expected, but this is not the case in the context of the parser effect as we further discuss in § 2.3.1.

2.3. The parser effect

We conclude the overview with a more advanced example in the form of monadic parsers. A parser can be defined as a function that consumes the input string and returns a list of (all possible) pairs of parsed tokens and the remaining input: string list(a,string). This representation is quite standard but many other designs are possible [15, 21]. Since a parser (like the behaviour effect) is a function, it may have effects itself: parsers can diverge or throw exceptions for example. This means that we need to parameterize the parser effect with two type parameters (instead of one):

effect parsere,a = string e list(a,string) {
 function unit( x ) { return fun(s) { [(x,s)] } }
 function bind( p, f ) {
  return fun(s) {
   p(s).concatMap( fun(r) { f(r.fst)(r.snd) } )
 }}
}

Given the above definition, Koka automatically derives the conversion functions:

function to_parser( p : string e list(a,string) )
 : parser|e a
function from_parser( action : () parser|e a)
 : e (string e list(a,string))

which can be used by the parser-library developer to build primitive parsing operators as shown in Figure 2: parse that takes a parsing computation and an input string and runs the parser; succeed(x) that returns its argument x, without consuming the input; satisfy(p) that parses the string iff it satisfies p; and choice(p1, p2) that chooses between two parsers p1 or p2.

Note how the effect e in from_parser occurs both as the effect of the function, but also in the returned parser function. Essentially this is because we cannot distinguish at the type level whether an effect occurs when constructing the parser (i.e. before the first bind), or whether it occurs when running the parser.

function parse( p : () parser|e a, input : string
  ) : e list(a,string) {
 from_parser(p)(input)
}
function succeed( x : a ) : parser a {
 to_parser fun(input) { [(x,input)]
}
     
function satisfy( pred : (string) maybe(a,string) ) {
 to_parser fun(input) {
  match(pred(input)) {
   Just((x,rest)) [(x,rest)]
   Nothing []
 }}
}
function choice( p1 : () parser|e a,
    p2 : () parser|e a ) : parser|e a {
 to_parser fun(input) {
  match (parse(p1,input)) {
   Nil parse(p2,input)
   res res
 }}
}

Figure 2. Parser primitives

Having set up the parser effect and its primitives, we combine them to construct other parsers. For example, many(p) is a parser that applies p zero or more times. A digit can be parsed as a character where satisfy isDigit. Combining these two, many(digit) gives a list of parsed digits.

function main(input: string): div listint, string {
 parse(integer, input)
}
function integer() : parser,div int {
 val ds = many(digit)
 ds.foldl(0,fun(i,d) { i*10 + d })
}
function digit() : parser int { satisfy( ... ) }
function many( p : () parser,div|e a )
 : parser,div|e lista {
choice { Cons(p(),many(p)) } { succeed(Nil) }
}

Running main("12a") now results in [(12,"a")]. Note also how in the integer function we combine parser results (many(digit)) with pure library functions (foldl).

2.3.1. Interaction with exceptions

Because the parser monad is defined as a function exception handling does not work as expected. Take for example the following parser that may raise an exception:

function division() : parser,exn int {
 val i = integer(); keyword("/"); val j = integer()
 if (j==0) then error("divide by zero") else i/j
}

Suppose now that we catch errors on parsers, as in the following safe version of our parser:

function safe() : parser int { catch( division, fun(err) { 0 } ) }

If catch is implemented naïvely the behaviour of safe would not be the expected one. In particular, if catch just wraps a native try-catch block, then the exceptions raised inside division will not be caught: after the monadic translation, division would return immediately with a parser function as, only invoking the parser function would actually raise the exception (i.e. when the parser is run using parse). Effectively, the lexical scoping expectation of the catch would be broken.

Our (primitive) catch implementation takes particular care to work across monadic effects too. Since catch is polymorphic in the effect, the type directed translation will actually call the specific monadic version of catch and pass a dictionary as a first argument. The primitive monadic catch is implemented in pseudo-code as:

function catch_monadic( d : dicte, action, handler ) {
 catch( { d.bind_catch( action, handler ) }, handler)
}

Besides catching regular exceptions raised when executing action(), it uses the special bind_catch method on the dictionary that allows any user-defined effect to participate in exception handling. This is essential for most effects that are implemented as functions. For the parser, we implement it as:

effect parsere,a = string e list(a,string) {
 ...
 function bind_catch( p, handler ) {
  fun(s) { catch( { p(s) }, fun(err) { handler(err)(s) }) }
 }
}

With this implementation in place, the parser effect participates fully in exception handling and the safe parser works as expected, where any exception raised in division is handled by our handler, i.e. the expression parse(safe,"1/0") evaluates to 0.

Here is the type of bind_catch and its default implementation:

function bind_catch( action : () exn|e mexn|e,a,
 handler : exception e me,a
 ) : e me,a
{ catch(action,handler) }

In the above type we write m for the particular monadic type on which the effect is defined. A nice property of this type signature and default implementation is that Koka type inferencer requires you to define bind_catch, only when needed for your particular monad. For example, the default works as is for the amb effect since its monad disregards the e parameter, but the default is correctly rejected by the type checker for the parser since the signature of catch requires the mexn|e,a to be unified with me,a.

3. Formalism

In this section we formalize the type-directed translation using an explicitly typed effect calculus we call $\mathpre{\lambda^{\kk\mathsf{u}}}$. First, we present the syntax (§ 3.1) and typing (§ 3.2) rules for $\mathpre{\lambda^{\kk\mathsf{u}}}$. Then, we formalize our translation (§ 3.3) from effectful to monadic $\mathpre{\lambda^{\kk\mathsf{u}}}$. Finally, we prove soundness (§ 3.4) by proving type preservation of the translation.

3.1. Syntax

expressions $\mathpre{\exp}$ $\mathpre{::=}$ $\mathpre{\mathid{x}^{\s}}$ | $\mathpre{\mathid{c}^{\s}}$ | $\mathpre{\exp\ \exp}$
| $\mathpre{\elambda{\mathid{x}}{\s}{\exp}{\e}}$
| $\mathpre{\eval{\mathid{x}^\s}{\exp}{\exp}}$
| $\mathpre{\ecase{\exp}{\exp}{\exp}}$
| $\mathpre{\exp\ [\s]}$ | $\mathpre{\Lambda \a^{\kk}~.~\exp}$
 
types $\mathpre{\t^\kk}$ $\mathpre{::=}$ $\mathpre{\a^\kk}$ type variable
| $\mathpre{\mathid{c}^{\kk_0}{\langle}\t_1^{\kk_1},...,\t_\mathid{n}^{\kk_\mathid{n}}{\rangle}}$ $\mathpre{{\scriptstyle \kk_0~=~(\kk_1,...,\kk_\mathid{n})~{\rightarrow}~\kk}}$
 
kinds $\mathpre{\kk}$ $\mathpre{::=}$ $\mathpre{\star}$ | $\mathpre{\ke}$ values, effects
| $\mathpre{\kl}$ effect constants
| $\mathpre{\ku}$ user effects
| $\mathpre{(\kk_1,...,\kk_\mathid{n})~{\rightarrow}~\kk}$ type constructor
 
type scheme $\mathpre{\s}$ $\mathpre{::=}$ $\mathpre{\forall\a^{\kk}.~\s}$ | $\mathpre{\t^{*}}$
const $\mathpre{()}$ $\mathpre{::}$ $\mathpre{\star}$ unit type
$\mathpre{\mathid{bool}}$ $\mathpre{::}$ $\mathpre{\star}$ bool type
$\mathpre{(\_~{\rightarrow}~\_\,\_)}$ $\mathpre{::}$ $\mathpre{(\star,\ke,\star)~{\rightarrow}~\star }$ functions
$\mathpre{\empeffect}$ $\mathpre{::}$ $\mathpre{\ke}$ empty effect
$\mathpre{{\langle}\_}$ |$\mathpre{\_{\rangle}}$ $\mathpre{::}$ $\mathpre{(\kl,\ke)~{\rightarrow}~\ke}$ effect extension
$\mathpre{\mathid{exn},\mathid{div}}$ $\mathpre{::}$ $\mathpre{\kl}$ partial, divergent
$\mathpre{\toue{\langle}\_{\rangle}}$ $\mathpre{::}$ $\mathpre{\ku {\rightarrow}~\kl}$ user effects
$\mathpre{\tdict{\_}}$ $\mathpre{::}$ $\mathpre{\ke {\rightarrow}~\star}$ effect to universe

Syntactic sugar:

effects $\mathpre{\e}$ $\mathpre{\doteq}$ $\mathpre{\t^{\ke}\hspace{\textwidth}}$
effect variables $\mathpre{\mu}$ $\mathpre{\doteq}$ $\mathpre{\a^{\ke}}$
closed effects $\mathpre{{\langle}\mathid{l}_1,...,\mathid{l}_\mathid{n}{\rangle}}$ $\mathpre{\doteq}$ $\mathpre{{\langle}\mathid{l}_1,...,\mathid{l}_\mathid{n}~}$ | $\mathpre{\mdmathindent{1}\empt{\rangle}}$
single effect $\mathpre{\mathid{l}}$ $\mathpre{\doteq}$ $\mathpre{{\langle}\mathid{l}{\rangle}}$
user effects $\mathpre{\mathid{l}^{\ku}}$ $\mathpre{\doteq}$ $\mathpre{\mdmathindent{1}\toue {\langle}{\mathid{l}^{\ku}}{\rangle}~}$

Figure 3. Syntax of explicitly typed Koka, $\mathpre{\lambda^{\kk\mathsf{u}}}$.

Figure 3 defines the syntax of expressions and types of $\mathpre{\lambda^{\kk\mathsf{u}}}$, a polymorphic explicitly typed $\mathpre{\lambda}$-calculus. $\mathpre{\lambda^{\kk\mathsf{u}}}$ is System F [12, 28] extended with effect types.

Expressions. $\mathpre{\lambda^{\kk\mathsf{u}}}$ expressions include typed variables $\mathpre{\mathid{x}^\s}$, typed constants $\mathpre{\mathid{c}^\s}$, $\mathpre{\lambda}$-abstraction $\mathpre{\elambda{\mathid{x}}{\s}{\exp}{\e}}$, application $\mathpre{\exp\ \exp}$, value bindings $\mathpre{\eval{\mathid{x}^\s}{\exp}{\exp}}$, if combinators $\mathpre{\ecase{\exp}{\exp}{\exp}}$, type application $\mathpre{\exp\ [\s]}$ and type abstraction $\mathpre{\Lambda \a^{\kk}~.~\exp}$. Each value variable is annotated with its type and each type variable is annotated with its kind. Finally, each $\mathpre{\lambda}$-abstraction $\mathpre{\elambda{\mathid{x}}{\s}{\exp}{\e}}$ is annotated with its result effect $\mathpre{\e}$ which is necessary to check effect types.

In strict languages one distinguishes between values and expressions to restrict type abstraction and application over value expressions. For simplicity, here we omit this separation and rely on the Koka type checker to guarantee that we only generalize over expressions with a total effect (hence there is no need for the `value restriction' [20]).

Types and type schemes. Types consist of explicitly kinded type variables $\mathpre{\a^\kk}$ and application of constant type constructors $\mathpre{\mathid{c}^{\kk_0}{\langle}\t_1^{\kk_1},...,\t_\mathid{n}^{\kk_\mathid{n}}{\rangle}}$, where the type constructor $\mathpre{\mathid{c}}$ has the appropriate kind $\mathpre{{\kk_0~=~(\kk_1,...,\kk_\mathid{n})~{\rightarrow}~\kk}}$. We do not provide special syntax for function types, as they can be modeled by the constructor $\mathpre{(\_~{\rightarrow}~\_\,\_)~::~(\star,\ke,\star)~{\rightarrow}~\star }$ that, unlike the usual function type, explicitly reasons for the effect produced by the function. Finally, types can be qualified over type variables to yield type schemata.

Kinds. Well-formedness of types is guaranteed by a kind system. We annotate the type $\mathpre{\t}$ with its kind $\mathpre{\kk}$, as $\mathpre{\t^\kk}$. Apart from the kind of types ($\mathpre{*}$) and the kind of functions $\mathpre{{\rightarrow}}$, we have kinds for effect rows ($\mathpre{\ke}$), effect constants ($\mathpre{\kl}$), and user-defined effects ($\mathpre{\ku}$). We omit the kind $\mathpre{\kk}$ of the type $\mathpre{\t^\kk}$, and write $\mathpre{\t}$, when $\mathpre{\kk}$ is immediately apparent or not relevant. For clarity, we use $\mathpre{\alpha}$ for regular type variables and $\mathpre{\mu}$ for effect type variables. Finally, we write $\mathpre{\e}$ for effects, i.e. types of kind $\mathpre{\ke}$.

Effects. Effects are types. Effect types are defined as a row of effect labels $\mathpre{\mathid{l}}$. Such effect row is either empty $\mathpre{\empt}$, a polymorphic effect variable $\mathpre{\mu}$, or an extension of an effect row $\mathpre{\e}$ with an effect constant $\mathpre{\mathid{l}}$, written as $\mathpre{{\langle}\mathid{l}|\e{\rangle}}$. Effect constants are either built-in Koka effects, i.e. anything that is interesting to our language like exceptions ($\mathpre{\ec{\mathid{exn}}}$), divergence ($\mathpre{\ec{\mathid{div}}}$) etc. or lifted user-defined monadic effects like the ambiguous effect $\mathpre{\mathkw{amb}^\ku ::~\ku}$. Note that for an effect row to be well-formed we use the $\mathpre{\mathkw{user}}$ effect function to lift $\mathpre{\mathkw{user}{\langle}\mathkw{amb}^\ku{\rangle}~::~\kl}$ to the appropriate kind $\mathpre{\kl}$. For simplicity, in the rest of this section we omit the explicit lifting and write $\mathpre{\mathkw{amb}^\ku}$ to denote $\mathpre{\mathkw{user}{\langle}\mathkw{amb}^\ku{\rangle}}$ when a label of kind $\mathpre{\kl}$ is expected.

Finally, Figure 3 includes definition of type constants and syntactic sugar required to simplify the rest of this section.

Type and Effect Checking $\mathpre{\fbox{\ensuremath{{\vdash}~\mathid{e}~:~\s |~\e}}}$

(T-Con) $\mathpre{\inference{}{{\vdash}~\mathid{c}^{\s}~:~\s |~\e}}$(T-Var) $\mathpre{\inference{}{{\vdash}~\mathid{x}^{\s}~:~\s |~\e}}$

(T-TLam) $\mathpre{\inference{{\vdash}~\mathid{e}~:~\s |~\empeffect }{{\vdash}~\Lambda \a^{\kk}.~\mathid{e}~:~\forall \a^{\kk}.~\s |~\e}}$   (T-TApp) $\mathpre{\inference{{\vdash}~\mathid{e}~:~\forall \a.~\s |~\e}{{\vdash}~\mathid{e}[\t]~:~\s[\a \mapsto \t]~|~\e }}$

(T-Lam) $\mathpre{\inference{{\vdash}~\mathid{e}~:~\t_2~|~\e}{{\vdash}~\elambda{\mathid{x}}{\t_1}{\mathid{e}}{\e}~:~\t_1~{\rightarrow}~\e\ \t_2~~|~\e'}}$

(T-App) $\mathpre{\inference{{\vdash}~\mathid{e}_{1}~:~\t_1~{\rightarrow}~\e\ \t_2~|~\e \quad {\vdash}~\mathid{e}_{2}~:~\t_1~|~\e }{{\vdash}~\mathid{e}_{1}~\mathid{e}_{2}~:~\t_2~|~\e }}$

(T-Val) $\mathpre{\inference{{\vdash}~\mathid{e}_{1}~:~\s_1~|~\e \quad {\vdash}~\mathid{e}_{2}~:~\s_2~|~\e }{{\vdash}~\mathkw{val}~\mathid{x}~=~\mathid{e}_{1};~\mathid{e}_{2}~:~\s_2~|~\e }}$

(T-If) $\mathpre{\inference{{\vdash}~\mathid{e}~:~\mathkw{bool}~|~\e \quad {\vdash}~\mathid{e}_{1}~:~\s |~\e \quad {\vdash}~\mathid{e}_{2}~:~\s |~\e }{{\vdash}~\mathkw{if}~\mathid{e}~\mathkw{then}~\mathid{e}_{1}~\mathkw{else}~\mathid{e}_{2}:~\s |~\e }}$  
Type Checking $\mathpre{\fbox{\ensuremath{{\vdash}~\mathid{e}~:~\s }}}$

(T-If) $\mathpre{\inference{{\vdash}~\mathid{e}~:~\s |~\e }{{\vdash}~\mathid{e}~:~\s }}$


Figure 4. Type rules for explicitly typed Koka.

Type rules. Figure 4 describes type rules for $\mathpre{\lambda^{\kk\mathsf{u}}}$ where the judgment $\mathpre{{\vdash}~\mathid{e}~:~\s |~\e}$ assigns type $\mathpre{\s}$ and effect $\mathpre{\e}$ to an expression $\mathpre{\mathid{e}}$. All the rules are equivalent to the System F rules, except for rule (Lam) where the effect of the function in the type is drawn from the effect annotation in the $\mathpre{\lambda}$-abstraction. $\mathpre{\lambda^{\kk\mathsf{u}}}$ is explicitly typed, in that variables are annotated with their type and functions with their effect, hence, type checking does not require an environment. By construction, the Koka type inference rules always produce well-formed $\mathpre{\lambda^{\kk\mathsf{u}}}$. Soundness of $\mathpre{\lambda^{\kk\mathsf{u}}}$ follows from soundness of Koka as described in [20]. Next, we write $\mathpre{{\vdash}~\mathid{e}~:~\s}$ if there exists a derivation $\mathpre{{\vdash}~\mathid{e}~:~\s |~\e }$ for some effect $\mathpre{\e}$.

3.2. Type inference for effect and morphism declarations

Declarations of User Effects and Morphisms $\mathpre{\fbox{\ensuremath{\Gamma {\vdash}~\mathid{def}~:~\Gamma }}}$

(Eff)$\mathpre{\inference{\ontop{\Gamma,\mu^\ke,\alpha^\star\ {\vdash}_\mathkw{k}~\t ::\star \quad \Gamma'~=~\Gamma,~\mathid{M}_\mathid{eff}{\langle}\mu,\alpha{\rangle}=\t\quad \Gamma'\ {\vdash}_\mathkw{k}~\mathid{e}_{1}~:~\forall\alpha\mu.~\alpha {\rightarrow}~\mu\ \mathid{M}_\mathid{eff}{\langle}\mu,\alpha{\rangle}}{\Gamma'\ {\vdash}_\mathkw{k}~\mathid{e}_{2}~:~\forall\mu\alpha\beta.~(\mathid{M}_\mathid{eff}{\langle}\mu,\alpha{\rangle},~\alpha {\rightarrow}~\mu\ \mathid{M}_\mathid{eff}{\langle}\mu,\beta{\rangle})~{\rightarrow}~\mu\ \mathid{M}_\mathid{eff}{\langle}\mu,\beta{\rangle}~}~}{\Gamma\ {\vdash}~\mathkw{effect}~\mathid{eff}{\langle}\mu,\alpha{\rangle}~=~\t\ \{~\mathid{unit}~=~\mathid{e}_{1};~\mathid{bind}~=~\mathid{e}_{2}~\}~:\ontoplthree{\Gamma',~\mathid{eff}^\ku,~\mathid{dict}_{\mathid{eff}}~:~\mathid{tdict}{\langle}\mathid{M}_\mathid{eff}{\rangle}}{~~\mathid{to}_{\mathid{eff}}~:~\forall\alpha\mu.~(\mathid{M}_\mathid{eff}{\langle}\mu,\alpha{\rangle})~{\rightarrow}~{\langle}\mathid{eff}|\mu{\rangle}~\alpha,}{~~\mathid{from}_{\mathid{eff}}~:~\forall\alpha\beta\mu.~(()~{\rightarrow}~{\langle}\mathid{eff}|\mu{\rangle}~\alpha)~{\rightarrow}~\mu\ \mathid{M}_\mathid{eff}{\langle}\mu,\alpha{\rangle}~}}}$

(Morph)$\mathpre{\inference{\mathid{s}~\equiv{\langle}\mathid{l}_1,...,\mathid{l}_\mathid{n}{\rangle}~\quad \mathid{t}~\equiv{\langle}\mathid{l}_1,...,\mathid{l}_\mathid{n},...,\mathid{l}_\mathid{m}{\rangle}~\quad \Gamma\ {\vdash}_\mathkw{k}~\mathid{e}~:~\forall \a \mu.\ \mathid{M}_{\mathid{s}}{\langle}\mu,~\a{\rangle}~{\rightarrow}~\mu\ \mathid{M}_{\mathid{t}}{\langle}\mu,~\a{\rangle}~}{{\Gamma\ {\vdash}~\mathkw{morphism}~\mathid{s}~\mathid{t}~\{~\mathid{e}~\}~:}{\Gamma,~\xmorph{\mathid{s}}{\mathid{t}}~:~\forall \a \mu.\ \mathid{M}_{\mathid{s}}{\langle}\mu,~\a{\rangle}~{\rightarrow}~\mu\ \mathid{M}_{\mathid{t}}{\langle}\mu,~\a{\rangle}}}}$


Figure 5. Type rule for effect and morphism declarations.

In this subsection we present how Koka preprocesses the effect and morphism declarations provided by the user. Figure 5 summarizes the rules that the Koka compiler follows to desugar the user definitions to $\mathpre{\lambda^{\kk\mathsf{u}}}$. After desugaring, Koka proceeds to effect- and type- inference as presented in previous work [19, 20].

3.2.1. Effect Declarations

The Identity Effect. Before we look at the general type inference rule for effect declarations we start with a concrete example, namely the identity effect $\mathpre{\eid}$:

effect uide,a = a {
 function unit(x) { x }
 function bind(x,f) { f(x) }
}

From the above effect definition, initially, Koka generates a type alias that isolates the first line of the definition and relates the effect name with its monadic representation.

$\mathpre{\mathkw{alias}~\mathid{M}_\eid{\langle}\e,\alpha{\rangle}~=~\alpha}$

Then, Koka checks well-formedness of the effect definition, by (type-) checking that $\mathpre{\mathid{unit}}$ and $\mathpre{\mathid{bind}}$ are the appropriate monadic operators. Concretely, it checks that

\[\begin{mdmathpre}%mdk \mdmathindent{2}\mathid{unit}~:~\forall\alpha\mu.~\alpha {\rightarrow}~\mu\ \mathid{M}_{\eid}{\langle}\mu,\alpha{\rangle}\\ \mdmathindent{2}\mathid{bind}~:~\forall\alpha\beta\mu.~(\mathid{M}_{\eid}{\langle}\mu,\alpha),~\alpha {\rightarrow}~\mu\ \mathid{M}_{\eid}{\langle}\mu,\beta{\rangle})~{\rightarrow}~\mu\ \mathid{M}_{\eid}{\langle}\mu,\beta{\rangle} \end{mdmathpre}%mdk \]

Given the definitions of unit and bind, Koka automatically constructs the primitives required by the rest of the program to safely manipulate the identity effect:

Dictionaries. The first three values are user-visible but the final dictionary value is only used internally during the monadic translation. The type of the effect dictionary (e.g. $\mathpre{\mathid{dict}_{\eid}}$), is a structure that contains the monadic operators $\mathpre{\mathid{unit}}$ and $\mathpre{\mathid{bind}}$ of the effect. It can as well include the monadic $\mathpre{\mathid{map}}$ which will otherwise be automatically derived from $\mathpre{\mathid{unit}}$ and $\mathpre{\mathid{bind}}$, and the $\mathpre{\mathid{bind}_\mathid{catch}}$ method to interact with primitive exceptions. Thus, we define the dictionary structure as a type that is polymorphic on the particular monad, represented as type variable $\mathpre{\mathid{m}~::~{(\ke,\star)~{\rightarrow}~\star}}$:

\[\begin{mdmathpre}%mdk \mathkw{struct}~\mathid{tdict}{\langle}{}\mathid{m}{\rangle}~\{\\ \mdmathindent{2}\mathid{unit}~:~\forall\alpha\mu.~\alpha {\rightarrow}~\mu\ \mathid{m}{\langle}\mu,\alpha{\rangle}\\ \mdmathindent{2}\mathid{map}~~:~\forall\alpha\beta\mu.~(\mathid{m}{\langle}\mu,\alpha{\rangle},~\alpha {\rightarrow}~\beta)~{\rightarrow}~\mu\ \mathid{m}{\langle}\mu,\beta{\rangle}~~\\ \mdmathindent{2}\mathid{bind}~:~\forall\alpha\beta\mu.~(\mathid{m}{\langle}\mu,\alpha{\rangle},~\alpha {\rightarrow}~\mu\ \mathid{m}{\langle}\mu,\beta{\rangle})~{\rightarrow}~\mu\ \mathid{m}{\langle}\mu,\beta{\rangle}\\ \mdmathindent{2}\mathid{bind}_\mathid{catch}:~\forall\alpha\mu.~(\mathid{m}{\langle}{\langle}\mathid{exn}|\mu{\rangle},\alpha{\rangle}{\rangle},~\mathid{exc}~{\rightarrow}~\mu\ \mathid{m}{\langle}\mu,\alpha{\rangle})~{\rightarrow}~\mu\ \mathid{m}{\langle}\mu,\alpha{\rangle}\} \end{mdmathpre}%mdk \]

With this we can type $\mathpre{\mathid{dict}_{\eid}~:~\mathid{tdict}{\langle}\mathid{M}_{\eid}{\rangle}}$.

General user-defined effects. Figure 5 generalizes the previous concrete example to any user-defined effect declaration. The judgment:

\[\begin{mdmathpre}%mdk \Gamma\ {\vdash}~\mathkw{effect}~\mathid{eff}{\langle}\mu,\alpha{\rangle}~=~\t{\langle}\mu,\alpha{\rangle}\ \{~\mathid{unit}~=~\mathid{e}_{1};~\mathid{bind}~=~\mathid{e}_{2}~\}~:~\Gamma' \end{mdmathpre}%mdk \]

states that under a kind- and type- environment $\mathpre{\Gamma}$, the effect declaration $\mathpre{\mathid{eff}}$ results in a new type environment $\mathpre{\Gamma'}$ that is extended with the needed types and primitives implied by $\mathpre{\mathid{eff}}$. As shown in Figure 5, we first check well-formedness of the effect types, and then check that $\mathpre{\mathid{unit}}$ and $\mathpre{\mathid{bind}}$ operations have the proper types. Finally, the environment is extended with the corresponding types and values.

3.2.2. Morphism Declarations

As a morphism example, we assume the existence of the two user defined effects from the Overview (§ 2), the ambiguous and the behaviour. Moreover, we assume that the user appropriately defined their joined effect amb, beh. From these three user effect definitions, Koka desugarer yields three aliases, say:

\[\begin{mdmathpre}%mdk \mathkw{alias}~\mathid{M}_{\mathit{amb}}{\langle}\e,\alpha{\rangle}~=~\mathkw{list}{\langle}\alpha{\rangle}\\ \mathkw{alias}~\mathid{M}_{\mathit{beh}}{\langle}\e,\alpha{\rangle}~=~\mathkw{time}~{\rightarrow}\e\ \alpha\\ \mathkw{alias}~\mathid{M}_{{\langle}\mathit{amb},~\mathit{beh}{\rangle}}{\langle}\e,\alpha{\rangle}~=~\mathkw{time}~{\rightarrow}\e\ \mathkw{list}{\langle}\alpha{\rangle} \end{mdmathpre}%mdk \]

Then, the user can define morphisms that go from amb or beh to the combined effect amb, beh

morphism amb amb, beh {
 fun(xs : lista) : time e lista{
  fun(t){xs}
 }
}
   
morphism beh amb, beh {
 fun(x : time e a) : time e lista{
  fun(t){[x(t)]}
 }
}

From the above definitions, Koka will generate two morphism functions:

\[\begin{mdmathpre}%mdk \mdmathindent{2}\xmorph{\mathit{amb}}{{\langle}\mathit{amb},~\mathit{beh}{\rangle}}~:~\forall\alpha \mu.~\mathid{M}_{\mathit{amb}}{\langle}\mu,~\alpha{\rangle}~{\rightarrow}~\mu\ \mathid{M}_{{\langle}\mathit{amb},~\mathit{beh}{\rangle}}{\langle}\mu,\alpha{\rangle}\\ \mdmathindent{2}\xmorph{\mathit{beh}}{{\langle}\mathit{amb},~\mathit{beh}{\rangle}}~:~\forall\alpha \mu.~\mathid{M}_{\mathit{beh}}{\langle}\mu,~\alpha{\rangle}~{\rightarrow}~\mu\ \mathid{M}_{{\langle}\mathit{amb},~\mathit{beh}{\rangle}}{\langle}\mu,\alpha{\rangle} \end{mdmathpre}%mdk \]

The above morphisms are internal Koka functions that will be used at the translation phase to appropriately lift the monadic computations.

General user-defined morphisms. Figure 5 generalizes the previous concrete example to any morphism declaration. The judgment:

\[\begin{mdmathpre}%mdk \Gamma\ {\vdash}~\mathkw{morphism}~\mathid{s}~\mathid{t}\ {\mathid{e}}~:~\Gamma' \end{mdmathpre}%mdk \]

states that under a kind- and type- environment $\mathpre{\Gamma}$, the morphism declaration from effect raws $\mathpre{\mathid{s}}$ to $\mathpre{\mathid{t}}$ results in a new type environment $\mathpre{\Gamma'}$ that is extended with the morphism from the source effect $\mathpre{\mathid{s}}$ to the target effect $\mathpre{\mathid{t}}$, when the expression $\mathpre{\mathid{e}}$ has the appropriate morphism type. The first premise ensures that $\mathpre{\mathid{s}}$ is always a sub-effect of the target effect $\mathpre{\mathid{t}}$.

3.3. Type-directed monadic translation

Next, we define the type-directed monadic translation $\mathpre{\exp \mathop{\leadsto}\aef \exp'~|~\ue}$ that takes an effect expression $\mathpre{\exp}$ to the monadic expression $\mathpre{\exp'}$.

Computed effects. Our translation needs two effects $\mathpre{\e}$ and $\mathpre{\ue}$: the maximum (inferred) effect $\mathpre{\e}$ and the minimum (computed) effect $\mathpre{\ue}$. After type inference, every function body has one unified effect $\mathpre{\e}$, that consists of the unification of all the effects in that function. Our translation computes bottom-up the minimal user-defined portion of each separate sub-expression, where $\mathpre{\ue}$ should always be contained in $\mathpre{\e}$. Specifically, we define computed effects $\mathpre{\ue}$ as effect types $\mathpre{\e}$ that have the following grammar:

\[\begin{mdmathpre}%mdk \ue ::=~\mu{}~|~{\langle}\mathid{l}_1^\ku,~...,~\mathid{l}_\mathid{n}^\ku{\rangle}~~\quad (\mathid{n}\ge 0) \end{mdmathpre}%mdk \]

Thus, computed effects can be a row of user-effect labels (including the empty row) or an effect variable. Note that because user effects are always constants, and according to the equivalence rules for rows [20], we consider computed effect rows equal up to reordering. For example $\mathpre{\mdmathindent{1}{\langle}\mathid{l}_2^\ku,~\mathid{l}_1^\ku{\rangle}~\equiv{}~{\langle}\mathid{l}_1^\ku,~\mathid{l}_2^\ku{\rangle}}$.

As shown by the grammar, the computed effects are restricted in that a row of monadic effects cannot end with a polymorphic tail $\mathpre{\mu}$. This limits the functions that a user can write: no user-defined effects can be in a row that has a polymorphic tail. We believe that this restriction is not too severe in practice since it only restricts functions that are higher-order over user-defined effects where the function parameter is open-ended in the side-effects it can have. This is quite unusual and easy to circumvent by stating the allowed effects explicitly. The advantage of adding this restriction is great though: we completely circumvent the need to add constraints to the type language and can simplify the translation significantly compared to earlier work [31].

We convert a regular effect type $\mathpre{\e}$ to a computed effect $\mathpre{\tou\e}$, and dually, we apply $\mathpre{\tononuser{\e}}$ to an effect $\mathpre{\e}$ to remove the user defined effects:

\[\begin{mdmathpre}%mdk \tou{{\langle}\mathid{l}^\ku |~\e{\rangle}}~&=~{\langle}\mathid{l}^\ku |~\tou\e{\rangle}~&~\mathkw{if}~\tou\e \neq \mu &~\tononuser{{\langle}\mathid{l}^\ku |~\e{\rangle}}&=~~\tononuser{\e}\\ \tou{{\langle}\mathid{l}^\kk |~\e{\rangle}}~&=~\tou\e \quad &~\mathkw{if}~\kk \neq \ku &~\tononuser{{\langle}\mathid{l}^\kk |~\e{\rangle}}&=~{\langle}\mathid{l}^\kk |~\tononuser{\e}~{\rangle}~\\ \tou{\empeffect}~~~~~~~~~~~&=~\empeffect &~~~~~~~~~~~~~~~~~~~~&~\tononuser{\empeffect}~~~~~~~~~~&=~\empeffect\\ \tou{\mu}~~~~~~~~~~&=~\mu &~~~~~~~~~~~~~~~~~~~~&~\tononuser{\mu}~~~~~~~~~&=~\mu \end{mdmathpre}%mdk \]

Note that this function is partial: when a type is passed that combines a user-defined effect with a polymorphic tail it fails and the compiler raises an error that the program is too polymorphic.

To join computed effects we use the $\mathpre{\oplus{}{}}$ operator:

\[\begin{mdmathpre}%mdk \empeffect \oplus \ue_2~~~~&=&~\ue_2~\xstrut\\ \mu \oplus \mu &=&~\mu \xstrut\\ {\langle}\mathid{l}~|~\ue_1{\rangle}~\oplus {\langle}\mathid{l}~|~\ue_2{\rangle}~&=&~{\langle}\mathid{l}~|~\ue_1~\oplus \ue_2{\rangle}~\xstrut\\ {\langle}\mathid{l}~|~\ue_1{\rangle}~\oplus \ue_2~&=&~{\langle}\mathid{l}~|~\ue_1~\oplus \ue_2{\rangle}~\quad \mathkw{if}~\mathid{l}~\notin \ue_2~\xstrut \end{mdmathpre}%mdk \]

Again, this function is partial but we can show that the usage in the translation over a well-typed koka program never leads to an undefined case.

\[\begin{mdmathpre}%mdk \xbind{\empeffect}{\ue}{\mathid{x}}{\mathid{e}_\mathid{x}}{\mathid{e}}{\e}~~~~~~=~\mathkw{val}~\mathid{x}~=~\mathid{e}_\mathid{x};~\mathid{e}~\\ \xbind{\ue_\mathid{x}}{\empeffect}{\mathid{x}}{\mathid{e}_\mathid{x}}{\mathid{e}}{\e}~~~~=~\mathid{dict}_{\ue_\mathid{x}}.\mathid{map}~{\langle}\s_\mathid{x},\s,\e{\rangle}(\mathid{e}_\mathid{x},~\lambda^{\empeffect}~\mathid{x}~:~\s_\mathid{x}.~\mathid{e})\\ \mdmathindent{2}\mathkw{where}~\\ \mdmathindent{5}{\vdash}~\mathid{e}_\mathid{x}:\tmonad{\ue_\mathid{x}}{\e}{\s_\mathid{x}},~{\vdash}~\mathid{e}:\s\\ \xbind{\ue_\mathid{x}}{\ue}{\mathid{x}}{\mathid{e}_\mathid{x}}{\mathid{e}}{\e}~=~\mathid{dict}_{\ue_\mathid{x}~\oplus \ue}.\mathid{bind}{\langle}\s_\mathid{x},\s,\e{\rangle}(\mathid{e}'_\mathid{x},~\mathid{e}')\\ \mdmathindent{2}\mathkw{where}\\ \mdmathindent{5}\mathid{e}'_\mathid{x}~=~\xlift{\ue_\mathid{x}}{(\ue_\mathid{x}~\oplus \ue)}{\mathid{e}_\mathid{x}}{\e}\\ \mdmathindent{5}\mathid{e}'~=~\lambda^{\tononuser{\e}}~\mathid{x}~:~\s_\mathid{x}.~(\xlift{\ue}{(\ue_\mathid{x}~\oplus \ue)}{\mathid{e}}{\e})\\ \mdmathindent{5}{\vdash}~\mathid{e}_\mathid{x}:\tmonad{\ue_\mathid{x}}{\e}{\s_\mathid{x}},~{\vdash}~\mathid{e}:\tmonad{\ue}{\e}{\s} \end{mdmathpre}%mdk \]
\[\begin{mdmathpre}%mdk \xlift{\ue}{\ue}{\mathid{e}}{\e}~~&~=~&~\mathid{e}~&~\xstrut\\ \xlift{\empeffect}{\ue}{\mathid{e}}{\e}~~~&~=~&~\mathid{dict}_{\ue}.\mathid{unit}{\langle}\s,~\e{\rangle}(\mathid{e})~&~\mathkw{where}\ \ue \neq \empeffect,~{\vdash}~\mathid{e}~:~\s\\ \xlift{\ue_\mathid{s}}{\ue_\mathid{t}}{\mathid{e}}{\e}~&~=~&~\xmorph{\ue_\mathid{s}}{\ue_\mathid{t}}{\langle}\s,~\e{\rangle}(\mathid{e})~&~\mathkw{where}\ {\vdash}~\mathid{e}~:~\tmonad{\ue_\mathid{s}}{\e}{\s} \end{mdmathpre}%mdk \]

Figure 6. Helper functions for binding and lifting.

Translation $\mathpre{\fbox{\ensuremath{\mathid{e}~\leadsto\aef \mathid{e}~|~\ue}}}$

(Con)$\mathpre{\inference{}{\mathid{c}^{\s}~\mathop{\leadsto}\aef \mathid{c}^{\ttr{\s}}~|~\empeffect}}$     (Var)$\mathpre{\inference{}{\mathid{x}^{\s}~\mathop{\leadsto}\aef \mathid{x}^{\ttr{\s}}~|~\empeffect}}$     (Lam)$\mathpre{\inference{\mathid{e}~\mathop{\leadsto}\aef \mathid{e}'~|~\uen }{\elambda{\mathid{x}}{\t}{\exp}{\e}~\mathop{\leadsto}\translationeffect{\e_0}~\elambda{\mathid{x}}{\ttr{\t}}{\xlift{\uen}{\toen{\e}}{\mathid{e}'}{\e}}{\tononuser{\e}}~|~\empeffect}}$

(TLam) $\mathpre{\inference{\mathid{e}~\mathop{\leadsto}\aef \mathid{e}'~|~\empeffect \quad \kk \neq \ke}{\Lambda \a^{\kk}.~\mathid{e}~\mathop{\leadsto}\aef \Lambda \a^{\kk}.~\mathid{e}'~|~\empeffect}}$     (TLam-E) $\mathpre{\inference{\mathid{e}~\mathop{\leadsto}\aef \mathid{e}'~|~\empeffect}{\Lambda \mu.~\mathid{e}~\mathop{\leadsto}\aef \Lambda \mu .\elambda{\vardict{\mu}}{\tdict{\tou\mu}}{\exp'}{\empeffect}~|~\empeffect}}$

(TApp)$\mathpre{\inference{\mathid{e}~\mathop{\leadsto}\aef \mathid{e}'~|~\ue \quad \kk \neq \ke}{\mathid{e}[\t^{\kk}]~~\mathop{\leadsto}\aef \mathid{e}'~[\ttr{\t^{\kk}}]~|~\ue}}$     (TApp-E)$\mathpre{\inference{\mathid{e}~\mathop{\leadsto}\aef \mathid{e}'~|~\ue }{\mathid{e}[\e']~~\mathop{\leadsto}\aef \mathid{e}'[\ttr{\e'}]~\mathid{dict}_{\tou{\ttr{\e'}}}\ |~\ue}}$

(App)$\mathpre{\inference{\mathid{e}_{1}~\mathop{\leadsto}\aef \mathid{e}_{1}'~|~\ue_1~\quad \mathid{e}_{2}~\mathop{\leadsto}\aef \mathid{e}_{2}'~|~\ue_2~\quad \compute{\mathid{e}_{1}}{\ue_3}~~\quad \ue =~\ue_1~\oplus \ue_2~\oplus \ue_3}{\mathid{e}_{1}~\mathid{e}_{2}~\mathop{\leadsto}\aef \xbind{\ue_1}{\ue_2\oplus\ue_3}{\mathid{f}}{\mathid{e}_{1}'}{\xbind{\ue_2}{\ue_3}{\mathid{y}}{\mathid{e}_{2}'}{\mathid{f}~\mathid{y}}{\e}}{\e}~|~\ue}}$

(Val)$\mathpre{\inference{\mathid{e}_{1}~\mathop{\leadsto}\aef \mathid{e}_{1}'~|~\ue_1~\quad \mathid{e}_{2}~\mathop{\leadsto}\aef \mathid{e}_{2}'~|~\ue_2}{\mathkw{val}~\mathid{x}~=~\mathid{e}_{1};~\mathid{e}_{2}~\mathop{\leadsto}\aef \xbind{\ue_1}{\ue_2}{\mathid{x}}{\mathid{e}_{1}'}{\mathid{e}_{2}'}{\e}~|~\ue_1~\oplus \ue_2}}$

(If)$\mathpre{\inference{\mathid{e}_{1}~\mathop{\leadsto}\aef \mathid{e}_{1}'~|~\ue_1~\quad \mathid{e}_{2}~\mathop{\leadsto}\aef \mathid{e}_{2}'~|~\ue_2~\quad \mathid{e}_{3}~\mathop{\leadsto}\aef \mathid{e}_{3}'|~\ue_3~\quad \ue =~\ue_1~\oplus \ue_2~\oplus \ue_3}{\mathkw{if}~\mathid{e}_{1}~\mathkw{then}~\mathid{e}_{2}~\mathkw{else}~\mathid{e}_{3}~\mathop{\leadsto}\aef \xbind{\ue_1}{\ue_2\oplus\ue_3}{\mathid{y}}{\mathid{e}_{1}'}{\mathkw{if}~\mathid{y}~\mathkw{then}~\xlift{\ue_2}{\ue_2~\oplus\ue_3}{\mathid{e}_{2}'}{\e}~\mathkw{else}~\xlift{\ue_3}{\ue_2\oplus\ue_3}{\mathid{e}_{3}'}{\e}}{\e}~|~\ue}~}$


Figure 7. Basic translation rules. Any $\mathpre{\mathid{f}}$ and $\mathpre{\mathid{y}}$ are assumed fresh.

Type translation. The type operator $\mathpre{\ttr{\cdot}}$ translates effectful- to monadic types.

\[\begin{mdmathpre}%mdk \ttr{\a^{\kk}}~~~~~~~~~~&~=~&~\a^{\kk}\\ \ttr{\tau {\rightarrow}~\e\ \tau'}~&~=~&~\ttr{\tau}~{\rightarrow}~\tononuser{\e}~\tmonad{\tou\e}{\e}{\ttr{\tau'}}\\ \ttr{\mathid{c}^{\kk}{\langle}\t_1,~\dots,~\t_\mathid{n}{\rangle}}~&~=~&~\mathid{c}^{\kk}{\langle}\ttr{\t_1},~\dots,~\ttr{\t_\mathid{n}}{\rangle}~&&~\mathid{with}~\mathid{c}~\not =~{\rightarrow}\\ \ttr{\forall \a^{\kk}~.~\s}~~~~~~&~=~&~\forall \a^{\kk}~.~\ttr{\s}~&&~\mathid{with}~\kk \neq \ke\\ \ttr{\forall \a^{\ke}~.~\s}~~~~~~&~=~&~\forall \a^{\ke}~.~\tdict{\tou{\a^{\ke}}}~{\rightarrow}~\empeffect \ttr{\s}~ \end{mdmathpre}%mdk \]

For function types $\mathpre{\tau {\rightarrow}~\e\ \tau'}$ the effect $\mathpre{\e}$ is split to the build-in effect portion $\mathpre{\tononuser{\e}}$ and the user-defined portion $\mathpre{\tou\e}$. The effect of the translated type is only the build-in portion $\mathpre{\tononuser{\e}}$ while the result is monadically wrapped according to the user-defined portion $\mathpre{\tou\e}$ using the $\mathpre{\mathkw{mon}}$ operator

\[\begin{mdmathpre}%mdk \tmonad{\empeffect}{\e}{\s}~&~=~&~\s\\ \tmonad{{\langle}\mathid{l}_1^\ku ,~...~,~\mathid{l}_\mathid{n}^\ku{\rangle}}{\e}{\s}~&~=~&~\mathid{M}_{{\langle}\mathid{l}_1^\ku,~...~,~\mathid{l}_\mathid{n}^\ku{\rangle}}{\langle}\e,~\s{\rangle}~\mathkw{where}~\mathid{n}\ge 1\\ \tmonad{\mu}{\e}{\s}~&~=~&~(\mathid{evaluated}~\mathid{at}~\mathid{instantiation}) \end{mdmathpre}%mdk \]

The $\mathpre{\mathkw{mon}}$ operation derives a monadic result type and effect. For polymorphic effect types, $\mathpre{\mathkw{mon}}$ cannot be computed until instantiation. We therefore keep this type unevaluated until instantiation time. As such, it is really a dependent type (or a type parametrized over types). In our case, this is a benign extension to $\mathpre{\lambda^{\kk\mathsf{u}}}$ since $\mathpre{\lambda^{\kk\mathsf{u}}}$ is explicitly typed. After instantiation, the type argument is not polymorphic, thus $\mathpre{\mathkw{mon}}$ will return a concrete type.

The translation uses another dependent type to get the type of a polymorphic dictionary (see Figure 7):

\[\begin{mdmathpre}%mdk \tdict{\empeffect}~&~=~\mathid{tdict}{\langle}\mathid{M}_\eid{\rangle}\\ \tdict{{\langle}\mathid{l}_1^\ku,~...,~\mathid{l}_\mathid{n}^\ku{\rangle}}~&~=~\mathid{tdict}{\langle}\mathid{M}_{{\langle}\mathid{l}_1^\ku,~...,~\mathid{l}_\mathid{n}^\ku{\rangle}}{\rangle}~\mathkw{where}~\mathid{n}\ge 1\\ \tdict{\mu}~&~=~~\textrm{(evaluated at instantiation)} \end{mdmathpre}%mdk \]

Note that the type translation function $\mathpre{\ttr{\cdot}}$ reveals how the to_eff and from_eff functions are internally implemented. If we apply type translation to their signatures, we see that both become identity functions. For example, the type translation type of to_eff is $\mathpre{\ttr{\mathid{M}_\mathid{eff}{\langle}\e,\alpha{\rangle}~{\rightarrow}~{\langle}\mathid{eff}|\e{\rangle}~\alpha}}$ which is equivalent to $\mathpre{\mathid{M}_\mathid{eff}{\langle}\e,\alpha{\rangle}~{\rightarrow}~\e\ \mathid{M}_\mathid{eff}{\langle}\e,\alpha{\rangle}}$, i.e. we can implement to_eff simply as $\mathpre{\lambda \mathid{x}.~\mathid{x}}$. Similarly, from_eff is implemented as $\mathpre{\lambda \mathid{f}.~\mathid{f}()}$.

Monadic Abstractions. Figure 6 defines two syntactic abstractions that we use to lift and bind effect computations.

3.3.1. Monadic Translation

We use all the above operators to define the translation relation $\mathpre{\exp \mathop{\leadsto}\aef \exp'~|~\ue}$ as shown in Figure 7, where $\mathpre{\e}$ is inherited and $\mathpre{\ue}$ synthesized.

Values. Values have no effect, and compute $\mathpre{\empeffect}$. Rules (Con) and (Var) are simple: they only translate the type of the expression and leave the expression otherwise unchanged. Rule (Lam) states that when translating $\mathpre{\elambda{\mathid{x}}{\t}{\exp}{\e}}$ the type $\mathpre{\t}$ of the parameter is also translated. Moreover, the effect $\mathpre{\e}$ dictates the maximum effect in the translation of the body $\mathpre{\exp}$. Finally, we $\mathpre{\mathid{lift}}$ the body of the function from the computed minimum effect to $\mathpre{\e}$.

Type Operations. Type abstraction and application preserve the computed effect of the wrapped expression $\mathpre{\exp}$, and the Koka type system guarantees that type abstraction only happens over total expressions. In (TLam-E) we abstract over an effect variable $\mathpre{{\mu}}$, thus we add an extra value argument, namely, the dictionary of the effect that instantiates $\mathpre{\mu}$, i.e. $\mathpre{\vardict{\mu}~:~{\tdict{\tou\mu}}}$. Symmetrically, the rule (TApp-E) that translates application of the effect $\mathpre{\e'}$ applies the dictionary $\mathpre{\mathid{dict}_{\tou{\e'}}~:~{\tdict{\tou\e'}}}$ of the effect $\mathpre{\e'}$. Note that if the computed effect $\mathpre{\tou{\e'}}$ is a set of user-defined effects, say $\mathpre{{\langle}\mathkw{amb}{\rangle}}$, then the rule directly applies the appropriate dictionary $\mathpre{\mathid{dict}_\mathid{amb}}$, i.e. the dictionary value that Koka created from the $\mathpre{\mathkw{amb}}$ effect definition. If the computed effect $\mathpre{\tou{\e'}}$ is an effect variable $\mathpre{\mu}$, then the rule applies the appropriate variable dictionary $\mathpre{\vardict{\mu}}$, i.e. the variable abstracted by a rule (TLam-E) lower in the translation tree. By the way we defined computed effects, the final case is the computed effect $\mathpre{\tou{\e'}}$ to be the empty effect $\mathpre{\empeffect}$, and then the identity dictionary $\mathpre{\mathid{dict}_{\eid}}$ is applied. This is because in the computed effects world the total effect $\mathpre{\empeffect}$ is the identity effect $\mathpre{\eid}$. In our rules we used the $\mathpre{\empeffect}$ effect as it is more intuitive.

(Opt-TApp)$\mathpre{\inference{{\vdash}~\mathid{e}~:~\forall\mu,\alpha_1,...,\alpha_\mathid{m}.~\s_1~{\rightarrow}~{\langle}\mathid{l}_{1},...,\mathid{l}_\mathid{n}|\mu{\rangle}~\s_2}{\compute{\mathid{e}[\e,\alpha_1,...,\alpha_\mathid{m}]}{\tou{{\langle}\mathid{l}_{1},...,\mathid{l}_\mathid{n}{\rangle}}}}}$

(Opt-Default)$\mathpre{\inference{{\vdash}~\mathid{e}~:~\s_1~{\rightarrow}~\e\ \s_2}{\compute{\mathid{e}}{\tou\e}}}$


Figure 8. Computing minimal effects of function expressions.

Application. The rule (App) translates the application $\mathpre{\exp_1\ \exp_2}$. The minimal computed effect of the application is the union of the computed effects of the function $\mathpre{\exp_1}$ (that is $\mathpre{\ue_1}$), the argument $\mathpre{\exp_2}$ (that is $\mathpre{\ue_2}$) and the computed effect of the body of the the function. The maximum effect of the function is $\mathpre{\e}$ but using this maximum effect would lead to unoptimized translation, since every application would be unnecessarily lifted to its maximum effect. For example, if we wrote:

choose(id([False,True]))

then the unified effect for the id application would be amb and we would unnecessarily pass an amb dictionary to id and bind the result.

As an optimization, we compute the minimal effect as $\mathpre{\compute{\exp_1}{\ue_3}}$, which is presented in Figure 8. In this example, we can apply (Opt-TApp) and use a fully pure invocation of the $\mathpre{\mathid{id}([\mathid{False},\mathid{True}])}$ sub-expression. As it turns out, in practice this optimization is very important and saves much unnecessary binding, lifting, and passing of dictionaries. Since a row-based effect system like Koka uses simple unification, all sub expressions get unified with the final type. With this optimization we basically recover some of the subtyping but we can do it separately from the initial type inference. This is important in practice as we can now clearly separate the two complex phases and keep using simple unification during type inference.

Finally, the rule (Val) translates $\mathpre{\mathkw{val}}$-binding $\mathpre{\eval{\mathid{x}}{\mathid{e}_1}{\mathid{e}_2}}$ by binding $\mathpre{\mathid{e}_1}$ to $\mathpre{\mathid{x}}$ in $\mathpre{\mathid{e}_2}$. Similarly, the rule (If) translates $\mathpre{\ecase{\mathid{e}_1}{\mathid{e}_2}{\mathid{e}_3}}$ by first binding $\mathpre{\exp_1}$ to a fresh variable $\mathpre{\mathid{y}}$, since $\mathpre{\mathid{e}_1}$ may have user-defined effects and then lifting both branches to the computed effect $\mathpre{\ue}$ that is the union of the computed effects of the guard $\mathpre{\ue_1}$ and the two branches $\mathpre{\ue_2}$ and $\mathpre{\ue_3}$.

3.4. Soundness

From previous work on type inference for Koka [20] we have that the resulting explicitly typed Koka is well-typed, i.e.

Lemma 1.
(Explicit Koka is well-typed)
If $\mathpre{\Gamma{}~{\vdash}~\mathid{k}~:~\sigma{}~|~\e \mathop{\leadsto}~\mathid{e}}$ then $\mathpre{{\vdash}~\mathid{e}~:~\sigma |~\e}$.

Here, the relation $\mathpre{\Gamma{}~{\vdash}~\mathid{k}~:~\sigma{}~|~\e \mathop{\leadsto}~\mathid{e}}$ is the type inference relation defined in [20] where the source term $\mathpre{\mathid{k}}$ gets type $\mathpre{\sigma}$ with effect $\mathpre{\e}$ and a corresponding explicitly typed term $\mathpre{\mathid{e}}$. The new part in this paper is that our translation preserves types according to the $\mathpre{\llbracket\cdot\rrbracket}$ type translation:

Theorem 1.
(Type Preservation)
If  $\mathpre{{\vdash}~\mathid{e}~:~\sigma}$ and $\mathpre{\mathid{e}~\mathop{\leadsto}_\e \mathid{e}'~|~\empeffect}$, then $\mathpre{{\vdash}~\mathid{e}'~:~\llbracket\sigma\rrbracket}$.

Proof. In Appendix A we give a proof of soundness for a more general Theorem (General Type Preservation): if $\mathpre{{\vdash}~\mathid{e}~:~\sigma}$ and $\mathpre{\mathid{e}~\mathop{\leadsto}_\e \mathid{e}'~|~\ue}$, then $\mathpre{{\vdash}~\mathid{e}'~:~\tmonad{\ue}{\e}{\llbracket\sigma\rrbracket}}$. Theorem 1 follows as a direct implication for a computed effect $\mathpre{\ue =~\empeffect}$.

This property is strong since Koka has explicit effect types, i.e. it is not possible to have a typed translation simply by using $\mathpre{\bot}$, and as such it gives high confidence in the faithfulness of the translation. This is related to the types of bind and unit for example which are both guaranteed to be total functions (since they are polymorphic in the effect).

4. Implementation

We implemented monadic user-defined effects in Koka and the implementation is available at koka.codeplex.com. Koka's compiler is implemented in Haskell and it transforms Koka source code to JavaScript:

The goal of our implementation is to build a sound, complete, and efficient translation with minimum run-time overhead. We get soundness by § 3.4, and in § 4.2 we discuss that the translation is complete, modulo the monomorphic restriction. Moreover (§ 4.1), our translation is optimized to reduce any compile- and run-time overhead as far as possible. We conclude this section by a quantitative evaluation (§ 4.3) of our translation.

4.1. Optimizations

We optimized the translation rules of Figure 7 with three main optimization rules: only translate when necessary, generate multiple code paths for effect polymorphic functions, and use monadic laws to optimize bind structures.

Selective Translation. Looking at the existing Koka source code, we observed that most of the functions are user-defined effect free. A function is user-defined effect free when (1) it does not generate user-defined effects, (2) it is not effect polymorphic (as any abstract effect can be instantiated with a user-defined one), and (3) all the functions that calls or defines are user-defined effect free.

A user-defined effect free function is translated to itself. Thus our first optimization is to skip translation of such functions. This optimization is crucial in code that does not make heavy use of user-defined effects. As it turns out, 229 out of 287 Koka library functions are not translated!

Two versions of effect polymorphic functions. The translation rule (TApp-E) is quite inefficient when the applied effect $\mathpre{\e}$ is not user-defined: the identity dictionary is applied and it is used to perform identity monadic operators. User-defined effect free functions are the common case in Koka code, and as such they should not get polluted with identity dictionaries.

As an optimization, when translating an effect polymorphic function we create two versions of the function:

To soundly perform this optimization we use an environment with the effect variables that cannot be instantiated with user-defined effects, which is used as a proof that insertion of monadic operators is not required.

before translation after translation percentage increase
lines bytes lines bytes lines bytes
2678 89038 3248 121668 21.28 % 36.65%

Figure 9. Code size of Koka's library before and after translation.

Non-monadic versions are translated, but using the effect environment that constraints their effect variables to non-user effects. Still translation is required as these functions may use or produce user-defined effects. Though, in practice translation of non-monadic versions of functions is non-required and optimized by our previous optimization. It turns out that in Koka's library there are 58 polymorphic functions for which we created double versions. None of the non-monadic version requires translation.

Monadic Laws. As a final optimization we used the monadic laws to produce readable and optimized JavaScript code. Concretely, we applied the following three equivalence relations to optimize redundant occurrences:

\[\begin{mdmathpre}%mdk \mathkw{bind}(\mathkw{unit}~\mathid{x},~\mathid{f})~&~\equiv\ \mathid{f}~\mathid{x}~\\ \mathkw{bind}(\mathid{f},~\mathkw{unit}~\mathid{x})~&~\equiv\ \mathid{f}~\mathid{x}\\ \mathkw{map}(\mathkw{unit}~\mathid{x},~\mathid{f}~)~&~\equiv\ \mathkw{unit}~(\mathid{f}~\mathid{x}) \end{mdmathpre}%mdk \]

4.2. The Monomorphism Restriction

The Monomorphism Restriction restricts value definitions to be effect monomorphic. Consider the following program

function poly(x : a, g : (a) e b) : e b
val mr = if (expensive() 0) then poly else poly  

How often is expensive() executed? The user can naturally assume that the call is done once, at the initialization of mr. But, since mr is effect polymorphic (due to poly), our translation inserts a dictionary argument. Thus, the call is executed as many times as mr is referenced. To avoid this situation the Koka compiler rejects such value definitions, similar to the monomorphism restriction of Haskell. Aside from this restriction, our translation is complete, i.e., we accept and translate all programs that plain Koka accepts.

4.3. Evaluation

Finally, we give a quantitative evaluation of our approach that allows us to conclude that monadic user-defined effects can be used to produce high quality code without much affecting the compile- or running-time of your program.

static time file size
program compile trans. time trans. % lines
amb 107 ms 2.795 ms 2.60 % 67
parser  89 ms 2.582 ms 2.88 % 72
async 117 ms 3.155 ms 2.67 % 166
behamb 276 ms 3.009 ms 1.09 % 101
core 6057 ms 16.424 ms 0.27 % 2465

Figure 10. Quantitative evaluation of static time for user-defined effects.

In Figure 10 we present the static metrics and the file size of our five benchmarks: (1) amb manipulates boolean formulas using the ambiguous effect, (2) parser parses words and integers from an input file using the parser effect, (3) async interactively processes user's input using the asynchronous effect, and (4) behamb combines the ambiguous and the behavior effects (5) core is Koka's core library that we translate so that all library's functions can be used in effectful code. On these benchmarks we count the file size in lines, the total compilation time, the translation time and we compute the percentage of the compilation time that is spent on translation. The results are collected on an Intel Core i5 machine.

Static Time. As Figure 10 suggests the compile-time spend in translation is low (less that 3% of compilation time). More importantly, the fraction of the time spend in translation is minor in code that does not use monadic effects, mostly due to our optimizations (§ 4.1).

Run Time. To check the impact of our translation on run-time we created “monadic” versions of our examples, i.e. a version of the amb that uses lists instead of the amb effect and a version of the parser that uses a parser data type. We observed that our monadic translation does not have any run-time cost mostly because it optimizes away redundant calls (§ 4.1).

We conclude that our proposed abstraction provides quality code with no run-time and low static-time overhead.

Many effect typing disciplines have been proposed that study how to delimit the scope of effects. Early work is by Gifford and Lucassen [11, 22] which was later extended by Talpin [33] and others [25, 32]. These systems are closely related since they describe polymorphic effect systems and use type constraints to give principal types. The system described by Nielson et al. [25] also requires the effects to form a complete lattice with meets and joins. Wadler and Thiemann [36] show the close connection between monads [24, 35] and the effect typing disciplines.

Java contains a simple effect system where each method is labeled with the exceptions it might raise [13]. A system for finding uncaught exceptions was developed for ML by Pessaux et al. [26]. A more powerful system for tracking effects was developed by Benton [4] who also studies the semantics of such effect systems [5]. Recent work on effects in Scala [30] shows how restricted polymorphic effect types can be used to track effects for many programs in practice.

Marino et al. created a generic type-and-effect system [23]. This system uses privilege checking to describe analytical effect systems. Their system is very general and can express many properties but has no semantics on its own. Banados et al. [1] layer a gradual type system on top this framework. This may prove useful for annotating existing code bases where a fully static type system may prove too conservative.

Our current work relies heavily on a type directed monadic translation. This was also described in the context of ML by Swamy et al. [31], where we also showed how to combine multiple monads using monad morphisms. However, Koka uses row-polymorphism to do the typing, while [31] uses subtyping. A problem with subtyping is that the inferred types can be too complicated to understand. For example, in an η-robust version, the type inferred for function composition in [31] is:

\[\begin{mdmathpre}%mdk \forall \mathid{a}~\mathid{b}~\mathid{c}~\mu_1~\mu_2~\mu_3~\mu_4~\mu.~(\mu_1~{\ge}~\mu_,\mu_2~{\ge}~\mu_)~\Rightarrow\\ \mdmathindent{3}(\mathid{b}~{\rightarrow}~\mu_2~\mathid{c})~{\rightarrow}~\mu_3~(\mathid{a}~{\rightarrow}~\mu_1~\mathid{b})~{\rightarrow}~\mu_4~(\mathid{a}~{\rightarrow}~\mu{}~\mathid{c}) \end{mdmathpre}%mdk \]

which is much harder to read than the type inferred in Koka:

\[\begin{mdmathpre}%mdk \forall{\langle}\mathid{a},\mathid{b},\mathid{c},\e{\rangle}~(\mathid{b}~{\rightarrow}~{\e}~\mathid{c},~\mathid{a}~{\rightarrow}~{\e}~\mathid{b})~{\rightarrow}~{\e}~\mathid{c} \end{mdmathpre}%mdk \]

where no constraints are present.

A similar approach to [31] is used by Rompf et al. [29] to implement first-class delimited continuations in Scala which is essentially done by giving a monadic translation. Similar to our approach, this is also a selective transformation; i.e. only functions that need it get the monadic translation. Both of the previous works are a typed approach where the monad is apparent in the type. Early work by Filinksi [8, 9] showed how one can embed any monad in any strict language that has mutable state in combination with first-class continuations (i.e. callcc). This work is untyped in the sense that the monad or effect is not apparent in the type. In a later work Filinksi [10] proposes a typed calculus where monads are used to give semantics to effects. This proposal has many similarities with our current work, but does not explore effect inference and polymorphism, which both are features crucial for a usable effect system.

Algebraic effect handlers described by Plotkin et al. [27] are not based on monads, but on an algebraic interpretation of effects. Even though monads are more general, algebraic effects are still interesting as they compose more easily. Bauer and Pretnar describe a practical programming model with algebraic effects [2] and a type checking system [3]. Even though this approach is quite different than the monadic approach that we take, the end result is quite similar. In particular, the idea of handlers to discharge effects, appears in our work in the form of the from primitives induced by an effect declaration.

6. Conclusion

Using the correspondence between monads and effects [36], we have shown how you can define the semantics of an effect in terms of a first-class monadic value, but you can use the monad using a first-class effect type. We provide a prototype implementation that builds on top of Koka's type- and effect inference system.

In “The essence of functional programming” [35], Wadler remarks that “by examining where monads are used in the types of programs, one determines in effect where impure features are used. In this sense, the use of monads is similar to the use of effect systems”. We take the opposite view: by examining the effect types one can determine where monads are to be used. In Wadler's sense of the word, the essence of effectful programming is monads.

References

[1]Felipe Bañados Schwerter, Ronald Garcia, and Éric Tanter. “A Theory of Gradual Effect Systems.” In ICFP. 2014. doi:10.1145/2628136.2628149🔎
[2]Andrej Bauer, and Matija Pretnar. “Programming with Algebraic Effects and Handlers.” CoRR 1203.1539. 2012. arXiv:1203.1539🔎
[3]Andrej Bauer, and Matija Pretnar. “An Effect System for Algebraic Effects and Handlers.” Logical Methods in Computer Science 10 (4). 2014. doi:10.2168/LMCS-10(4:9)2014🔎
[4]Nick Benton, and Peter Buchlovsky. “Semantics of an Effect Analysis for Exceptions.” In TLDI. 2007. doi:10.1145/1190315.1190320🔎
[5]Nick Benton, Andrew Kennedy, Lennart Beringer, and Martin Hofmann. “Relational Semantics for Effect-Based Program Transformations with Dynamic Allocation.” In PPDP. 2007. doi:10.1145/1273920.1273932🔎
[6]Olivier Danvy, Kevin Millikin, and Lasse R. Nielsen. “On One-Pass CPS Transformations.” J. Funct. Program. 17 (6): 793–812. Nov. 2007. doi:10.1017/S0956796807006387🔎
[7]Conal Elliott, and Paul Hudak. “Functional Reactive Animation.” In International Conference on Functional Programming. 1997. http://​conal.​net/​papers/​icfp97/​🔎
[8]Andrzej Filinski. “Representing Monads.” In POPL. 1994. 🔎
[9]Andrzej Filinski. Controlling Effects. U.S. Dept. of Labor, OSHA. 1996. 🔎
[10]Andrzej Filinski. “Monads in Action.” In POPL. 2010. doi:10.1145/1707801.1706354🔎
[11]David K. Gifford, and John M. Lucassen. “Integrating Functional and Imperative Programming.” In LFP. 1986. doi:10.1145/319838.319848🔎
[12]Jean-Yves Girard. “The System F of Variable Types, Fifteen Years Later.” TCS. 1986. doi:10.1016/0304-3975(86)90044-7🔎
[13]James Gosling, Bill Joy, and Guy Steele. The Java Language Specification. 1996. 🔎
[14]Michael Hicks, Gavin Bierman, Nataliya Guts, Daan Leijen, and Nikhil Swamy. “Polymonadic Programming.” In MSFP. 2014. 🔎
[15]Graham Hutton, and Erik Meijer. Monadic Parser Combinators. NOTTCS-TR-96-4. Dept. of Computer Science, University of Nottingham. 1996. 🔎
[16]Kennedy Kambona, Elisa Gonzalez Boix, and Wolfgang De Meuter. “An Evaluation of Reactive Programming and Promises for Structuring Collaborative Web Applications.” In DYLA. 2013. doi:10.1145/2489798.2489802🔎
[17]Oleg Kiselyov, and Chung-chieh Shan. “Embedded Probabilistic Programming.” In Domain-Specific Languages. 2009. doi:10.1007/978-3-642-03034-5_17🔎
[18]John Launchbury, and Amr Sabry. “Monadic State: Axiomatization and Type Safety.” In ICFP. 1997. doi:10.1145/258948.258970🔎
[19]Daan Leijen. Koka: Programming with Row-Polymorphic Effect Types. MSR-TR-2013-79. Microsoft Research. 2013. 🔎
[20]Daan Leijen. “Koka: Programming with Row Polymorphic Effect Types.” In MSFP. 2014. doi:10.4204/EPTCS.153.8🔎
[21]Daan Leijen, and Erik Meijer. Parsec: Direct Style Monadic Parser Combinators for the Real World. UU-CS-2001-27. Universiteit Utrecht. 2001. http://​www.​haskell.​org/​haskellwiki/​Parsec🔎
[22]J. M. Lucassen, and D. K. Gifford. “Polymorphic Effect Systems.” In POPL. 1988. doi:10.1145/73560.73564🔎
[23]Daniel Marino, and Todd Millstein. “A Generic Type-and-Effect System.” In TLDI. 2009. doi:10.1145/1481861.1481868🔎
[24]Eugenio Moggi. “Notions of Computation and Monads.” Inf. Comput. 1991. doi:10.1016/0890-5401(91)90052-4🔎
[25]Hanne Riis Nielson, Flemming Nielson, and Torben Amtoft. “Polymorphic Subtyping for Effect Analysis: The Static Semantics.” In LOMAPS. 1997. doi:10.1007/3-540-62503-8_8🔎
[26]François Pessaux, and Xavier Leroy. “Type-Based Analysis of Uncaught Exceptions.” In POPL. 1999. doi:10.1145/292540.292565🔎
[27]Gordon D. Plotkin, and Matija Pretnar. “Handlers of Algebraic Effects.” In ESOP, 5502:80–94. LNCS. Springer. 2009. doi:10.1007/978-3-642-00590-9_7🔎
[28]John C. Reynolds. “Towards a Theory of Type Structure.” In Programming Symposium. 1974. 🔎
[29]Tiark Rompf, Ingo Maier, and Martin Odersky. “Implementing First-Class Polymorphic Delimited Continuations by a Type-Directed Selective CPS-Transform.” In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming, 317–328. ICFP ’09. 2009. doi:10.1145/1596550.1596596🔎
[30]Lukas Rytz, Martin Odersky, and Philipp Haller. “Lightweight Polymorphic Effects.” In ECOOP. 2012. doi:10.1007/978-3-642-31057-7_13🔎
[31]Nikhil Swamy, Nataliya Guts, Daan Leijen, and Michael Hicks. “Lightweight Monadic Programming in ML.” In ICFP. 2011. doi:10.1145/2034773.2034778🔎
[32]Jean-Pierre Talpin, and Pierre Jouvelot. “The Type and Effect Discipline.” Inf. Comput. 1994. doi:10.1006/inco.1994.1046🔎
[33]J.P. Talpin. “Theoretical and Practical Aspects of Type and Effect Inference.” Phdthesis, Ecole des Mines de Paris and University Paris VI, Paris, France. 1993. 🔎
[34]Stefan Tilkov, and Steve Vinoski. “NodeJS: Using JavaScript to Build High-Performance Network Programs.” IEEE Internet Computing. 2010. 🔎
[35]Philip Wadler. “The Essence of Functional Programming.” In . POPL. 1992. doi:10.1145/143165.143169🔎
[36]Philip Wadler, and Peter Thiemann. “The Marriage of Effects and Monads.” TOLC. 2003. doi:10.1145/601775.601776🔎

A. Proof of soundness

We prove a generalization of the Type Preservation Theorem 2 in the paper where the computed effect is $\mathpre{\ue }$ not restricted to $\mathpre{\empeffect}$. Then our main theorem follows trivially.

Definition 1.
Since $\mathpre{\tmonad{{\langle}\mathid{l}_1^\ue|~...|~\mathid{l}_\mathid{n}^\ue|\empeffect{\rangle}}{\e}{\tau}~=~\mathid{M}_{\{\mathid{l}_1^\ue,~...,~\mathid{l}_\mathid{n}^\ue\}}{\langle}\e,~\tau{\rangle}}$, we can rewrite dictionary and morphism types using $\mathpre{\tmonad{\cdot}{\cdot}{\cdot}}$, as:

\[\begin{mdmathpre}%mdk \mathkw{struct}~\mathid{tdict}{\langle}{}\mathid{m}{\rangle}~\{\\ \mdmathindent{2}\mathid{unit}~:~\forall\alpha\mu.~\alpha {\rightarrow}~\tononuser{\mu}\ \tmonad{\mathid{m}}{\mu}{\alpha}\\ \mdmathindent{2}\mathid{map}~~:~\forall\alpha\beta\mu.~(\tmonad{\mathid{m}}{\mu}{\alpha},~\alpha {\rightarrow}~\beta)~{\rightarrow}~\tononuser{\mu}\ \tmonad{\mathid{m}}{\mu}{\beta}~\\ \mdmathindent{2}\mathid{bind}~:~\forall\alpha\beta\mu.~(\tmonad{\mathid{m}}{\mu}{\alpha},~\alpha {\rightarrow}~\tononuser{\mu}\ \tmonad{\mathid{m}}{\mu}{\beta}~)~{\rightarrow}~\tononuser{\mu}\ \tmonad{\mathid{m}}{\mu}{\beta}~\\ \} \end{mdmathpre}%mdk \]
\[\begin{mdmathpre}%mdk \xmorph{\ue_\mathid{s}}{\ue_\mathid{t}}~::~\mathid{forall}~\a\ \e.~\tmonad{\ue_\mathid{s}}{\e}{\a}~{\rightarrow}~\e\ \tmonad{\ue_\mathid{t}}{\e}{\a} \end{mdmathpre}%mdk \]

Theorem 1.
(Lifting) If  $\mathpre{{\vdash}~\mathid{e}~:~\tmonad{\ue_\mathid{s}}{\e}{\sigma}}$, then  $\mathpre{{\vdash}~\xlift{\ue_\mathid{s}}{\ue_\mathid{t}}{\mathid{e}}{\e}~:~\tmonad{\ue_\mathid{t}}{\e}{\sigma}}$.

Proof. Let $\mathpre{\mathid{e}'~\equiv \xlift{\ue_\mathid{s}}{\ue_\mathid{t}}{\mathid{e}}{\e}}$

Theorem 2.
(Binding) If  $\mathpre{{\vdash}~\mathid{e}_1~:~\tmonad{\ue_1}{\e}{\sigma_1}}$ and    $\mathpre{{\vdash}~\mathid{e}_2~:~\tmonad{\ue_2}{\e}{\sigma_2}}$, then  $\mathpre{{\vdash}~\xbind{\ue_1}{\ue_2}{\mathid{x}}{\mathid{e}_{1}}{\mathid{e}_{2}}{\e}~:~\tmonad{\ue_1\oplus\ue_2}{\e}{\sigma_2}}$.

Proof. Let $\mathpre{\mathid{e}'~\equiv \xbind{\ue_1}{\ue_2}{\mathid{x}}{\mathid{e}_{1}}{\mathid{e}_{2}}{\e}}$

Theorem 3.
(General Type Preservation)
If  $\mathpre{{\vdash}~\mathid{e}~:~\sigma}$ and $\mathpre{\mathid{e}~\mathop{\leadsto}_\e \mathid{e}'~|~\ue}$, then $\mathpre{{\vdash}~\mathid{e}'~:~\tmonad{\ue}{\e}{\llbracket\sigma\rrbracket}}$.

Proof. By induction of the structure of the derivations, and checking at each rule that the results are well-typed..

Lemma 2.
$\mathpre{\ttr{\s [\a \mapsto \s_\mathid{x}]}~=~\ttr{\s}~[\a \mapsto \ttr{\s_\mathid{x}}]}$.

Proof. By induction on the structure of the type scheme $\mathpre{\s}$.

B. The Asynchronous effect

As another example, we present how user-defined effects can be used to simplify asynchronous programming. Asynchronous code can have big performance benefits but it notoriously cumbersome to program with since one has to specify the continuation (and failure continuation). This style of programming is quite widely used in the JavaScript community for XHR calls on the web, or when programming NodeJS [34] servers. Consider the following asynchronous JavaScript code that uses promises [16]. This example is somewhat simple but also in many ways typical for asynchronous code:

function main() {
 game().then(null, function(err) {
  println("an error happened");
 });
}
function game() {
 return new Promise().then( function() {
  println("what is your name");
  readline().then( function(name) {
   println("Ah, And who is your mentor?");
   readline().then( function(mentor) {
    println("Thinking...");
    wait(1000).then( function() {
     println("Hi " + name + ". Your mentor is " + mentor);
 });});});});
};

The asynchronous functions here are readline and wait. Both return immediately a so-called Promise object, on which we call the then method to supply its success continuation: a function that takes as argument the result of readline and uses it at its body. Finally, then takes a second (optional) argument as the failure continuation. If a failure occurs within a continuation with no failure continuation, execution skips forward to the next then. In this example if any error occurs, it will be forwarded to the main function which will die by printing "an error occured".

Programming with callbacks in tricky. Common errors include doing computations outside the continuation, forgetting to supply an error continuation, using try-catch naively (which don't work across continuations), and mistakes with deeply nested continuations (e.g. the pyramid of doom).

Asynchronicity as an effect.

In Koka, we can actually define an async effect that allows us to write asynchronous code in a more synchronous style while hiding all the necessary plumbing. that behave asynchronous, i.e., have exactly the same behaviour as the previous example. We define the asynchronous effect as a function with two arguments, the success and the failure continuation:

effect asynce,a = (a e (), exception e ()) e () {
 function unit(x) {
  return fun(c,ec) { c(x) }
 }
 function bind(m,f) {
  return fun(c,ec) {
   m( fun(x) {
    val g = catch( { f(x) }, fun(exn) { return fun(_,_) { ec(exn) } } )
    g(c,ec)
   }, ec )
  }
 }
 function bind_catch(m,h) {
  return fun(c,ec) {
   catch({
    m(c, fun(err) { h(err)(c,ec) })
   }, fun(err) { h(err)(c,ec) })
  }
 }
}

This one is quite complex but that is somewhat expected of course – getting asynchronicity right is complicated. As usual, Koka automatically creates the primitives to_async and from_async. We use these to define other functions: run(action) turns the async computation action into an io computation. readline is an async wrapper for the primitive readln function that is explicitly called with its success continuation.

function readline() : async,console string {
 to_async fun(cont,_econt) { readln(cont) }
}

Finally, using these two primitives and the async effect we can now program nice and “vertical”, synchronous-like code for our initial JavaScript example:

function main() {
 run(game)
}
function game() : async,io () {
 println("what is your name?")
 val name = readline()
 println("Ah. And who is your mentor?")
 val mentor = readline()
 println("Thinking...")
 wait(1000)
 println("Hi " + name + ". Your mentor is " + mentor)
}

Moreover, just like other effects, we can use any abstraction as usual, like mapping asynchronous computation over lists etc. Of course, we need more primitives, like fork which starts multiple asynchronous computations in parallel and finished when all are done.

The strong typing is crucial here as it provides good indication that the code is potentially asynchronous! It is generally recognized that knowing about asynchronicity is important, but other effects like exceptions, divergence, or heap mutation, are not always treated with the same care. In Koka, all effects are considered essential to the type of a function and asynchronicity is treated in the same way as any other effect.

Semantically, the asynchronous effect is not quite like our earlier examples which could be implemented in Koka as is. For example, note the invocation of catch in the definition of bind. Why is that necessary? and what happens if we would forget it? The reason behind this is that asynchronicity cannot exist within the basic semantics of Koka (as described in [20]). In particular, we introduce new constants supplied by the runtime environment that behave outside of Koka semantics, like readln. Effectively, every time an asynchronous operation is executed, the program terminates and is revived again when the continuation is executed. This is also why run cannot be implemented in Koka itself but needs special runtime support too – it effectively needs to ‘wait’ until all asynchronous operations are done and then return its result (or throw an exception). Of course, since Koka is implemented on top of JavaScript all these primitives (and many more) are provided the host runtime systems (i.e. NodeJS and browsers).

C. Download

The current prototype of the work in this article is freely available online. It is not yet ready for prime-time since some checks are lacking, but by the time of the conference we hope to have it online on http://​www.​rise4fun.​com/​koka. Currently, one can build the development branch though and play with the examples in this paper:

The basic Koka compiler compiles to JavaScript and is quite mature at this point. In fact, Koka was used to create a sophisticated online markdown processor called Madoko, which was used to completely write this article! Try it at http://​www.​madoko.​net.

Created with Madoko.net.

1.In contrast to Haskell for example, where $\mathpre{\mathid{Int}}$ really stands for $\mathpre{\mathid{Int}_\bot}$, i.e. referring to a value of such type may still diverge or raise an exception.