Interoperability for ML and a Linear Language

Anonymous for submission

Gabriel Scherer12 Max New1 Nick Rioux1 Amal Ahmed13
Northeastern University, US
INRIA Saclay, France
INRIA Paris, France

Gabriel Scherer
Max New
Nick Rioux
Amal Ahmed
Northeastern UniversityUS

Instead of a monolithic programming language trying to cover all
features of interest, some programming systems are designed by
combining together simpler languages that cooperate to cover the
same feature space. This can improve usability by making each part
simpler than the whole, but there is a risk of abstraction
leaks from one language to another that would break expectations
of the users familiar with only one or some of the involved

We propose a formal specification for what it means for a given
language in a multi-language system to be usable without leaks: it
should embed into the multi-language in a fully abstract way,
that is, its contextual equivalence should be unchanged in the
larger system.

To demonstrate our proposed design principle and formal
specification criterion, we design a multi-language programming
system that combines an ML-like statically typed functional language
and another language with linear types and linear state. Our goal is
to cover a good part of the expressiveness of languages that mix
functional programming and linear state (ownership), at only
a fraction of the complexity.  We prove that the embedding of ML
into the multi-language system is fully abstract: functional
programmers should not fear abstraction leaks. We show examples of
combined programs demonstrating in-place memory updates and safe
resource handling, and an implementation extending OCaml with our
linear language.

Note: Due to severe space restrictions, many details have been omitted
from this presentation of our work. We strongly encourage the reader
to consult the complete version at <https://arxiv.org/pdf/1707.04984>

§ INTRODUCTION

Feature accretion is a common trend among mature but actively evolving
programming languages, including C++, Haskell, Java, OCaml, Python, and
Scala. Each new feature strives for generality and expressiveness, and
may provide a large usability improvement to users of the particular
problem domain or programming style it was designed to empower (e.g., XML
documents, asynchronous communication, staged evaluation).  But
feature creep in general-purpose languages may also make it harder for
programmers to master the language as a whole, degrade the
user experience (e.g., leading to more cryptic error messages),
require additional work on the part of tooling providers, and lead to
fragility in
language implementations.

