1ML with Special Effects

Abstract

We take another look at 1ML, a language in the ML tradition, but with core and modules merged into one unified language, rendering all modules first-class values. 1ML already comes with a simple form of effect system that distinguishes pure from impure computations. Now we enrich it with effect polymorphism: by introducing effect declarations and, more interestingly, abstract effect specifications, effects can be parameterised over, and treated as abstract or concrete in the type system, very much like types themselves. Because type generativity in 1ML is controlled by (im)purity effects, this yields a somewhat exotic novel notion of generativity polymorphism – that is, a given functor can be asked to behave as either “generative” or “applicative”. And this time, we even get to define an interesting (poly)monad for that!

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

In a recent paper [13] we introduced 1ML, a reboot of ML where modules are first-class values. In this language, there no longer is any distinction between core and modules, records or structures, functions or functors. Morally, every expression denotes a module.

One peculiar feature of 1ML is its distinction between pure and impure functions and computations, through a – very simple – form of effect system. Although this is primarily motivated by the semantics of functors (as we will see below), it obviously is an interesting distinction to make for “core-like” functions as well. Effect systems [3, 9, 18] are regularly proposed as a complement to functional type systems. They serve a similar role as monads [12, 20], which have been successfully incorporated into languages like Haskell, but with a little extra flexibility – Wadler & Thiemann showed that both are essentially equivalent [21].

Telling pure from impure statically allows much better control over side effects. Like any other form of type discipline, it allows more accurate specification of interfaces, and prevents certain classes of errors. For example, a module can specify that some of its interface functions are free of side effects. Or not. Higher-order functions can shield against unwanted side effects when invoking an argument function (or “callback”, as laymen say nowadays). All useful capabilities, and in principle it is possible to put them to good use in 1ML already.

What makes the use of effects cumbersome in 1ML, however, is the lack of support for effect polymorphism. In a higher-order language that is a real bummer, because the purity of a higher-order function will typically depend on the purity of its argument. For example, consider

Is this a pure or impure function? It depends on $\textsf {f}$. We can imagine (at least) two different signatures for $\textsf {map}$:

Here, we use “$\rightarrow _{\textsf {P}}$” to denote pure function types, and “$\rightarrow _{\textsf {I}}$” for impure ones. Unfortunately however, $\textsf {map}$ may only have one of these types in 1ML. If we needed both, we would need to write different functions for the different signatures. (Notably, 1ML’s pure arrows are subtypes of impure ones, but such subtype polymorphism is insufficient to handle this case.)

Or we introduce the ability to abstract over (im)purity via polymorphism. Both $\textsf {map}$ and its argument could be polymorphic in their (joint) effect:

In this signature, we assume that $\textsf {e}$ is a (universally quantified) effect variable. By instantiating it with either $\textsf {P}$ or $\textsf {I}$, we can use the same implementation of $\textsf {map}$ on either a pure or an impure argument, and get a corresponding pure or impure computation in return.

Okay, you might think, that looks like a fairly trivial and standard extension. Others proposed this long ago [9]. Well, what makes it interesting in 1ML is that the (im)purity effect is intimately tied to the notion of type generativity.

Functions that return abstract types – “functors” in ML speak – are interesting beasts. There are two traditional schools of semantics: “generative” functors (the SML way) and “applicative” functors (the OCaml way). In 1ML, both notions coexist, and depend on whether a functor is pure or impure. Consider:

A pure functor like this is “applicative” [8, 15], meaning that all applications to equivalent types yield equivalent types:

defines types $\textsf {t}$ and $\textsf {u}$ to be equivalent. (Regardless, they are still abstract!)

An impure functor is “generative”, however:

generates a fresh type with every application. So,

are different types! This is important in the face of impurity, since the types produced by an impure computation may e.g. depend on state, and thus equating them would be plain unsound. (More reasons why you all want both applicative and generative functors are disclosed in Sects. 7 and 8 of [15].)

Now, what would happen if we allowed such a functor to be polymorphic over its effect? Say,

Depending on the choice of $\textsf {e}$, it would be either applicative or generative: that is, $\textsf {H\;bool\;P}$ = $\textsf {H\;bool\;P}$, while $\textsf {H\;bool\;I}$ is not reflexive (or even a well-formed type expression).

In other words, introducing polymorphism over effects implies a notion of generativity polymorphism. Is that actually a thing?

It is! In this paper, we show that this – rather esoteric – notion can actually be defined. And we don’t even have to leave the familiar grounds of System F$_\omega$ for that. Well, except for one small extension. We also show that generativity polymorphism is the essence of MacQueen & Tofte & Kuan’s (arguably equally esoteric) notion of “true” higher-order functors [6, 7, 10].

2 The Language

Figure 1 presents the syntax of 1ML extended with explicit effects, separated into core syntax and various syntactic sugar. For space reasons, we focus on the explicitly typed fragment 1ML$_{\mathop {\mathrm {ex}}\nolimits }$ [13] here (though complementing this with effect inference in full 1ML is an easy addition). The effect-related constructs that are new relative to the original formulation of 1ML$_{\mathop {\mathrm {ex}}\nolimits }$ are in the figure.

As in the original paper, the syntax is normalised to require named subterms in most constructs. The general forms, as well as many other familiar module or core-level constructs, can easily be defined as syntactic sugar. See [13] for enough sugar to upset your stomach.