A natural response to increased language complexity is to define subsets
of the language designed for a better programming experience.  For
instance, a subset can be easier to teach (e.g., “Core”
Haskell 98 as opposed to GHC Haskell, Scala mastery
levels[<http://www.scala-lang.org/old/node/8610>]); it
can facilitate static analysis or decrease the risk of programming
while remaining sufficiently expressive for the target users'
needs (e.g., MISRA C, Spark/Ada); it can enforce a common style within
a company; or it can be designed to encourage a transition to deprecate
some ill-behaved language features (e.g., strict Javascript).

Once a subset has been selected, it may be the case that users write
whole programs purely in the subset (possibly using tooling to enforce
that property), but programs will commonly rely on other libraries
that are not themselves implemented in the same subset of the
language.  If users stay in the subset while using these libraries,
they will only interact with the part of the library whose interface is
expressible in the subset.  But does the behavior of the library
respect the expectations of users who only know the subset?

When calling a function from within the subset breaks subset
expectations, it is a sign of leaky abstraction.

How should we design languages with useful subsets that manage
complexity and avoid abstraction leaks?

We propose to look at this question from a different, but equivalent,
angle: instead of designing a single big monolithic language with some
nicer subsets, we propose to consider multi-language
programming systems where several smaller programming languages
interact together to cover the same feature space. Each language or
sub-combination of languages is a subset, in the above sense, of the
multi-language, and there is a clear definition of abstraction
leaks in terms of user experience: a user who only knows some
of the languages of the system should be able to use the
multi-language system, interacting with code written in the other
languages, without have their expectations violated. If we write a
program in Java and call a function that, internally, is
implemented in Scala, there should be no surprises—our experience
should be the same as when calling a pure Java function. Similarly,
consider the subset of Haskell that does not contain
(input-output as a type-tracked effect): the expectations of a user of
this language, for instance in terms of valid equational reasoning,
should not be violated by adding  back to the language—in
the absence of the abstraction-leaking .

We propose a formal specification for a “no abstraction
leaks” guarantee that can be used as a design criterion to design new
multi-language systems, with graceful interoperation properties. It is
based on the formal notion of full abstraction which has
previously been used to study the denotational semantics of programming
languages <cit.>,
and the formal property of
compilers <cit.>,
but not for
user-facing languages. A
compiler $C$ from a source language $S$ to a target language $T$ is
fully abstract if, whenever two source terms $s_1$ and $s_2$
are indistinguishable in $S$, their translations $C(s_1)$ and $C(s_2)$
are indistinguishable in $T$. In a multi-language $G + E$ formed of a
general-purpose, user-friendly language $G$ and a more advanced
language $E$—one that provides an escape hatch for
experts to write code that can't be implemented in $G$—we say
that $E$ does not leak into $G$ if the embedding of $G$ into the
multi-language $G + E$ is fully abstract.

To demonstrate that our formal specification is reasonable, we design
a novel multi-language programming system that satisfies it. Our
multi-language $\ullang$ combines a general-purpose functional
programming language $\ulang$ (unrestricted) of the ML family with
an advanced language $\llang$ (linear) with linear types and linear
state. It is less convient to program in $\llang$'s restrictive type
system, but users can write programs in $\llang$ that could not be
written in $\ulang$: they can use linear types, locally, to enforce
resource usage protocols (typestate), and they can use linear state
and the linear ownership discipline to write programs that do in-place
update to allocate less memory, yet remain observationally pure.

Consider for example the following mixed-language program. The blue
fragments are written in the general-purpose, user-friendly functional
language, while the red fragments are written in the linear
language.  The boundaries $\ufont{UL}$ and $\lfont{LU}$ allow
switching between languages. The program reads all lines from a file,
accumulating them in a list, and concatenating it into a single string
when the end-of-file (EOF) is reached.

/!let concat_lines path : String = UL(/*
loop (open LU(/!path!/)) LU(/!Nil!/)
where rec loop handle LU(/!acc : List String!/) =
match line handle with
| Next line LU(/!handle!/) -> loop handle LU(/!Cons line acc!/)
| EOF handle -> close handle; LU(/!rev_concat "" acc!/)*/)!/

The linear type system ensures that the file handle is properly
closed: removing the $\lfont{close}~\lfont{handle}$ call would give a type
error. On the other hand, only the parts concerned with the
resource-handling logic need to be written in the red linear language;
the user can keep all general-purpose logic (here, how to accumulate
lines and what to do with them at the end) in the more convenient
general-purpose blue language—and call this function from a
blue-language program. Fine-grained boundaries allow users to rely on
each language's strength and to use the advanced features only when

In this example, the file-handle API specifies that the call to
$\lfont{line}$, which reads a line, returns the data at type
$\llumpedty{\ufont{String}}$.  The latter represents how $\usymbol$
values of type $\ufont{String}$ can be put into a lump type to
be passed to the linear world where they are treated as opaque
blackboxes that must be passed back to the ML world for consumption.

For other examples, such as in-place list manipulation or
transient operations on an persistent data structure, we will need a
deeper form of interoperability where the linear world creates,
dissects or manipulates $\usymbol$ values. To enable this, our
multi-language supports translation of types from one language to the
other, using a type compatibility relation $\uty \ulcompat
\lty$ between $\ulang$ types $\uty$ and $\llang$ types $\lty$.

We claim the following contributions:

* We propose a formal specification of what it means for advanced
language features to be introduced in a (multi-)language system
without introducing a class of abstraction leaks that break
equational reasoning. This specification captures a useful
usability property, and we hope it will help us and others
design more usable programming languages, much like the formal
notion of principal types served to better understand and
design type inference systems.

* We design a simple linear language, $\llang$, that supports
linear state (sec:u-and-l). This simple design for linear
state is a contribution of its own. A nice property of the language
(shared by some other linear languages) is that the code has both an
imperative interpretation—with in-place memory update, which
provides resource guarantees—and a functional
interpretation—which aids program reasoning. The imperative and
functional interpretations have different resource usage, but the
same input/output behavior.

* We present a multi-language programming system $\ullang$
combining a core ML language, $\ulang$ ($\usymbol$ for Unrestricted,
as opposed to Linear) with $\llang$

and prove that the embedding of the ML language $\ulang$ in
$\ullang$ is fully abstract (sec:multi-language).
Moreover, the multi-language is designed to ensure that our full
abstraction result is stable under extension of the embedded ML
language $\ulang$.

* We define a logical relation and prove parametricity for
$\ullang$. The logical relation illustrates, semantically, why one
can reason functionally about programs in $\ullang$ despite the
presence of state and strong updates (sec:logrel).

* We evaluate the resulting language design by providing examples
of hybrid $\ullang$ programs that exhibit programming patterns
inaccessible to ML alone, such that safe in-place updates and
typestate-like static protocol enforcement
(sec:examples), and describe our prototype implementation

§ THE U AND L LANGUAGES

1 2

1 2

, ,

Unrestricted Language: Syntax

The unrestricted language $\ulang$ is a run-of-the-mill idealized ML
language with functions, pairs, sums, iso-recursive types and
polymorphism. It is presented in its explicitly typed form—we will
not discuss type inference in this work. The full syntax is described
in fig:u:syntax, and the typing rules in
fig:u:staticsem.  The dynamic semantics is completely
standard. Having binary sums, binary products and iso-recursive types
lets us express algebraic datatypes in the usual way.

Unrestricted Language: Static Semantics

The novelty lies in the linear language $\llang$, which we present in
several steps. As is common in $\lambda$-calculi with references, the
small-step operational semantics is given for a language that is not
exactly the surface language in which programs are written, because
memory allocation returns locations $\lloc$ that are not in the
grammar of surface terms. Reductions are defined on
configurations, a local store paired with a term in
a slightly larger internal language. We have two type systems,
a type system on surface terms, that does not mention locations and
stores—which is the one a programmer needs to know—and a type
system on configurations, which contains enough static information to
reason about the dynamics of our language and prove subject
reduction. Again, this follows the standard structure of syntactic
soundness proofs for languages with a mutable store.

We present the surface language and type system in
subsec:l-intro, except for the language fragment
manipulating the linear store which is presented in
subsec:l:store. Finally, the internal terms, their
typing and reduction semantics are presented in

§.§ The Core of L

fig:l:surface-syntax presents the surface syntax of our
linear language $\llang$. For the syntactic categories of types
$\lty$, and expressions $\le$, the last line contains the
constructions related to the linear store that we only discuss in

1 ≤2 ≤

1 2

Linear Language: Surface Syntax

In technical terms, our linear type system is exactly propositional
intuitionistic linear logic, extended with iso-recursive

For simplicity and because we did not need them, our current system
also does not have polymorphism or additive/lazy pairs $\lowithty
\ltyone \ltytwo$. Additive pairs would be a trivial addition, but
polymorphism would require more work when we define the multi-language
semantics in sec:multi-language.

In less technical terms, our type system can enforce that values be
used linearly, meaning that they cannot be duplicated or
erased, they have to be deconstructed exactly once. Only some types
have this linearity restriction; others allow duplication and sharing
of values at will. We can think of linear values as resources to
be spent wisely; for any linear value somewhere in a term, there can
be only one way to access this value, so we can interpret the language as
enforcing an ownership discipline where whoever points to
a linear value owns it.

In particular, linear functions of type $\lofunty \ltyone \ltytwo$
must be called exactly once, and their results must in turn be
consumed – they can safely capture linear resources. On the other
hand, the non-linear, duplicable values are those at types of the
form $\lbangty \lty$ — the exponential modality of linear
logic. If the term $\le$ has duplicable type $\lbangty \lty$, then
the term $\lsrccopye \le$ has type $\lty$: this creates a local copy
of the value that is uniquely-owned by its receiver and must be
consumed linearily.

The types of linear values are the type of linear pairs
$\lopairty \ltyone \ltytwo$, of linear disjoint unions
$\losumty \ltyone \ltytwo$, of linear functions
$\lofunty \ltyone \ltytwo$, and of the linear unit type $\lunitty$.
For example, a linear function must be called exactly once, and its
result must in turn be consumed – such linear functions can safely
capture linear resources. The expression-formers at these types use
the same syntax as the unrestricted language $\ulang$, with the
exception of linear pair deconstruction
$\lletpaire \lvone \lvtwo \leone \letwo$, which names both members of
the deconstructed pair at once. A linear pair type with projection
would only ever allow to observe one of the two members; this would
correspond to the additive/lazy pairs $\lowithty \ltyone \ltytwo$,
where only one of the two members is ever computed.

The types of non-linear, duplicable values are the types of the form
$\lbangty \lty$—the exponential modality of linear logic. If
$\le$ has type $\lty$, the term $\lsrcsharee \le$ has type
$\lbangty \lty$. Values of this type are not uniquely owned, they can
be shared at will. If the term $\le$ has duplicable type
$\lbangty \lty$, then the term $\lsrccopye \le$ has type $\lty$: this
creates a local copy of the value that is uniquely-owned by its
receiver and must be consumed linearily.

$\ctxjoin \lGammaone \lGammatwo$

(, )
(, )

(, )         (),     (∉)

(, )
(),     (∉)

$\ljudgnoconf \lGamma \le \lty$

, ,

,  ≤

Linear Language: Surface Static Semantics

head reduction
$\le \lheadredexstep \lepr$
$\hconf \lstore \le \lheadredexstep \hconf \lstorepr \lepr$

(  )

Internal linear language: Typing and reduction (excerpt)

This resource-usage discipline is enforced by the surface typing rules
of $\llang$, presented in fig:l:surface-static-sem. They are
exactly the standard (two-sided) logical rules of intuitionistic
linear logic, annotated with program terms. The non-duplicability of
linear values is enforced by the way contexts are merged by the
inference rules: if $\leone$ is type-checked in the context
$\lGammaone$ and $\letwo$ in $\lGammatwo$, then the linear pair
$\lpaire \leone \letwo$ is only valid in the combined context
$\ctxjoin \lGammaone \lGammatwo$. The $(\ctxjoin{}{})$ operation is
partial; this combined context is defined only if the variables shared
by $\lGammaone$ and $\lGammatwo$ are duplicable—their type is of
the form $\lbangty \lty$. In other words, a variable at
a non-duplicable type in $\ctxjoin \lGammaone \lGammatwo$ cannot
possibly appear in both $\lGammaone$ and $\lGammatwo$: it must appear
exactly once[Standard presentations of linear logic force
contexts to be completely distinct, but have a separate rule to
duplicate linear variables, which is less natural for

A good way to think of the linear judgment
$\ljudgnoconf \lGamma \le \lty$ is that the evaluation of $\le$
consumes the linear variables of $\lGamma$; it is thus natural
that the strict pair $\lpaire \leone \letwo$ would need separate sets
of resources $\lGammaone$ and $\lGammatwo$, as it evaluates both
members to return a value. On the other hand, case elimination
$\lcasee \le \lxone \leone \lxtwo \letwo$ reuses the same context
$\lGammapr$ in both branches $\leone$ and $\letwo$: only one will be
evaluated, so they do not compete for resources.

The expression $\lsrcsharee \le$ takes a term at some type $\lty$
and creates a “shared” term, whose value will be duplicable. Its
typing rule uses a context of the form $\lbangty \lGamma$, which is
defined as the pointwise application of the $(\lbangty)$ connectives
to all the types in $\lGamma$. In other words, the context of this
rule must only have duplicable types : a term can only be made
duplicable if it does not depend on linear resources from the
context. Otherwise, duplicating the shared value could break the
unique-ownership discipline on these linear resources.

The variable rule does not expect a context of the form
$\lGamma, \var \lx \lty$ but of the form
$\lbangty \lGamma, \var \lx \lty$.
Here $\lbangty \lGamma$ is a notation
for the pointwise application of the $(\lbangty)$ connective to all
the types in $\lGamma$—i.e., all types in $\lbangty \lGamma$ are of
the form $\lbangty \lty$.
This means that the variable rule can only be used
when all variables in the context are duplicable, except maybe the
variable that is being used. A context of the form
$\lGamma, \var \lx \lty$ would allow us to forget some variable present
in the context; in our judgment $\ljudgnoconf \lGamma \le \lty$, all
non-duplicable variables in $\lGamma$ must appear (once) in $\le$.

The form $\lbangty \lGamma$ is also used in the typing rule for
$\lsrcsharee \le$: a term can only be made duplicable if it does not
depend on linear resources from the context. Otherwise, duplicating
the shared value could break the unique-ownership discipline on these
linear resources.

Finally, the linear isomorphism notation for $\lfolde {}$ and
$\lunfolde {}$ in fig:l:surface-static-sem defines them as
primitive functions, at the given linear function type, in the empty
context – using them does not consume resources. This notation also
means that, operationally, these two operations shall be inverses of
each other. The rules for the linear store type $\lboxedty \lty$ and
$\lemptyboxty$ are described in subsec:l:store.

Context joining $(\ctxjoin{}{})$ is partial but associative and
commutative. In particular, if
$\ctxjoin {(\ctxjoin \lGammaone \lGammatwo)} \lGammapr$ is defined,
then both $\ctxjoin \lGammai \lGammapr$ are defined.

§.§ Linear Memory in L

The surface typing rules for the linear store are given at the end of
fig:l:store-surface-static-sem. The linear type
$\lboxedty \lty$ represents a memory location that holds a value of
type $\lty$. The type $\lemptyboxty$ represents a location that
has been allocated, but does not currently hold a value.
The primitive
operations to act on this type are given as linear isomorphisms:
$\lnewe {}$ allocates, turning a unit value into an empty location;
conversely, $\lfreee {}$ reclaims an empty location. Putting a value
into the location and taking it out are expressed by $\lboxe {}$ and
$\lunboxe {}$, which convert between a pair of an empty location and
a value, of type $\lunboxedty \lty$, and a full location, of type
$\lboxedty \lty$.

For example, the following program takes a full reference and a value,
and swaps the value with the content of the reference:

p ()
r p
l xl
l  xl

p ()

r p

l xl

l  xl

The programming style following from this presentation of linear
memory is functional, or applicative, rather than imperative. Rather
than insisting on the mutability of references—which is allowed by
the linear discipline—we may think of the type $\lboxedty \lty$ as
representing the indirection through the heap that is implicit in
functional programs. In a sense, we are not writing imperative
programs with a mutable store, but rather making explicit the
allocations and dereferences happening in higher-level purely
functional language. In this view, empty cells allow memory reuse.

This view that $\lboxedty \lty$ represents indirection through the
memory suggests we can encode lists of values of type $\lty$ by the
\lapptyop {LinList} \lty
\defeq
\lmuty \lalpha
\lunitty
{\lboxedty {(\lopairty \lty \lalpha)}}}
$.  The placement of the box inside the sum mirrors
the fact that empty list is represented as an immediate value in
functional languages. From this type definition, one can write
an in-place reverse function on lists of $\lty$ as follows:

LinList  LinList

l p

xs p

rev_into xs
( (2 (l acc)))

This definition uses a fixpoint operator $\lfont{fix}$ that can be
defined, in the standard way, using the iso-recursive type
$\lmuty \lalpha {\lofunty \lalpha {\lofunty \lty \ltypr}}$ of the
strict fixpoint combinator on functions $\lofunty \lty \ltypr$.

Our linear language $\llang$ is a formal language that is not
terribly convenient to program directly. We will not present a full
surface language in this work, but one could easily define syntactic
sugar to write the exact same function as follows:

(Cons l xs)
(Cons l acc)

One can read this function as the usual functional
function on lists, annotated with memory reuse
information: if we assume we are the unique owner of the input list
and won't need it anymore, we can reuse the memory of its cons cells
(given in this example the name $\lfont{l}$) to store the reversed
list. On the other hand, if you read the $\lboxe{}$ and $\lunboxe{}$
as imperative operations, this code expresses the usual imperative
pointer-reversal algorithm.

This double view of linear state occurs in other programming systems
with linear state. It was recently emphasized in <cit.>,
where the functional point of view is seen as easing formal
verification, while the imperative view is used as a compilation
technique to produce efficient C code from linear programs.

§.§ Internal L Syntax and Typing

To give a dynamic semantics for $\llang$ and prove it sound, we need
to extend the language with explicit stores and store
locations. Indeed, the allocating term $\lnewe \lunite$ should reduce
to a “fresh location” $\lloc$ allocated in some store $\lstore$, and
neither are part of the surface-language syntax. The corresponding
internal typing judgment is more complex, but note that users do not
need to know about it to reason about correctness of surface
programs. The internal typing is essential for the soundness proof,
but also useful for defining the multi-language semantics in

We work with configurations $\hconf \lstore \le$, which are
pairs of a store $\lstore$ and a term $\le$.  Our internal typing
judgment $\ljudg \lstorety \lGamma \lstore \le \lty$ checks
configurations, not just terms, and relies not only on a typing
context for variables $\lGamma$ but also on a store typing
$\lstorety$, which maps the locations of the configuration to typing

Unfortunately, due to space limits, we will not present this part of
the type system – which is not directly exposed to users of the

We include it for convenience in

See some examples of reduction rules in
fig:l:internal-reduction-excerpt, and the long version of
this work.

§.§ Reduction of Internal Terms

the long version of this work
we give a reduction relation between linear configurations
$\hconf \lstore \le \lredexstep \hconf \lstorepr \lepr$
and prove a subject reduction result.

If $\ljudg \lstorety \lGamma \lstore \le \lty$
and $\hconf \lstore \le \lredexstep \hconf \lstorepr \lepr$,
then there exists a (unique) $\lstoretypr$ such that
$\ljudg \lstoretypr \lGamma \lstorepr \lepr \lty$.

§ MULTI-LANGUAGE SEMANTICS

To formally define our multi-language semantics we create a combined
language $\ullang$ which lets us compose term fragments from both
$\ulang$ and $\llang$ together, and we give an operational semantics
to this combined language. Interoperability is enabled by specifying
how to transport values across the language boundaries.

Multi-language systems in the wild are not defined in this
way: both languages are given a semantics, by interpretation or
compilation, in terms of a shared lower-level language (C, assembly,
the JVM or CLR bytecode, or Racket's core forms), and the two
languages are combined at that level. Our formal multi-language
description can be seen as a model of such combinations, that gives
a specification of the expected observable behavior of this language

Another difference from multi-languages in the wild is our use of very
fine-grained language boundaries: a term written in one language can
have its subterms written in the other, provided the type-checking
rules allow it. Most multi-language systems, typically using Foreign
Function Interfaces, offer coarser-grained composition at the level of
compilation units. Fine-grained composition of existing languages, as
done in the Eco project <cit.>, is difficult because of semantic
mismatches. In sec:examplesthe full version of this
work we demonstrate that fine-grained
composition is a rewarding language design, enabling new programming

§.§ Lump Type and Language Boundaries

(unchanged from fig:u:syntax)

(unchanged from fig:u:syntax)

with  ≤

≤        …

, , ,

Typing rules
$\ulujudg \ulGamma \ue \uty$
$\ulljudg \lstorety \ulGamma \lstore \le \lty$

$\bareuljudg \ulGamma \le \lty
\;\defeq\; \ulljudg \lemptystorety \ulGamma \lemptystore \le \lty$

(Typing rules of $\ujudg \uGamma \ue \uty$
reused, with mixed context $\ulbGamma$)

(Typing rules of $\ljudg \lstorety \lGamma \lstore \le \lty$
reused, with mixed context $\ulGamma$)

Reduction rules

(Reduction rules of $\ulang$ and $\llang$ reused unchanged)

Multi-language: Lump and Boundaries

static compatibility
$\ulSigma \ulwf \uty \ulcompat \lty$

value conversion
$\uv \ulcompate \lty \lv$

i ()

( )

( )

Interoperability: static and dynamic semantics (excerpt)

The core components the multi-language semantics are shown
fig:ul:static-sem—the communication of values from one
language to the other will be described in the next section. The
multi-language $\ullang$ has two distinct syntactic categories of
types, values, and expressions: those that come from $\ulang$ and
those that come from $\llang$. Contexts, on the other hand, are mixed,
and can have variables of both sorts.  For a mixed context $\ulGamma$,
the notation $\lbangty \ulGamma$ only applies $(\lbangty)$ to its
linear variables.

The typing rules of $\ulang$ and $\llang$ are imported into our
multi-language system, working on those two separate categories of
program. They need to be extended to handle mixed contexts $\ulGamma$
instead of their original contexts $\uGamma$ and $\lGamma$. In the
linear case, the rules look exactly the same. In the ML case, the
typing rules implicitly duplicate all the variables in the context.
It would be unsound to extend them to arbitrary linear variables, so
they use a duplicable context $\lbangty \ulGamma$.

To build interesting multi-language programs, we need a way to insert
a fragment coming from a language into a term written in another. This
is done using language boundaries, two new term formers $\LUe \ue$
and $\ULe \lstore \lstorety \le$ that inject an ML term into the
syntactic category of linear terms, and a linear configuration into
the syntactic category of ML terms.

Of course, we need new typing rules for these term-level
constructions, clarifying when it is valid to send a value from
$\ulang$ into $\llang$ and vice versa.  It would be incorrect to allow
sending any type from one language into the other—for instance, by
adding the counterpart of our language boundaries in the syntax of
types—since values of linear types must be uniquely owned so they
cannot possibly be sent to the ML side as the ML type system cannot
enforce unique ownership.

On the other hand, any ML value could safely be sent to the linear
world. For closed types, we could provide a corresponding linear type
($\uunitty$ maps to $\lbangty \lunitty$, etc.), but an ML value may
also be typed by an abstract type variable $\ualpha$, in which case we
can't know what the linear counterpart should be. Instead of trying to
provide translations, we will send any ML type $\uty$ to the
lump type $\llumpty \uty$, which embeds ML types into linear

types. A lump is a blackbox, not a type translation: the linear
language does not assume anything about the behavior of its
values—the values of $\llumpty \uty$ are of the form $\llumpe \uv$,
where $\uv : \uty$ is an ML value that the linear world cannot
use. More precisely, we only propagate the information that ML values
are all duplicable by sending $\uty$ to $\llumpedty \uty$.

The typing rules for language boundaries insert lumps when going
from $\ulang$ to $\llang$, and remove them when going back from
$\llang$ to $\ulang$. In particular, arbitrary linear types cannot
occur at the boundary, they must be of the form $\llumpedty \uty$.

Finally, boundaries have reduction rules: a term or configuration
inside a boundary in reduction position is reduced until it becomes
a value, and then a lump is added or removed depending on the boundary
direction. Note that because the $\lv$ in $\ULe \lstore \lstorety \lv$
is at a duplicable type $\llumpedty \uty$, we know by inversion that
the store is empty.

§.§ Interoperability: Static Semantics

If the linear language could not interact with lumped values at all,
our multi-language programs would be rather boring, as the only way
for the linear extension to provide a value back to ML would be to
have received it from $\ulang$ and pass it back unchanged (as in the
lump embedding of <cit.>). To provide
a real interaction, we provide a way to extract values out of a lump
$\llumpedty \uty$, use it at some linear type $\lty$, and put it back
in before sending the result to $\ulang$.

The correspondence between intuitionistic types $\uty$ and linear
types $\lty$ is specified by a heterogeneous compatibility
relation $\uty \ulcompat \lty$ – defined in full in
. The specification of this
relation is that if $\uty \ulcompat \lty$ holds, then the space of
values of $\llumpedty \uty$ and $\lty$ are isomorphic: we can convert
back and forth between them. When this relation holds, the
term-formers $\lump \lty {}$ and $\unlump \lty {}$ perform the

The term $\LUe \ue$ turns a $\ue : \uty$ into a lumped type
$\llumpedty \uty$, and we need to unlump it with some
$\unlump \lty {}$ for a compatible $\uty \ulcompat \lty$ to interact
with it on the linear side. It is common to combine both operations
and we provide syntactic sugar for it: $\LUmpe \lty \ue$. Similarly
$\UmpLenoconf \lty \le$ first lumps a linear term then sends the result
to the ML world.

§.§ Interoperability: Dynamic Semantics

When the relation
$\uty \ulcompat \lty$ holds, we can define a relation
$\uv \ulcompate \lty \lv$ between the values of $\uty$ and the
values of $\lty$ – see
the long version of this work. It is
functional in both direction: with our definition $\uv$ is uniquely
determined from $\lv$ and conversely. We then define the reduction
rule for (un)lumping: if $\uv \ulcompate \lty \lv$, then

§.§ Full Abstraction from U
into UL

We can now state and prove the major meta-theoretical result of this
work, which is the proposed multi-language design extends the simple
language $\ulang$ in a way that provably has, in a certain sense, “no
abstraction leaks”.

We say that $\ue, \uepr$ such that
$\ujudg \uGamma {\ue, \uepr} \uty$ are contextually
equivalent, written $\ue \uctxeq \uepr$, if, for any expression
context $\uctxt \hw \square$ such that
$\ujudg \uemptyGamma {\uctxt \hw \ue} \uunitty$, the closed terms
$\uctxt \hw \ue$ and $\uctxt \hw \uepr$ are equi-terminating.

We say that $\ue, \uepr$ such that
$\ulujudg \ulGamma {\ue, \uepr} \uty$ are contextually
equivalent, written $\ue \ulctxeq \uepr$, if, for any expression
context $\ulctxt \hw \square$ such that
$\ulujudg \ulemptyGamma {\ulctxt \hw \ue} \uunitty$, the closed terms
$\ulctxt \hw \ue$ and $\ulctxt \hw \uepr$ are equi-terminating.

The embedding of $\ulang$ into $\ullang$ is fully-abstract:

See the full proof argument in appendix:full-abstraction.


11institutetext:  Casey Kennington 22institutetext: Computer Science, Boise
State University, USA, 22email<EMAIL_ADDRESS>33institutetext: Jerry Alan Fails 44institutetext: Computer Science, Boise
State University, USA, 44email<EMAIL_ADDRESS>55institutetext:
Katherine Landau Wright 66institutetext: Literacy, Language and Culture, Boise
State University, USA, 66email<EMAIL_ADDRESS>77institutetext: Maria Soledad Pera 88institutetext: Web Information Systems,
TU Delft, The Netherlands, 88email<EMAIL_ADDRESS>
# Conversational Agents and Children:
Let Children Learn

Casey Kennington and Jerry Alan Fails and Katherine Landau Wright and Maria
Soledad Pera

###### Abstract

Using online information discovery as a case study, in this position paper we
discuss the need to design, develop, and deploy (conversational) agents that
can – non-intrusively – guide children in their quest for online resources
rather than simply finding resources for them. We argue that agents should
“let children learn” and should be built to take on a teacher-facilitator
function, allowing children to develop their technical and critical thinking
abilities as they interact with varied technology in a broad range of use
cases.111This paper was accepted to the Language-Based AI Agent Interaction
with Children @IWSDS’23, Los Angeles, USA - February 21st, 2023

##  1 Introduction

Children are increasingly turning to search engines to seek information on the
Internet Azpiazu2017-fx ; Rowlands2008-uo ; pilgrim2019we ;
gwizdka2017analysis ; usta2014k , but these young children (ages 6-11) are
still in the process of learning literacy skills which, as argued in
Madrazo_Azpiazu2018-pn , affects how they search for and consume information.
Web search for children seems like an obvious setting where an intelligent
conversational agent such as a spoken dialogue system or interactive virtual
agent could make the search process easier by automatically transcribing child
speech into search terms (so the child doesn’t have to type), performing the
search, then selecting and reading aloud the information that the agent thinks
that the child is searching for. Furthermore, web search often requires
multiple iterations of query formulation and an agent could help with the
steps of fine-tuning the search parameters. Such an agent could enable
children to more easily access web resources for entertainment as well as
educational purposes (see Garg2022-jp  for a review of children and voice-
based conversational agents).

Following recent work Aliannejadi2022-op  that explored how technology can
sometimes hinder child learning, in this paper, we take the position that an
automated agent should act as a facilitator in the search process, not
actually perform the work of web search (including transcription) for the
child because doing so can potentially hinder the development of critical
literacy and technical skills. We explain some of the functionality such an
agent should have and the methodology for designing the agent. Moreover, we
take the stance that the agent should be perceived as an adult taking on a
teacher-facilitator role — not as a child peer. Though web search seems like a
relatively narrow use case for automated agents that interact with children,
search is a common and important setting that children begin using early and
we can derive an important guiding principle for all child-directed
conversational agent research: agents should not do for children what children
can do, or should learn to do, for themselves.

##  2 Web Search: A Setting for Learning Critical Skills

Web search is an important domain to consider because many children use web
search tools almost daily Dragovic2016-rt ; gossen2013specifics  and search is
a setting where children’s writing and reading skills enable them to interact
with a broader and increasingly important part of their digital world.
Effective web search requires the application of multiple skills that are
required for effective query formulation, including literacy (i.e., typing,
spelling words, composing words into phrases), understanding how search
results are structured, determining if a resource returned by a search engine
is relevant (i.e., what they were looking for, and reformulating their query
to refine their search). This follows recent work in calling for a _search as
learning_ paradigm gwizdka2016search  that focuses on what web search is good
for: finding information and learning from a wealth of public resources, but
doing so requires properly training children in classroom settings
Landoni2022-fw .

Some of the above-listed skills required for web search are often skipped
altogether when using a conversational agent that automatically transcribes a
verbal request and replies with a specific answer instead of a listing of
resources. While this pattern of interaction allows children to access
information more directly in a context of developing their literacy skills,
one cannot assume that the agent’s response actually fulfills the child’s
particular search need yarosh2018children ; lovato2019hey . Even children who
like using Amazon Echo to request information often do not trust the
information they are given Wojcik2022-fd , which highlights yet another skill
that children need to acquire besides literacy and search: a healthy
skepticism that technology always has the correct answer murray2021more . A
traditional graphical web search interface is not so direct: they don’t just
give the answer; rather, they lead a child searcher to potentially relevant
resources, but the child has to determine if the resource fulfills their
search need.

Our position, therefore, is that conversational agents can help facilitate
children to accomplish tasks, but those agents should not do what children
need to learn to do for themselves, but can provide scaffolding to help
children learn.

##  3 Agent Facilitator: Requirements and Methods for Development

Here we sketch some of the requirements for a child-directed conversational
agent that facilitates learning about web search. The first requirement is
that the agent should be viewed by the child as an adult teacher.222This is
not to say that child agents are never useful; see for example Vogt2017-gn
that explored second language tutoring with a child-like agent, but
researchers should take into consideration the goals and outcomes of the
tutoring when deciding about agent morphology. In Downs2020-gf  we showed that
children prefer adult voices in correcting spelling mistakes, a small yet
crucial aspect of the search process. Moreover, Landoni2020-nz  showed that
children do not prefer a virtual search agent to be a peer. This suggests that
when corrections take place, it is better for the agent to have a clear role
of being a teacher-like facilitator.

Landoni2020-nz  explored child-directed (ages 9-11) search agents by asking
the children to illustrate “Sonny,” a fictitious virtual agent that could help
them find information, then the researchers asked the children what they
thought Sonny should be able to do from a list of options. While the children
indicated that they wanted the agent to be able to talk (i.e., converse
verbally) with them, the children also indicated that they wanted to feel
safe, have fun, and that the agent should remember their previous requests and
take care of privacy. We point out here that the children may have identified
memory as an important aspect of the search because speech-based assistants
like Alexa do not remember dialogue context beyond the current request, making
the ability (or lack thereof) salient to the children. Remembering prior
interactions is crucial to not only to learn about a particular child’s
preferences, but, perhaps more importantly, to recognize the literary and
search skill levels of the child and how to help the child improve those
skills.

The role of the agent should be clear to the child, and here we are advocating
for a teacher-facilitator role. An agent that takes on a facilitator role
should use proper pedagogical methodology because children are in a crucial
developmental stage where they are learning many new things, and learning best
occurs when children are given opportunities to attempt challenging tasks with
proper support. If the task is too easy (i.e., the agent completes the task
for the child), the child will not learn. If the task is too hard and the
child is not provided scaffolded support that will help them be successful,
they will become frustrated and disengaged. A facilitator agent can ensure
that children are working within this “Zone of Proximal Development” (ZPD)
vygotsky1978mind  – where a task is challenging enough for them to learn while
not causing excessive frustration.

To illustrate how ZPD would work in a web search setting, consider an agent
that recognizes a misspelling and flatly utters _that’s spelled incorrectly_.
This would not help a child improve their spelling and could negatively
reinforce to the child that making mistakes is bad. In this instance, the
child will not improve as a speller or searcher. However, if the agent simply
corrects the spelling automatically without drawing any attention to the
error, the child is not provided any opportunity to learn. Rather, an
inquisitive attitude of _hmm, the spelling there doesn’t look right, can you
check the spelling of that word?_ , coupled with spelling suggestions, gives
the impression that being willing to make mistakes and correct them is part of
the learning process. It also gives the child an opportunity to review and
identify the spelling error on their own, rather than the error being auto-
corrected by the system. This means that not only should the agent take on a
facilitator role, but as argued in Murgia2021-xe ; Fails2022-xr , teachers
should be part of the design process of how the agents look and how the agents
act.

Recent work that focused on an “Effective reading partner” conversational
agent did not just read to the child; the agent asked questions and provided
feedback on a small set of topics relating to weather. The authors claim that
the agent could be used to enhance the motivation for children to read
Xu2020-gz , likely because the agent is mirroring what a good teacher does
during a classroom read-aloud. Skilled teachers build engagement around a text
by asking students questions, thinking-aloud, re-phrasing questions, and
building connections between the text and the world. Oftentimes algorithms and
models are trained to provide a specific result or classification; teachers
are well-trained to scaffold and support children as they learn and apply
skills (which no agent will fully replace). In some cases, teachers may answer
questions directly (as Google sometimes does at the top of its search results
page), but teachers also help children think about what the answers mean.
Conversational agents for children need to build on both kinds of training. In
order to best capture the wealth of knowledge teachers have and to better
address children’s particular needs, we also advocate for a participatory
design approach where diverse stake-holders can utilize their experiences,
perspectives, and expertise to collaboratively co-construct a solution. The
scaffolding required to effectively implement a teacher-facilitator
conversational agent requires that teacher’s expertise be well represented.
Additionally, children – as the intended users of the system – can also lend
valuable insights into the design of technology as they co-design with adults
fails_methods_2013 .

##  4 Conclusion: Better Building Together

In this paper, we present a case for teacher-facilitator agents in the domain
of information discovery. The agent should have some adult-like
anthropomorphic characteristics that clearly signal their role to a child
(e.g., adult voice) and the agent should operate in the Zone of Proximal
Development to ensure that the child is stretched, but not overwhelmed as the
child learns how literary and technical skills complement each other. We
therefore advocate that teachers who have training and experience in educating
children should be part of the design process of conversational agents that
interact with children, and we also believe that children should have a voice
in the design process.

###### Acknowledgements.

Thank you to the anonymous reviewers for their helpful feedback. Work funded
by NSF Award # 1763649.

## References

  * [1] Ion Madrazo Azpiazu, Nevena Dragovic, Maria Soledad Pera, and Jerry Alan Fails.  Online searching and learning: YUM and other search tools for children and teachers.  Inf. Retr. Boston., 20(5):524–545, October 2017.
  * [2] Ian Rowlands, David Nicholas, Peter Williams, Paul Huntington, Maggie Fieldhouse, Barrie Gunter, Richard Withey, Hamid R Jamali, Tom Dobrowolski, and Carol Tenopir.  The google generation: the information behaviour of the researcher of the future.  Aslib Proc., 60(4):290–310, January 2008.
  * [3] Jodi Pilgrim.  Are we preparing students for the web in the wild? an analysis of features of websites for children.  The Journal of Literacy and Technology, 20(2):97–124, 2019.
  * [4] Jacek Gwizdka and Dania Bilal.  Analysis of children’s queries and click behavior on ranked results and their thought processes in google search.  In Proceedings of the 2017 conference on conference human information interaction and retrieval, pages 377–380, 2017.
  * [5] Arif Usta, Ismail Sengor Altingovde, Ibrahim Bahattin Vidinli, Rifat Ozcan, and Özgür Ulusoy.  How k-12 students search for learning? analysis of an educational search engine log.  In Proceedings of the 37th international ACM SIGIR conference on Research & development in information retrieval, pages 1151–1154, 2014.
  * [6] Ion Madrazo Azpiazu, Nevena Dragovic, Oghenemaro Anuyah, and Maria Soledad Pera.  Looking for the movie seven or sven from the movie frozen? a multi-perspective strategy for recommending queries for children.  In Proceedings of the 2018 Conference on Human Information Interaction & Retrieval, CHIIR ’18, pages 92–101, New York, NY, USA, March 2018\. Association for Computing Machinery.
  * [7] Radhika Garg, Hua Cui, Spencer Seligson, Bo Zhang, Martin Porcheron, Leigh Clark, Benjamin R Cowan, and Erin Beneteau.  The last decade of HCI research on children and voice-based conversational agents.  In Proceedings of the 2022 CHI Conference on Human Factors in Computing Systems, number Article 149 in CHI ’22, pages 1–19, New York, NY, USA, April 2022. Association for Computing Machinery.
  * [8] Mohammad Aliannejadi, Theo Huibers, Monica Landoni, Emiliana Murgia, and Maria Soledad Pera.  The effect of prolonged exposure to online education on a classroom search companion.  In Experimental IR Meets Multilinguality, Multimodality, and Interaction, pages 62–78. Springer International Publishing, 2022.
  * [9] Nevena Dragovic, Ion Madrazo Azpiazu, and Maria Soledad Pera.  “is sven seven?”: A search intent module for children.  In Proceedings of the 39th International ACM SIGIR conference on Research and Development in Information Retrieval, SIGIR ’16, pages 885–888, New York, NY, USA, July 2016. Association for Computing Machinery.
  * [10] Tatiana Gossen and Andreas Nürnberger.  Specifics of information retrieval for young users: A survey.  Information Processing & Management, 49(4):739–756, 2013.
  * [11] Jacek Gwizdka, Preben Hansen, Claudia Hauff, Jiyin He, and Noriko Kando.  Search as learning (sal) workshop 2016.  In Proceedings of the 39th International ACM SIGIR conference on Research and Development in Information Retrieval, pages 1249–1250, 2016.
  * [12] Monica Landoni, Maria Soledad Pera, Emiliana Murgia, and Theo Huibers.  Let’s learn from children: Scaffolding to enable search as learning in the educational environment.  September 2022.
  * [13] Svetlana Yarosh, Stryker Thompson, Kathleen Watson, Alice Chase, Ashwin Senthilkumar, Ye Yuan, and AJ Bernheim Brush.  Children asking questions: speech interface reformulations and personification preferences.  In Proceedings of the 17th ACM conference on interaction design and children, pages 300–312, 2018.
  * [14] Silvia B Lovato, Anne Marie Piper, and Ellen A Wartella.  Hey google, do unicorns exist? conversational agents as a path to answers to children’s questions.  In Proceedings of the 18th ACM international conference on interaction design and children, pages 301–313, 2019.
  * [15] Erica H Wojcik, Aarathi Prasad, Samantha P Hutchinson, and Kyla Shen.  Children prefer to learn from smart devices, but do not trust them more than humans.  International Journal of Child-Computer Interaction, 32:100406, June 2022.
  * [16] Grace W Murray.  Who is more trustworthy, alexa or mom?: Children’s selective trust in a digital age.  2021\.
  * [17] Paul Vogt, Mirjam de Haas, Chiara de Jong, Peta Baxter, and Emiel Krahmer.  Child-robot interactions for second language tutoring to preschool children.  Front. Hum. Neurosci., 11:73, March 2017.
  * [18] Brody Downs, Aprajita Shukla, Mikey Krentz, Maria Soledad Pera, Katherine Landau Wright, Casey Kennington, and Jerry Fails.  Guiding the selection of child spellchecker suggestions using audio and visual cues.  In Proceedings of the Interaction Design and Children Conference, IDC ’20, pages 398–408, New York, NY, USA, June 2020. Association for Computing Machinery.
  * [19] Monica Landoni, Emiliana Murgia, Theo Huibers, and Maria Soledad Pera.  You’ve got a friend in me: Children and search agents.  In Adjunct Publication of the 28th ACM Conference on User Modeling, Adaptation and Personalization, UMAP ’20 Adjunct, pages 89–94, New York, NY, USA, July 2020. Association for Computing Machinery.
  * [20] Lev Semenovich Vygotsky and Michael Cole.  Mind in society: Development of higher psychological processes.  Harvard university press, 1978.
  * [21] Emiliana Murgia, Monica Landoni, Theo Huibers, and Maria Soledad Pera.  All together now: Teachers as research partners in the design of search technology for the classroom.  May 2021.
  * [22] Jerry Alan Fails, Monica Landoni, Theo Huibers, and Maria Soledad Pera.  Report on the 5th workshop on international and interdisciplinary perspectives on children & recommender and information retrieval systems (KidRec 2021) at IDC 2021: the teacher lens.  SIGIR Forum, 55(2):1–6, March 2022.
  * [23] Ying Xu and Mark Warschauer.  Exploring young children’s engagement in joint reading with a conversational agent.  In Proceedings of the Interaction Design and Children Conference, IDC ’20, pages 216–228, New York, NY, USA, June 2020. Association for Computing Machinery.
  * [24] Jerry Alan Fails, Mona Leigh Guha, and Allison Druin.  Methods and Techniques for Involving Children in the Design of New Technology for Children.  Now Publishers Inc., Hanover, MA, USA, 2013.