Fig. 1.

Syntax of 1ML$_{\mathop {\mathrm {ex}}\nolimits }$ with effect polymorphism (see [13] for more abbreviations)

2.1 Basic Use of Effects

The extended language incorporates three main additions.

Effect Annotations. First, function types acquire an explicit annotation F, that specifies the effect that is released when calling the function. Because real programming language syntax better works as plain text, we use the notation “$F\textsf {/}T$” instead of making F a subscript on the arrow, as we did in the introduction.

There are two basic effect constants: ${{\mathbf {\mathsf{{pure}}}}}$ and ${{\mathbf {\mathsf{{impure}}}}}$. To ease notation in the common cases, we allow abbreviating pure function types with a plain arrow “$\rightarrow$”, and impure ones with a squiggly arrow “$\leadsto$”.¹

For example, the type of the polymorphic identity function,

can be denoted as

or shorter, as just

Similarly, we can add impure operators to the language; for example, an ML-style type $\textsf {ref}\;T$ of mutable references with operators

Note how these types mix pure and impure arrows. A type parameter – expressing (explicit) polymorphism – is best considered a pure function: “instantiating” a polymorphic type should not have any effect. Similarly, an impure function with curried value parameters (like $\textsf {wr}$) releases its effect only when the last argument is provided.

Effect Values. Second, what makes the new syntax for function types interesting instead of just verbose is that effects can now be “computed”: F can not just refer to the two effect constants, it can also consist of an expression E. This has to be a (pure) expression of the new type ${{\mathbf {\mathsf{{effect}}}}}$, a type that is inhabited by effect “values”. Those values are formed by the corresponding expression ${{\mathbf {\mathsf{{effect}}}}}\,F$. Just like types in 1ML, effects can thus be named or passed around as if they were first-class values.

For example, we can write an effect-polymorphic $\textsf {apply}$ combinator:

The type of this function is:

To apply it, we have to provide the right effect argument:

Similarly, the $\textsf {map}$ function from the introduction can be given the (explicitly) polymorphic type

Like any other value, effects can also be named by a binding:

Analogous to type bindings in 1ML, this effect binding is just sugar for the value binding “e = (${{\mathbf {\mathsf{{effect}}}}}$ pure)”. Admittedly, such bindings are a bit boring with just effect constants, but they become more interesting with the following feature.

Effect Composition. Finally, how are we going to type the following function?

To give a type to that, we need the ability to compose effects. That is the role of the effect operator “$\textsf {,}$”:

“$F_1\textsf {,}F_2$” denotes the least upper bound of effects $F_1$ and $F_2$ in a lattice where ${{\mathbf {\mathsf{{pure}}}}}$ is the bottom element and ${{\mathbf {\mathsf{{impure}}}}}$ is top (the direction of this lattice is consistent with the natural notion of subtyping on effects, where $\textsf {pure} \le \textsf {impure}$; see Sect. 3). Consequently, an invocation of $\textsf {compose}$ will be impure if at least one of the effect parameters is instantiated with $\textsf {impure}$; only if both are pure the result is pure as well. That should come as no surprise.

2.2 Generativity Polymorphism

So far, we have only looked at effects of simple functions. If you are already familiar with effect polymorphism, and much of the above looked boring, then you can wake up now – we are now turning to modules and functors.

First-Order Generativity Polymorphism. Let us start with the simplest possible functor – essentially, the identity type constructor:

The most specific type derivable for $\textsf {Id}$ in 1ML is the fully transparent type

where the singleton type $\textsf {(= a)}$ indicates that the function returns the argument $\textsf {a}$ itself. This transparent signature is a subtype of two possible opaque signatures that do not reveal the identity of their resulting type:

We can seal $\textsf {Id}$ with either of these signatures:

Both these functors now return an abstract type, but the first is “applicative”, i.e., always returns the same type for equivalent arguments, while the second is “generative”, i.e., always returns a fresh type, regardless of the argument.

But in our extended 1ML, there now is a third choice:

We have just created our first “poly-generative” functor! This one can be applied to our choice of effect: for example, $\textsf {Id\_poly\,pure\,bool} = \textsf {Id\_poly\,pure\,bool}$ are equivalent types, while $\textsf {Id\_poly\,impure\,bool}$ is a generative (and thus impure) expression that cannot be used as a type without binding it to a name. This is exactly the functor $\textsf {H}$ we wondered about in the introduction.

Higher-Order Generativity Polymorphism. Okay, that was a contrived example. Generativity polymorphism becomes more relevant in the higher-order case. Because we can now write the kind of functors that MacQueen always wanted to write, under his slogan of “true higher-order functors” [6, 7, 10]. Recast in 1ML, the problem he is concerned with, as formulated by Kuan & MacQueen [7], boils down to the ability to define a generic $\textsf {Apply}$ functor over types:

Kuan & MacQueen want to be able to use such a functor transparently (i.e., such that type identities are fully propagated) in both of the following cases:

As it turns out, these examples already type-check in plain 1ML: both applications are well-typed, provided one picks $\textsf {e}$ $=$ $\textsf {pure}$ in the parameter type of $\textsf {F}$ when defining $\textsf {Apply}$ (which is equivalent to a plain 1ML pure function type). In fact, even the application to an abstract functor works, as long as that is pure as well:

However, Kuan & MacQueen didn’t deal with a language of (only) applicative functors (and neither do we), so the above isn’t quite a fair answer to their challenge. What they really meant in particular is that $\textsf {Apply}$ should also be applicable to a generative functor, like here:

That also works in plain 1ML, but only if the parameter $\textsf {F}$ is typed as an impure functor in the definition of $\textsf {Apply}$, equivalent to picking $\textsf {e}$ $=$ $\textsf {impure}$ in our extended language. That is, in plain 1ML, we can write $\textsf {Apply}$ such that either the former three examples type-check, or the last, but not all at the same time.

Effect polymorphism to the rescue! You already guessed it: in extended 1ML we can escape that dilemma by making $\textsf {e}$ into a parameter itself:

Now all examples are expressible:

The extra argument is a bit more tedious to write than Kuan & MacQueen would want, but it could easily be inferred (though we don’t discuss that here).

Existential Effect Polymorphism. Just for completeness, we mention that effects can also – like types – be sealed, introducing the notion of an “abstract effect”:

Honestly, this does not look like it would be a particularly useful feature, but it falls out from 1ML’s design naturally and for free. Ruling it out would be more complicated than allowing it. Maybe there even is some crazy use case that we don’t foresee yet... Phantom effects, anyone?

3 Type System

Here’s how we build a type system for 1ML$_{\mathop {\mathrm {ex}}\nolimits }$ with generativity polymorphism. (Unfortunately, for the lack of space, we have to focus on the novelties, and refer the interested reader to [13] for many basic details and rules omitted here.)

Semantic Types. Following the F-ing modules approach [15], 1ML’s type system [13] is not defined in terms of its own syntactic types. Instead, it is defined by translating those types into semantic types. (The short story behind that approach is that syntactic module types are not expressive enough to accurately account for all details of type abstraction and functorisation, especially the problem of local types, a.k.a. the avoidance problem. See [15] for the long story.)

Fig. 2.

Semantic types

Figure 2 shows the grammar of semantic types needed for 1ML$_{\mathop {\mathrm {ex}}\nolimits }$ with effect polymorphism (plus some auxiliary notation we’ll get to). They are written in the style of System F types with explicit quantifiers (and as we will see later they actually are System F types). Once more, additions to the original 1ML system are . Type variables can be higher-order in these types, but we assume they are kinded implicitly, and we use the notation $\kappa _\alpha$ if we need to talk about the kind of $\alpha$.

Let us recap the main intuitions behind those F-ing module types. The central idea is introducing explicit quantifiers to remove all dependencies within a type.

Following Mitchell & Plotkin [11], signature types containing abstract types (i.e., ADTs) are represented as existential types. For example, the signature

where components $\textsf {v}$ and $\textsf {f}$ depend on $\textsf {t}$ and $\textsf {u}$, corresponds to the semantic type

$$\begin{aligned} \exists \alpha _1 \alpha _2. \{ {\mathrel {\mathsf {t}}} : [= \alpha _1], {\mathrel {\mathsf {u}}} : [= \alpha _2], {\mathrel {\mathsf {v}}} : [= \alpha _1 \rightarrow \alpha _1], {\mathrel {\mathsf {f}}} : \alpha _1 \rightarrow \alpha _2 \} \end{aligned}$$

where $\alpha _1$ and $\alpha _2$ are the local names for type components $\textsf {t}$ and $\textsf {u}$, respectively, and there are no dependencies inside the record. The notation $[= \tau ]$ denotes the type of $\tau$ reified “as a value”, i.e., represents the type ${{\mathbf {\mathsf{{type}}}}}$ (recall that a component specification “type t” is just short for “t: type” in 1ML).

Functors, on the other hand, correspond to universal types. Any abstract type from their domain signature becomes a universal type variable with scope widened to include the codomain. For example, the functor type

with dependencies from its codomain on the type $\textsf {X.t}$ from the domain, maps to

$$\begin{aligned} \forall \alpha . \{{\mathrel {\mathsf {t}}} : [= \alpha ], {\mathrel {\mathsf {v}}} : \alpha \} \rightarrow _{\mathop {\mathrm {\texttt {P}}}\nolimits }\{{\mathrel {\mathsf {u}}} : [= \alpha \rightarrow \alpha ], {\mathrel {\mathsf {x}}} : \alpha \} \end{aligned}$$

More interesting are cases where an abstract type is bound in the codomain:

If $\textsf {e}$ is $\textsf {impure}$, then this is a generative functor, which is modeled in the semantic types by returning an existential package:

$$\begin{aligned} \forall \alpha . \{{\mathrel {\mathsf {t}}} : [= \alpha ], {\mathrel {\mathsf {v}}} : \alpha \} \rightarrow _{\mathop {\mathrm {\texttt {I}}}\nolimits }\exists \beta . \{{\mathrel {\mathsf {u}}} : [= \beta ], {\mathrel {\mathsf {f}}} : \alpha \rightarrow \beta \} \end{aligned}$$

If $\textsf {e}$ is $\textsf {pure}$, however, then the functor is supposed to behave applicatively, i.e., return the same abstract type on each application. That is modeled by lifting the existential out of the function:

$$\begin{aligned} \exists \beta . \forall \alpha . \{{\mathrel {\mathsf {t}}} : [= \alpha ], {\mathrel {\mathsf {v}}} : \alpha \} \rightarrow _{\mathop {\mathrm {\texttt {P}}}\nolimits }\{{\mathrel {\mathsf {u}}} : [= \beta \,\alpha ], {\mathrel {\mathsf {f}}} : \alpha \rightarrow \beta \,\alpha \} \end{aligned}$$

In fact, it as an invariant of our semantic types that a pure arrow never has an existential quantifier to the right – a pure functor cannot generate types. There is one subtlety involved with the above type, though: in the implementation of a functor matching this signature, the definition of $\textsf {u}$ may depend on the parameter type $\textsf {t}$. Following Biswas [1] and Russo [16], all uses of $\beta$ in the semantic interpretation are hence skolemised over $\alpha$ accordingly. Consequently, $\beta$ needs to have higher kind $\kappa _\beta = \varOmega \rightarrow \varOmega$ here (other variables had base kind $\varOmega$ so far).

As we can see, the structure of the semantic type modeling the functor type above is quite different depending on the choice of $\textsf {e}$. It differs in terms of where the quantifier goes (inside vs. outside), its variable kind ($\varOmega$ vs. $\varOmega \rightarrow \varOmega$), and how the abstract type $\textsf {u}$ is denoted ($\beta$ vs. $\beta \,\alpha$). How can we reconcile these structural differences to support a parametric choice of effect?

We can’t. Not really, anyway. We need something new.

The natural trick is to use sums: we generalise function types such that their codomain is a “computation” type $\varPhi$ that allows arbitrary many alternative results. That is, if $\textsf {e}$ is not statically known to be either $\textsf {pure}$ or $\textsf {impure}$, then the functor signature above will be represented as

$$\begin{aligned} \begin{array}{l} \exists \beta _1. \forall \alpha . \{{\mathrel {\mathsf {t}}} : [= \alpha ], {\mathrel {\mathsf {v}}} : \alpha \} \rightarrow _\eta \\ \qquad ( \{{\mathrel {\mathsf {u}}} : [= \beta _1\,\alpha ], {\mathrel {\mathsf {f}}} : \alpha \rightarrow \beta _1\,\alpha \} + \exists \beta _2. \{{\mathrel {\mathsf {u}}} : [= \beta _2], {\mathrel {\mathsf {f}}} : \alpha \rightarrow \beta _2\} )^\eta \end{array} \end{aligned}$$

This encodes both possibilities: the left side of the sum is for the pure choice, the right for the impure one. In this type, $\eta$ is the representation of the effect $\textsf {e}$ as a semantic type. If $\eta$ is not a constant ${\mathop {\mathrm {\texttt {P}}}\nolimits }$ or ${\mathop {\mathrm {\texttt {I}}}\nolimits }$, then it either is an effect variable $\iota$, or the least upper bound of several of those, represented by the “$\vee$” operator. Since the two effect constants are the top and bottom elements of the effect lattice, least upper bounds that contain those constants can always be simplified to either ones that don’t, or directly to ${\mathop {\mathrm {\texttt {I}}}\nolimits }$. We assume that this simplification is always performed implicitly, according to the notational rules given in Fig. 2.

The effect $\eta$ appears twice in the above type: once as an annotation on the arrow, and once as an index on the sum, which is written $(\varPhi _1 + \varPhi _2)^\eta$. The former occurrence tracks the effect of the function, in a generalisation of what we already had in plain 1ML. The latter tracks the choice of the sum: if, at some point, the free effect variables of $\eta$ get substituted such that the result normalises to an effect constant, then the choice is statically determined – this basically is a binary GADT. We say that a $\varPhi$ with all effect indices being constants is unique. As we will see below, this static extra knowledge is important for figuring out when an expression of type ${{\mathbf {\mathsf{{type}}}}}$ unambiguously denotes a type, such that it is legal to project it.

It may be surprising that we need $\eta$ twice. The reason is that, in general, the computation type $\varPhi$ in the codomain of an arrow can consist of many nested sums, indexed by different effects – e.g., when a functor itself invokes several other functors with variable effects. The effect on the arrow then only is an upper bound of all these individual indices (and not necessarily the least); for example, we could construct a functor of type $\varSigma \rightarrow _{\eta _1\vee \eta _2} ((\varXi _1 + \varXi _2)^{\eta _1} + \varXi _3)^{\eta _2}$. In a pure function, however, this upper bound is ${\mathop {\mathrm {\texttt {P}}}\nolimits }$, so all effect indices in $\varPhi$ must be pure as well, such that $\varPhi$ is already guaranteed to be unique.

Fig. 3.

Elaboration of types and effects (new and modified rules)

Types and Effects. The new and modified rules for translating syntactic types T into semantic types $\varXi$ are collected in Fig. 3 (please see [13] for the others). The individual modifications over plain 1ML are again .

The new rule $\textsc {Teffect}$ for the type ${{\mathbf {\mathsf{{effect}}}}}$ is analogous to the rule for ${{\mathbf {\mathsf{{type}}}}}$, in that it introduces a fresh type variable to name the abstract effect. We use $\iota$ to range over type variables that encode effects. We assume that these type variables are a subcategory of general type variables $\alpha$, such that they can be uniformly written as $\alpha$ wherever we don’t care about the distinction.

The rule $\textsc {Tfun}$ for function types effectively merges the previous rules $\textsc {Tfun}$ and $\textsc {Tpfun}$ from 1ML, covering both impure and pure functors, but also effect-polymorphic ones. It refers to the simple effect elaboration judgement also shown in the figure. The auxiliary operator “$\oplus$” (defined in Fig. 2) avoids the sum in those cases where the effect is statically known or does not change the type. Likewise, we write “$\exists \overline{\alpha }^{\iota \ne {\mathop {\mathrm {\texttt {I}}}\nolimits }}$” to say that a quantifier is to be empty if $\eta = {\mathop {\mathrm {\texttt {I}}}\nolimits }$.

Another change is in rules $\textsc {Tpath}$ and $\textsc {Tsing}$ (and inherited by $\textsc {Fpath}$): the notation $\varPhi !$ (also defined in Fig. 2) requires E’s type $\varPhi$ to be unique – it selects $\varPhi$’s unique summand and is undefined otherwise. It is here where we rely on the effect index on sums: only sums whose indices are constant are unique, and can be used for unambiguous projection of static information.

Fig. 4.

Elaboration of expressions (selected rules)

Expressions and Bindings. Figure 4 shows selected typing rules for expressions E and bindings B, novelties once more . Before we go into details, let us recap the main idea of typing modules using the F-ing modules approach.

As we saw before, the main trick in interpreting module types is introducing quantifiers for abstract types. That is reflected in the typing of expressions: an expression that defines new abstract types will have an “abstracted” type $\varXi$ with existential quantifiers, one quantifier for each new type.

When such an expression is nested into a larger expression then the rules have to propagate these quantifiers accordingly. For example, for a projection $E\textsf {.x}$ to be well-typed, E obviously needs to have a type of the form $\{{\mathrel {\mathsf {x}}} : \varSigma , \dots \}$; the resulting type would be $\varSigma$ then. However, if E creates abstract types locally, then its type will be of the form $\exists \overline{\alpha }. \{{\mathrel {\mathsf {x}}} : \varSigma , \dots \}$ instead. The central idea of F-ing modules is to handle such types implicitly by extruding the existential quantifier automatically: that is, the projection $E\textsf {.x}$ is well-typed and assigned type $\exists \overline{\alpha }. \varSigma$, with the same sequence of quantifiers. And so on for other constructs.

As we pointed out in [15], this handling of existential types is akin to a monad – the monad of type generation! More precisely, it is a stack of nested monads, one for each generated type. By extending 1ML with generativity polymorphism, however, there no longer necessarily is a unique quantifier sequence for a given expression. Expressions are now classified by “computation” types $\varPhi$, which are sums over heterogeneous existentials. Our monad just became more interesting!

Fortunately, the sums we are dealing with are not arbitrary. Ultimately, they all originate, directly or indirectly, from uses of the rule $\textsc {Tfun}$ introducing effect-polymorphic function types. And a quick look at this rule reveals that the inner structure of the type is the same in both cases, up to the presence of quantifiers and the internal naming of the abstract types introduced.

Fig. 5.

Polymonad notation for computation types

That allows to factor computation types $\varPhi$ such that we separate their inner structure from their quantification scheme. To that end, Fig. 5 defines an auxiliary syntactic class of monadic type constructors M. Any computation type $\varPhi$ can be expressed $\beta$-equivalently as an application of such an M to a suitable type constructor defining the inner structure of the result. For example, the effect-polymorphic functor type from earlier can be written equivalently as

$$\begin{aligned} \begin{array}{l} \exists \beta _1. \forall \alpha . \{{\mathrel {\mathsf {t}}} : [= \alpha ], {\mathrel {\mathsf {v}}} : \alpha \} \rightarrow _\eta ( \exists [\beta _1\,\alpha ] + \exists \beta _2 [\beta _2] )^\eta \, (\lambda \beta . \{{\mathrel {\mathsf {u}}} : [= \beta ], {\mathrel {\mathsf {f}}} : \alpha \rightarrow \beta \}) \end{array} \end{aligned}$$

That is, an application of $(M_1 + M_2)^\eta$ with $M_1 = \exists [\beta _1\,\alpha ]$ (which has an empty existential quantifier) and $M_2 = \exists \beta _2 [\beta _2]$ to the structural template $\lambda \beta . \{{\mathrel {\mathsf {u}}} : [=~\beta ], {\mathrel {\mathsf {f}}} : \alpha \rightarrow \beta \}$, with $\beta$ being mapped to either $\beta _1\,\alpha$ or $\beta _2$, accordingly.

The set of all monadic types M forms a polymonad [5] or productoid [19], with $\exists []$ as its identity element. We can define the composition $M_1 M_2$ as given in Fig. 5. We won’t go into details here, but leave proving the polymonad laws as an exercise (see also Sect. 4).

It suffices to observe that we can use this notation to uniformly access the structure of all alternatives of a computation type. Moreover, we can construct a new computation type that lives in the same monadic envelope M. In particular, this happens in rules $\textsc {Edot}$ and $\textsc {Bvar}$, which project and inject a value from/into a structure, respectively. The notation is put to more interesting use in rule $\textsc {Bseq}$, where two nested monadic computations in $M_1$ and $M_2$ are lifted to their composition $M_1 M_2$.

On the term level, the polymonad is witnessed by suitably defined ${\mathsf {do}}$-notation (which expresses a mapping over some M) and a ${\mathsf {join}}$ operator. The definition of these operators, indexed by M, is given in Fig. 5.

Fig. 6.

Elaboration of subtyping (new rules)

Subtyping. The existing rules for 1ML subtyping don’t change, but subtyping now needs to be generalised to computation types $\varPhi$. Figure 6 shows how.

Basically, the six new rules inductively express that $\varPhi _1 \le \varPhi _2$ holds if each $\varXi _1$ from $\varPhi _1$ is a subtype of each $\varXi _2$ from $\varPhi _2$. Except that in the case of a constant effect index, the excluded alternative can be ignored.

The most interesting case is rule $\textsc {Sr}$. It coerces a unique type $\varXi '$ into a sum indexed by an effect $\eta$. Since $\eta$ may force later which alternative to pick, the coercion has to perform a case distinction over $\eta$. To enable that, effects need to be reified as terms in the elaboration. We refer to the Appendix for details. There, we also explain the operators ${\mathsf {asl}}$ and ${\mathsf {asr}}$ used in the elaboration of rules $\textsc {Slp}$ and $\textsc {Sli}$, which are akin to a one-armed ${\mathsf {case}}$ over the binary “$+$” GADT.

Metatheory. For space reasons, we have banished all metatheory to the Appendix, where we define the encoding of semantic types into System F$_\omega$, and state the obvious soundness results for the elaboration.

4 Related Work

There has been a broad range of work on effect systems and effect polymorphism, starting from Gifford & Lucassen’s original work [3, 9] and Talpin & Jouvelot’s refinements [18]. But as noted in the introduction, the implications of effect polymorphism that we have investigated in this paper is rather esoteric – to the best of our knowledge, there is no other work on effect systems for modules, or generativity polymorphism of the kind we introduced here.

“True” Higher-Order Modules. The idea most closely related hence actually is MacQueen’s notion of “true” higher-order modules, as originally introduced by MacQueen & Tofte [10], implemented in SML of New Jersey, and later recast by Kuan & MacQueen [6, 7]. In this semantics, every functor type is implicitly “generativity polymorphic” as much as possible.

However, the formal details are rather involved, defining a specialised operational calculus of type name creation, path trees, and explicit environment manipulation (named the “entity calculus” in Kuan & MacQueen’s more recent work). This semantics has so far escaped a more type-theoretic treatment, and consequently, none of the other formalisations of higher-order modules on the market [2, 4, 8, 13–15, 17] has followed its lead.

The system we presented is coming from a completely different angle. Yet, as we show in Sect. 2, it has similar expressiveness, while maintaining most of the relative simplicity of the 1ML semantics. One could argue that effect polymorphism is what was hiding in MacQueen’s system all along, and that our system makes that explicit and gives it a foundation in standard type theory.

Monads, Polymonads and Productoids. Moggi [12] suggested monads as a means for semantic modeling of effectful computations. Wadler [20] recognised their broader value for language design, as an immensely viable user-facing feature, which became a cornerstone of Haskell.

Our paper on F-ing modules [15] already pointed out that existentials behave “like a monad” in our semantics, encapsulating the underlying “effect” of type generation. However, we never formally investigated the connection. A slightly more careful look reveals that it’s not really a single monad, but a whole stack of them: one for each abstract type generated.

In the current paper, this interpretation as nested monads is no longer sufficient. Computation types are sums of existentials. In order to maintain this invariant under composition, composition can no longer be just nesting. Consequently, they give rise to a more general, more heterogeneous structure.

Hicks et al. [5] have recently investigated a generalisation of this kind of structure under the name polymonad. One way to describe it is as a set of monadic type constructors with heterogeneous ${\mathsf {bind}}$ (or ${\mathsf {join}}$) operators. Independently, Tate [19] introduced a similar, slightly more general notion he calls productoids. In both cases, these formal structures were motivated by the desire to model certain forms of effects (though both works only investigate classical term-level effects).

Our computation types $\varPhi$, when factored into monadic constructors M, are an instance of this general structure. However, they are higher-kinded: they take a(nother) type constructor as argument, to allow transmitting the choice of type names to the “value” type. We leave a closer investigation of their exact relation to polymonads and productoids, and their formal properties, to future work.

5 Future Work

The current paper is primarily a sketch of a basic system. As always, there are many future roads to go. To mention only a few:

Implementation. We would like to integrate effect polymorphism into our 1ML prototype interpreter (mpi-sws.org/~rossberg/1ml/), to gather some practical experience from more experiments with the system.

Effect Inference. In the current paper we have only investigated the explicitly-typed fragment of 1ML. We believe that it is straightforward to incorporate implicit functions over effects to full 1ML, and enable the inference of effect parameters and arguments, just like for types.

More Effects. Our little language provides “impurity” (or partiality, if you prefer) as the only effect. That is as coarse as it can get. While already useful, it would be interesting to refine it to distinguish different concrete effects.

Abstract Effects. We have not yet explored what kind of abstractions might be enabled by the notion of abstract effect that our system introduces. Is it useful?

A Elaboration

1.1 A.1 Internal Language

As in the F-ing modules semantics [15] and the original 1ML paper [13], we define the semantics of the extended language by elaborating 1ML$_{\mathop {\mathrm {ex}}\nolimits }$ types and terms into types and terms of a (call-by-value, impredicative) variant of System F$_\omega$ with simple record types – see the syntax in Fig. 7.

Fig. 7.

Syntax and non-standard typing rules of F$_\omega$ with binary GADTs

However, this time we need a small extension over plain F$_\omega$: to track generativity effects and the different forms of quantification they can cause in an indexed sum, we require a simple notion of GADT. We add this to F$_\omega$ in the simplest possible form: an indexed binary sum $(\tau _1 + \tau _2)^\tau$. Operationally, it is equivalent to an ordinary sum, with injections ${\mathsf {inl}} \,e$ and ${\mathsf {inr}} \,e$ and a ${\mathsf {case}}$ construct for elimination. However, the index $\tau$ allows deducing the choice statically: if it is equivalent to the type $\top$, then the value is known to be a left injection; analogously, $\bot$ implies a right injection. Accordingly, there are two additional elimination constructs, ${\mathsf {asl}} \,e$ and ${\mathsf {asr}} \,e$, that are only valid on operands with known index, and perform the respective projection (they correspond to a one-armed case in more general forms of GADTs).

Figure 7 shows the syntax for this IL. The non-standard extensions just described are . The figure also includes the typing and kinding rules for those additional constructs. We omit reduction rules, because they are straightforward. The semantics is otherwise completely standard, and reuses the formulation from [15].

We write $\varGamma \vdash e : \tau$ for the F$_\omega$ typing judgement, and let $e \hookrightarrow e'$ denote (one-step) reduction. As one would hope, the language enjoys the standard soundness properties:

Theorem 1

(Preservation). If $\cdot \vdash e : \tau$ and $e \hookrightarrow e'$, then $\cdot \vdash e' : \tau$.

Theorem 2

(Progress). If $\cdot \vdash e : \tau$ and e is not a value, then $e \hookrightarrow e'$ for some $e'$.

To establish soundness of 1ML it suffices to ensure that elaboration always produces well-typed F$_\omega$ terms (Sect. A.3).

Fig. 8.

Encoding of semantic types in F$_\omega$

1.2 A.2 Encoding Semantic Types

Elaboration translates 1ML$_{\mathop {\mathrm {ex}}\nolimits }$ types directly into “equivalent” System F$_\omega$ types. The shape of these semantic types was given by the grammar in Fig. 2.

Not all the forms in that grammar are unadorned F$_\omega$ types, however. Some are auxiliary forms that are definable as syntactic sugar. Figure 8 shows how they can be encoded, along with respective term-level constructs for defining the evidence terms of the elaboration.

Several tricks in the elaboration are new relative to plain 1ML:

• Computation types are represented using the indexed binary sums introduced in the previous section. Their index is (the desugaring of) an effect type applied to $\top$ and $\bot$.

• To this end, effect types are represented as type constructors representing a simple Church-style encoding of Booleans. The kind of effect types hence is ${{\mathsf {Eff}}} = \varOmega \rightarrow \varOmega \rightarrow \varOmega$, and their application behaves like a conditional.

• Effects also need to be reified on the term level, however, in order to enable reflection as needed in rule $\textsc {Sr}$. We use a binary sum (over units) for that purpose that is indexed by the corresponding type-level effect encoding – terms of type $\textsf {eff}\; \eta$ are term-level encodings of effect type $\eta$.

• Since effects $\eta$ can contain effect variables $\iota$, this in turn requires those to be represented on both the type and term level. We use the trick of “twinning” each effect variable $\iota$ in the environment $\varGamma$ as both a type variable $\alpha _\iota$ and a term variable $x_\iota$, assuming appropriate namespace injections. Likewise, every abstraction and quantification over effect variables consistently happens on both levels.

These encodings make sense, because the following consistency properties hold (note how we overload effects $\eta$ as notation for both types and terms):

Proposition 1

(Derivable Rules for Effect Encodings). Let $\varGamma$ be a well-formed System F$_\omega$ environment.

• 1. $\varGamma \vdash {\mathop {\mathrm {\texttt {I}}}\nolimits }: {{\mathsf {Eff}}}$.

• 2. $\varGamma \vdash {\mathop {\mathrm {\texttt {P}}}\nolimits }: {{\mathsf {Eff}}}$.

• 3. If $\iota \in \varGamma$, then $\varGamma \vdash \alpha _\iota : {{\mathsf {Eff}}}$.

• 4. If $\varGamma \vdash \eta _1 : {{\mathsf {Eff}}}$ and $\varGamma \vdash \eta _2 : {{\mathsf {Eff}}}$, then $\varGamma \vdash \eta _1 \vee \eta _2 : {{\mathsf {Eff}}}$

• 5. $\varGamma \vdash {\mathop {\mathrm {\texttt {I}}}\nolimits }: {\mathsf {eff}} {\mathop {\mathrm {\texttt {I}}}\nolimits }$.

• 6. $\varGamma \vdash {\mathop {\mathrm {\texttt {P}}}\nolimits }: {\mathsf {eff}} {\mathop {\mathrm {\texttt {P}}}\nolimits }$.

• 7. If $\iota \in \varGamma$, then $\varGamma \vdash x_\iota : {\mathsf {eff}} \alpha _\iota$.

• 8. If $\varGamma \vdash \eta _1 : {\mathsf {eff}} \eta _1$ and $\varGamma \vdash \eta _2 : {\mathsf {eff}} \eta _2$, then $\varGamma \vdash \eta _1 \vee \eta _2 : {\mathsf {eff}} (\eta _1 \vee \eta _2)$.

Here, we write “$\iota \in \varGamma$ as a shorthand for “$\varGamma (\alpha _\iota ) = {{\mathsf {Eff}}} \wedge \varGamma (x_\iota ) = {\mathsf {eff}} \alpha _\iota$”, in correspondence to the twinning for effect variables explained above.

With the notation $\mathrel {\mathsf {Mon}} _{\overline{\kappa }}$ to denote the kind of a monadic computation constructor mentioning abstract types of kinds $\overline{\kappa }$, similar consistency properties can be shown for the polymonad notation from Fig. 5:

Proposition 2

(Derivable Rules for Polymonads). Let $\varGamma$ be a well-formed System F$_\omega$ environment.

• 1. If $\overline{\varGamma , \overline{\alpha }\vdash \pi : \kappa }$, then $\varGamma \vdash \exists \overline{\alpha }[\overline{\pi }] : {{\mathsf {Mon}}}_{\overline{\kappa }}$.

• 2. If $\varGamma \vdash M_1 : {{\mathsf {Mon}}}_{\overline{\kappa }}$ and $\varGamma \vdash M_2 : {{\mathsf {Mon}}}_{\overline{\kappa }}$ and $\varGamma \vdash \eta : {{\mathsf {Eff}}}$, then $\varGamma \vdash (M_1 + M_2)^\eta : {{\mathsf {Mon}}}_{\overline{\kappa }}$.

• 3. If $\varGamma \vdash M_1 : {{\mathsf {Mon}}}_{\overline{\kappa }_1}$ and $\varGamma \vdash M_2 : {{\mathsf {Mon}}}_{\overline{\kappa }_2}$, then $\varGamma \vdash M_1 M_2 : {{\mathsf {Mon}}}_{\overline{\kappa }_1 \overline{\kappa }_2}$.

• 4. If $\varGamma \vdash M : {{\mathsf {Mon}}}_{\overline{\kappa }_\alpha }$ and $\varGamma \vdash e_1 : M \lambda \overline{\alpha }. \tau _1$ and $\varGamma , \overline{\alpha }, x{:}\tau _1 \vdash e_2 : \tau _2$, then $\varGamma \vdash ({\mathsf {do}} _M \overline{\alpha }, x \leftarrow e_1 \mathrel {\mathsf {in}} e_2) : M \lambda \overline{\alpha }. \tau _2$.

• 5. If $\varGamma \vdash M_1 : {{\mathsf {Mon}}}_{\overline{\kappa }_1}$ and $\varGamma \vdash M_2 : {{\mathsf {Mon}}}_{\overline{\kappa }_2}$ and $\varGamma \vdash e : M_1 \lambda \overline{\alpha }_1. M_2 \lambda \overline{\alpha }_2. \tau$, then $\varGamma \vdash {\mathsf {join}} _{M_1 M_2} e : M_1 M_2 \lambda \overline{\alpha }_1 \overline{\alpha }_2. \tau$.

Note that our use of ${\mathsf {do}}$-notation is a slight abuse (if you’re coming from Haskell, anyway): it actually is a ${{\mathsf {map}}}$, not a monadic ${{\mathsf {bind}}}$ – both are instances of polymonadic binds, however.

1.3 A.3 Meta-Theory

With the previous propositions we can verify that elaboration is correct:

Proposition 3

(Correctness of Elaboration). Let $\varGamma$ be a well-formed F$_\omega$ environment.

• 1. If $\varGamma \vdash T/D \rightsquigarrow \varXi$, then $\varGamma \vdash \varXi : \varOmega$.

• 2. If $\varGamma \vdash F \rightsquigarrow \eta$, then $\varGamma \vdash \eta : {\mathsf {Eff}}$.

• 3. If $\varGamma \vdash E/B :_\eta \varPhi \rightsquigarrow e$, then $\varGamma \vdash e : \varPhi$ and $\varGamma \vdash \eta : {\mathsf {Eff}}$. Furthermore, if $\eta = {\mathop {\mathrm {\texttt {P}}}\nolimits }$ then ${\varPhi \,!} = \varSigma$.

• 4. If $\varGamma \vdash \varPhi ' \le _{\overline{\alpha \overline{\alpha }'}} \varPhi \rightsquigarrow \delta ; f$ and $\varGamma \vdash \varPhi ' : \varOmega$ and $\varGamma , \overline{\alpha }\vdash \varPhi : \varOmega$, then $\mathbin {\mathrm {dom}} (\delta ) = \overline{\alpha }$ and $\varGamma \vdash \delta : \varGamma ,\overline{\alpha }$ and $\varGamma \vdash f : \varPhi ' \rightarrow \delta \varPhi$.

Together with the standard soundness result for F$_\omega$ we can tell that the extension of 1ML$_{\mathop {\mathrm {ex}}\nolimits }$ is still sound:

Theorem 3

(Soundness of $\mathbf {1ML}_\mathrm{ex}$ with Effect Polymorphism). If $\cdot \vdash E : \varPhi \rightsquigarrow e$, then either $e \uparrow$ or $e \hookrightarrow ^* v$ such that $\cdot \vdash v : \varPhi$ and v is a value.