corbin-ocap17-monte.lyx

#LyX 2.2 created this file. For more info see http://www.lyx.org/
\lyxformat 508
\begin_document
\begin_header
\save_transient_properties true
\origin unavailable
\textclass article
\begin_preamble
\usepackage{microtype}

\usepackage{hyperref}

\usepackage{listings}
\lstdefinelanguage{Monte}
{
  morekeywords={
    [2]as,bind,def,else,escape,[2]exit,[2]extends,[2]guards,[2]implements,
    [2]in,[2]method,pass,var,via,
    exports,import,
    fn,interface,object,[2]to,
    catch,if,finally,for,[2]match,switch,try,when,while,
    break,continue,return},
  sensitive=false,
  morestring=[b]',
  morestring=[b]",
  morecomment=[l]{\#}
}
\lstset{language=Monte}

\newcommand{\df}{ DeepFrozen }
\end_preamble
\use_default_options true
\begin_modules
theorems-ams
eqs-within-sections
figs-within-sections
logicalmkup
\end_modules
\maintain_unincluded_children false
\language english
\language_package default
\inputencoding auto
\fontencoding global
\font_roman "default" "Liberation Serif"
\font_sans "default" "default"
\font_typewriter "default" "default"
\font_math "auto" "auto"
\font_default_family default
\use_non_tex_fonts true
\font_sc false
\font_osf false
\font_sf_scale 100 100
\font_tt_scale 100 100
\graphics default
\default_output_format default
\output_sync 0
\bibtex_command default
\index_command default
\paperfontsize default
\spacing single
\use_hyperref false
\papersize default
\use_geometry false
\use_package amsmath 1
\use_package amssymb 1
\use_package cancel 1
\use_package esint 1
\use_package mathdots 1
\use_package mathtools 1
\use_package mhchem 1
\use_package stackrel 1
\use_package stmaryrd 1
\use_package undertilde 1
\cite_engine basic
\cite_engine_type default
\biblio_style plain
\use_bibtopic false
\use_indices false
\paperorientation portrait
\suppress_date false
\justification true
\use_refstyle 1
\index Index
\shortcut idx
\color #008000
\end_index
\secnumdepth 3
\tocdepth 3
\paragraph_separation indent
\paragraph_indentation default
\quotes_language english
\papercolumns 1
\papersides 1
\paperpagestyle default
\tracking_changes false
\output_changes false
\html_math_output 0
\html_css_as_file 0
\html_be_strict false
\end_header

\begin_body

\begin_layout Title
Monte: A Spiritual Successor to E
\end_layout

\begin_layout Author
Corbin Simpson
\end_layout

\begin_layout Abstract
We introduce Monte, a capability-safe programming language in the style
 of E and Python.
 We detail several of Monte's differences from E, including new syntax,
 several new interfaces, and a simple module model.
 In particular, we examine five features and their consequences for secure
 distributed computing: named arguments, iterators, modules, controllers,
 and sealed exceptions.
\end_layout

\begin_layout Section
Introduction
\end_layout

\begin_layout Standard
Monte is a programming language cast in the same mold as the E programming
 language.
 
\begin_inset CommandInset citation
LatexCommand cite
key "MarkMThesis"

\end_inset

 Like E, Monte is a capability-safe language which models capabilities as
 objects (the 
\begin_inset Quotes eld
\end_inset

object-capability
\begin_inset Quotes erd
\end_inset

 security model).
 Also like E, Monte expands from a rich sugared language, Full-Monte, to
 a strict subset, Kernel-Monte.
 In this paper, we will introduce several facets of Monte, including Kernel-Mont
e expansions and applications to secure distributed computing.
\end_layout

\begin_layout Subsection
Surface Syntax
\end_layout

\begin_layout Standard
\begin_inset listings
lstparams "float=hb,frame=lines"
inline false
status open

\begin_layout Plain Layout

\begin_inset Caption Standard

\begin_layout Plain Layout
A mint, the 
\begin_inset Quotes eld
\end_inset

hello world
\begin_inset Quotes erd
\end_inset

 of capability-safe languages.
\end_layout

\end_inset


\end_layout

\begin_layout Plain Layout

def makeMint():
\end_layout

\begin_layout Plain Layout

  def [sealer, unsealer] := makeBrandPair("mint")
\end_layout

\begin_layout Plain Layout

  return def mint.makePurse(var balance :(Int >= 0)):
\end_layout

\begin_layout Plain Layout

    def decr(amount :(0..balance)) :Void { balance -= amount }
\end_layout

\begin_layout Plain Layout

    return object purse:
\end_layout

\begin_layout Plain Layout

      to getBalance() :Int { return balance }
\end_layout

\begin_layout Plain Layout

      to sprout() { return mint.makePurse(0) }
\end_layout

\begin_layout Plain Layout

      to getDecr() { return sealer.seal(decr) }
\end_layout

\begin_layout Plain Layout

      to deposit(amount :(Int >= 0), src) :Void:
\end_layout

\begin_layout Plain Layout

        unsealer.unseal(src.getDecr())(amount)
\end_layout

\begin_layout Plain Layout

        balance += amount
\end_layout

\end_inset


\end_layout

\begin_layout Standard
We start with the 
\begin_inset Quotes eld
\end_inset

hello world
\begin_inset Quotes erd
\end_inset

 of capability-safe languages, the basic mint.
 For readers familiar with E, Monte will immediately be readable.
 The two largest differences are the use of the 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
object
\end_layout

\end_inset

 keyword instead of 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
def
\end_layout

\end_inset

 for object literals, and the allowance of Python-style colons instead of
 braces for delimiting blocks.
 Additionally, other minor enhancements are on display in this example.
 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
def mint.makePurse(balance) { \SpecialChar ldots
 }
\end_layout

\end_inset

 is shorthand for 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
object mint { to makePurse(balance) { \SpecialChar ldots
 } }
\end_layout

\end_inset

, defining a single-method object.
 The Monte manual, available at 
\begin_inset CommandInset citation
LatexCommand cite
key "Monte"

\end_inset

, may be helpful.
\end_layout

\begin_layout Section
Named Arguments
\end_layout

\begin_layout Standard
In addition to positional arguments, Monte supports passing arguments keyed
 by name, which come after positional arguments.
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

def f(x, y, "key" => value):
\end_layout

\begin_layout Plain Layout

  return value
\end_layout

\end_inset


\end_layout

\begin_layout Standard
Keys are usually strings, and the syntax admits them as a special case,
 allowing 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
=> argumentName
\end_layout

\end_inset

 in place of 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
\begin_inset Quotes eld
\end_inset

argumentName
\begin_inset Quotes erd
\end_inset

 => argumentName
\end_layout

\end_inset

.
 The same syntax is used for both callers and receivers.
\end_layout

\begin_layout Standard
Default values and guards are supported as well, so that callers can optionally
 omit passing certain named arguments:
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

def adjustAndPad(adjustment, => padding :Str := " "):
\end_layout

\begin_layout Plain Layout

    adjust(adjustment)
\end_layout

\begin_layout Plain Layout

    pad(padding)
\end_layout

\end_inset


\end_layout

\begin_layout Standard
\begin_inset listings
lstparams "float=hb,frame=lines"
inline false
status collapsed

\begin_layout Plain Layout

\begin_inset Caption Standard

\begin_layout Plain Layout
Making rectangles with named arguments.
\end_layout

\end_inset

def makeRectangle(=> width :Int, => height :Int):
\end_layout

\begin_layout Plain Layout

    return object rectangle:
\end_layout

\begin_layout Plain Layout

        to getWidth() :Int:
\end_layout

\begin_layout Plain Layout

            return width
\end_layout

\begin_layout Plain Layout

        to getHeight() :Int:
\end_layout

\begin_layout Plain Layout

            return height
\end_layout

\begin_layout Plain Layout

        to getArea() :Int:
\end_layout

\begin_layout Plain Layout

            return width * height
\end_layout

\begin_layout Plain Layout

def width := 5
\end_layout

\begin_layout Plain Layout

def height := 7
\end_layout

\begin_layout Plain Layout

def rect1 := makeRectangle("width" => width, "height" => height)
\end_layout

\begin_layout Plain Layout

def rect2 := makeRectangle(=> width, => height)
\end_layout

\end_inset


\end_layout

\begin_layout Subsection
Semantics
\end_layout

\begin_layout Standard
Under the hood, Monte accommodates all of this functionality with a relatively
 small change of semantics.
 In E, a message always conforms to 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
[verb :Str, args :List]
\end_layout

\end_inset

.
 However, in Monte, a message conforms to 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
[verb :Str, args :List, namedArgs :Map]
\end_layout

\end_inset

, with a map of named arguments.
 When a method is called, after unifying all of the positional arguments,
 the named arguments are extracted and unified one-by-one.
\end_layout

\begin_layout Subsection
Optional Named Arguments
\end_layout

\begin_layout Standard
Crucially, any named arguments which are passed but not used by the receiving
 object are discarded.
 Callers may use this fact to pass optional named arguments which may or
 may not be used by the receiver.
\end_layout

\begin_layout Standard
Since named arguments can be optional both for callers and receivers, named
 arguments can be used to ease compatibility concerns when upgrading module
 code or object versions.
\end_layout

\begin_layout Subsection
Locked Methods
\end_layout

\begin_layout Standard
The named-argument keys can be arbitrary objects.
 Indeed, consider what happens when a closely-held object is used as a key:
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

object sesame {}
\end_layout

\begin_layout Plain Layout

object riches {}
\end_layout

\begin_layout Plain Layout

def cave((sesame) => _):
\end_layout

\begin_layout Plain Layout

    return riches
\end_layout

\end_inset


\end_layout

\begin_layout Standard
This function can only be called when the caller passes the right key, and
 otherwise it will not perform any effects in the method body.
 Since the key is passed as a named argument, it won't interfere with any
 other arguments.
 Therefore, we can apply this pattern to any method.
 We call this the 
\begin_inset Quotes eld
\end_inset

locked method
\begin_inset Quotes erd
\end_inset

 pattern since the method's named parameter is like a lock to which the
 key is applied.
\end_layout

\begin_layout Standard
Locked methods are largely equivalent in functionality to sealed dispatch,
 where a brand is passed to the 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
._sealedDispatch/1
\end_layout

\end_inset

 Miranda method.
 
\begin_inset CommandInset citation
LatexCommand cite
key "MonteMiranda"

\end_inset

 However, there are key differences that hint at different use cases, and
 in general, we do not recommend ever using locked methods in favor of sealed
 dispatch.
 We document the technique here for completeness only.
\end_layout

\begin_layout Subsection
Miranda FAIL
\end_layout

\begin_layout Standard
Monte grants one Miranda named argument to all calls.
 The 
\begin_inset Quotes eld
\end_inset

FAIL
\begin_inset Quotes erd
\end_inset

 named argument is a callable which takes a single value and aborts the
 computation.
 In a turn without a resolver, it is equivalent to 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
throw.run
\end_layout

\end_inset

, but if there is a resolver 
\begin_inset Formula $r$
\end_inset

, then it is equivalent to 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
r.smash
\end_layout

\end_inset

.
 The purpose of 
\begin_inset Quotes eld
\end_inset

FAIL
\begin_inset Quotes erd
\end_inset

 is to ease the effort required to write code which both can error and is
 often called from both immediate and asynchronous contexts.
\end_layout

\begin_layout Section
Iterators
\end_layout

\begin_layout Standard
E has internal iteration, where collections are passed a loop body and iterate
 by calling the loop body.
 Monte has external iteration and explicit iterator objects instead.
\end_layout

\begin_layout Standard
\begin_inset listings
lstparams "float=hb,frame=lines"
inline false
status collapsed

\begin_layout Plain Layout

\begin_inset Caption Standard

\begin_layout Plain Layout
\begin_inset Flex Code
status open

\begin_layout Plain Layout
zip()
\end_layout

\end_inset

 via composition of iterators.
\end_layout

\end_inset

def zip(left, right) as DeepFrozen:
\end_layout

\begin_layout Plain Layout

  return def zipper._makeIterator():
\end_layout

\begin_layout Plain Layout

    def l := left._makeIterator()
\end_layout

\begin_layout Plain Layout

    def r := right._makeIterator()
\end_layout

\begin_layout Plain Layout

    var counter := 0
\end_layout

\begin_layout Plain Layout

    return def iterator.next(ej):
\end_layout

\begin_layout Plain Layout

      def rv := [counter, [l(ej), r(ej)]]
\end_layout

\begin_layout Plain Layout

      counter += 1
\end_layout

\begin_layout Plain Layout

      return rv
\end_layout

\end_inset


\end_layout

\begin_layout Subsection
Rationale
\end_layout

\begin_layout Standard
Compared to internal iteration, external iteration with iterators offers
 several concrete benefits to Monte's design:
\end_layout

\begin_layout Itemize
Iterators only take one user-provided callable in their entire API, and
 that callable should be an ejector.
 (An idiomatic iterator will use 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
throw.eject/2
\end_layout

\end_inset

 to fire the ejector, ensuring that the callable cannot fool the iterator.)
 Instead of passing loop bodies to potentially untrusted collections, users
 can now be confident that an iterator can, at worst, loop forever.
 As a result, the expansion to Kernel-Monte does not have to generate defensive
 assertions in for-loops and while-loops to prevent the loop bodies from
 being stolen by malicious collections, as in E.
\end_layout

\begin_layout Itemize
An iterator is slightly more attenuated, in terms of authority, than its
 corresponding list of pairs.
 While a list can be examined many times, an iterator can only be consumed
 once in a linear fashion.
 Additionally, non-list collections can be iterable, allowing automatic
 attenuation from iterables to iterators.
\end_layout

\begin_layout Itemize
Iterators intrinsically permit pausing iteration.
 In particular, since iterators must complete their computation within a
 single turn, concurrency-aware patterns like asynchronously iterating over
 one item per turn are collection-independent and require no special container
 code.
 This means that iterators can represent partially-done computations which
 would be too expensive to consume in a single turn.
 For example, Monte Kanren logic programs can be turned into iterables and
 run incrementally.
 The Monte parser and lexer use iterables to incrementally parse Monte source
 code.
\end_layout

\begin_layout Itemize
Composition of iterators is relatively easy; a limited version of the classic
 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
zip()
\end_layout

\end_inset

 function can be written in fewer than ten lines.
 A complete version of 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
zip()
\end_layout

\end_inset

 can be found in the Typhon 
\begin_inset Quotes eld
\end_inset

lib/iterators
\begin_inset Quotes erd
\end_inset

 module.
 
\begin_inset CommandInset citation
LatexCommand cite
key "TyphonLibIterators"

\end_inset

 This version allows arbitrary numbers of arguments and has configurable
 support for iterables of unequal (
\begin_inset Quotes eld
\end_inset

ragged
\begin_inset Quotes erd
\end_inset

) length.
\end_layout

\begin_layout Subsection
Interface
\end_layout

\begin_layout Standard
The iterator protocol consists of just one method, 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
.next/1
\end_layout

\end_inset

, which accepts an ejector and either returns a pair of values or ejects.
 There is also an iterable protocol, similar to Python's iterable protocol,
 
\begin_inset CommandInset citation
LatexCommand cite
key "PythonIterable"

\end_inset

 consisting of another single method, 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
._makeIterator/0
\end_layout

\end_inset

, which merely makes iterators:
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

def counter._makeIterator():
\end_layout

\begin_layout Plain Layout

    var i :Int := 0
\end_layout

\begin_layout Plain Layout

    return object iterator.next(_ej):
\end_layout

\begin_layout Plain Layout

        def rv := [i, i]
\end_layout

\begin_layout Plain Layout

        i += 1
\end_layout

\begin_layout Plain Layout

        return rv
\end_layout

\end_inset


\end_layout

\begin_layout Standard
These two methods are the entirety of the iterator API.
\end_layout

\begin_layout Standard
Iteration always proceeds over pairs.
 The first element of the pair is usually a key or index, while the second
 element is a keyed value or datum.
 Iteration over lists yields pairs of indices and values, like Python's
 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
enumerate()
\end_layout

\end_inset

.
 Iteration over maps yields key-value pairs.
\end_layout

\begin_layout Subsection
Integrating Iterators
\end_layout

\begin_layout Standard
Monte syntax uses iterators in the same places where E would use internal
 iteration.
 Under the hood, for-loops and while-loops use iterators with the help of
 the 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
_loop()
\end_layout

\end_inset

 combinator.
\end_layout

\begin_layout Standard
We can recover classic mapping-and-filtering behavior with list comprehension
 syntax.
 For example, to make a list of odd integers from 0 to 20:
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

[for i in (0..!20) ? (i % 2 == 1) i]
\end_layout

\end_inset


\end_layout

\begin_layout Standard
Here, the 
\begin_inset Quotes eld
\end_inset

?
\begin_inset Quotes erd
\end_inset

 should be read as 
\begin_inset Quotes eld
\end_inset

such-that
\begin_inset Quotes erd
\end_inset

, just like in such-that patterns, and performs a filtering operation, skipping
 iterations where the such-that condition fails.
\end_layout

\begin_layout Section
Modules
\end_layout

\begin_layout Standard
A Monte module is both a compilation unit and a composable code unit.
 We replace E URI-getters and maker files with a uniform module interface.
\end_layout

\begin_layout Subsection
Imports & Exports
\end_layout

\begin_layout Standard
At the highest level, a module is a source file with a header which indicates
 the exports and imports of the module.
 After compilation, the module can be given a name and composed with other
 modules by piping exports to imports.
 The composition is performed by a module loader, which is a plain Monte
 expression empowered to load code objects.
\end_layout

\begin_layout Standard
Module syntax is relatively light.
 Here is a complete, if facetious, module which imports from 
\begin_inset Quotes eld
\end_inset

lib/iterators
\begin_inset Quotes erd
\end_inset

 and exports a single named value, 
\begin_inset Quotes eld
\end_inset

zipSum
\begin_inset Quotes erd
\end_inset

:
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

import "lib/iterators" =~ [=> zip :DeepFrozen]
\end_layout

\begin_layout Plain Layout

exports (zipSum)
\end_layout

\begin_layout Plain Layout

\end_layout

\begin_layout Plain Layout

def zipSum(left :List, right :List) :List as DeepFrozen:
\end_layout

\begin_layout Plain Layout

  return [for [l, r] in (zip(left, right)) l + r]
\end_layout

\end_inset


\end_layout

\begin_layout Standard
Expanding only the module syntax, the structure of a module is revealed
 to be a single anonymous object:
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

object _ as DeepFrozen:
\end_layout

\begin_layout Plain Layout

  to dependencies() :List[Str]:
\end_layout

\begin_layout Plain Layout

    return ["lib/iterators"]
\end_layout

\begin_layout Plain Layout

  to run(package) :Map[Str, DeepFrozen]:
\end_layout

\begin_layout Plain Layout

    def [=> zip :DeepFrozen] | _ := package."import"("lib/iterators")
\end_layout

\begin_layout Plain Layout

    def zipSum(left :List, right :List) :List as DeepFrozen:
\end_layout

\begin_layout Plain Layout

      return [for [l, r] in (zip(left, right)) l + r]
\end_layout

\begin_layout Plain Layout

    return [=> zipSum]
\end_layout

\end_inset


\end_layout

\begin_layout Standard
While arbitrary patterns are allowed in imports, we encourage a convention
 of map-patterns.
 Notice that we expand the import map-pattern 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
[=> zip :DeepFrozen]
\end_layout

\end_inset

 into 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
[=> zip :DeepFrozen] | _
\end_layout

\end_inset

, which is a convenience that both allows users to import only needed names
 and also allows for modules to add new exports without breaking users,
 making it easier to expand a module's interface without breaking compatibility.
 This is analogous to our usage of named arguments to allow optional names
 in calls.
\end_layout

\begin_layout Subsection
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
df
\end_layout

\end_inset

 Exports
\end_layout

\begin_layout Standard
In Monte, module exports must conform to 
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
df
\end_layout

\end_inset

.
 This constraint forces modules to do any impure or mutable computation
 prior to freezing and returning exported values.
\end_layout

\begin_layout Standard
There are several boons to the 
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
df
\end_layout

\end_inset

 requirement.
 Like E makers, Monte modules can be cached and composed.
 Module composition proceeds with the assistance of a module loader, which
 is a short routine that loads modules and incrementally executes them,
 routing exports to imports.
\end_layout

\begin_layout Standard
There are some difficulties, too.
 In particular, imported names usually must be guarded by 
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
df
\end_layout

\end_inset

.
 The only common exception is importing from the special 
\begin_inset Quotes eld
\end_inset

unittest
\begin_inset Quotes erd
\end_inset

 name, which produces an effect on import in order to run unit tests.
 Such impure effects executed on import don't alter the module formalism
 at all, just the implementation of the module loader.
 The impurity of the loader also lets us cache and reuse modules as plain
 objects, so that modules which occur often in the module dependency graph
 can be reused.
\end_layout

\begin_layout Subsection
Entrypoints
\end_layout

\begin_layout Standard
To replace E's URI getters, we instead designate the exported name 
\begin_inset Quotes eld
\end_inset

main
\begin_inset Quotes erd
\end_inset

 as an entrypoint for modules.
 To run an entrypoint, we call it with a message 
\begin_inset Flex Code
status open

\begin_layout Plain Layout

\family typewriter
[“run”, [argv :List[Str]], unsafeScope :Map]
\end_layout

\end_inset

, expecting a 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
Vow[Int]
\end_layout

\end_inset

 in return.
 The return value and list of arguments parallel the classic inputs and
 outputs to an OS process, while the unsafe scope consists of all of the
 primitive powers which the loader is willing to grant to the program at
 large.
\end_layout

\begin_layout Standard
This interface permits easy examination of coarse OS-level capabilities
 during code review, akin to the OpenBSD 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
pledge()
\end_layout

\end_inset

 syscall.
 
\begin_inset CommandInset citation
LatexCommand cite
key "pledge2"

\end_inset

 Consider the following entrypoint, from a real-world IRC client:
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

def main(argv :List[Str],
\end_layout

\begin_layout Plain Layout

         => Timer,
\end_layout

\begin_layout Plain Layout

         => currentRuntime,
\end_layout

\begin_layout Plain Layout

         => getAddrInfo,
\end_layout

\begin_layout Plain Layout

         => makeFileResource,
\end_layout

\begin_layout Plain Layout

         => makeTCP4ClientEndpoint,
\end_layout

\begin_layout Plain Layout

         => unsealException) :Vow[Int] as DeepFrozen:
\end_layout

\begin_layout Plain Layout

  …
\end_layout

\begin_layout Plain Layout

  return 0
\end_layout

\end_inset


\end_layout

\begin_layout Standard
We can consider the broad capabilities of this program entirely by considering
 its unsafe named arguments in the entrypoint.
 As we do so, we can imagine a code reviewer's rationale for each name:
\end_layout

\begin_layout Description
Timer It can read the system clock and measure time taken during vat turns.
 This is needed to provide a wall-clock IRC message throttle, so that messages
 aren't lost and the bot isn't kicked.
\end_layout

\begin_layout Description
currentRuntime It can access various runtime-specific capabilities.
 This object is meant for staging non-standard platform-specific functionality.
 In this particular case, Typhon exports a non-standard cryptographic interface
 based on libsodium 
\begin_inset CommandInset citation
LatexCommand cite
key "Sodium"

\end_inset

 via 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
currentRuntime.getCrypt()
\end_layout

\end_inset

.
 This is needed for cryptography services.
\end_layout

\begin_layout Description
getAddrInfo It can resolve hostnames using the system DNS configuration.
 This is needed to find IRC server addresses.
\end_layout

\begin_layout Description
makeFileResource It can read and write to the filesystem.
 This is needed for storing to-do lists.
\end_layout

\begin_layout Description
makeTCP4ClientEndpoint It can create TCP/IPv4 outgoing connections.
 This is needed to connect to IRC.
\end_layout

\begin_layout Description
unsealException It can examine exceptions caught by try-expressions.
 This is needed for REPL functionality.
\end_layout

\begin_layout Standard
Most of these unsafe powers have been well-studied, although we highlight
 the interesting case of 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
unsealException
\end_layout

\end_inset

 and will discuss it more later.
\end_layout

\begin_layout Standard
In addition to the unsafe named parameters, an entrypoint is also passed
 a list of input strings and should return an integer indicating success
 or otherwise, as is traditional.
 One change from tradition, however, is the ability to return a promise
 for an integer instead.
 This enables an entrypoint to implicitly indicate that it has more turns
 pending before it will be finished running.
 This design is based on Twisted Python's 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
twisted.internet.task.react()
\end_layout

\end_inset

 helper, which was designed to make it easier to produce Twisted-compatible
 entrypoints.
 
\begin_inset CommandInset citation
LatexCommand cite
key "TwistedInternetTaskReact"

\end_inset


\end_layout

\begin_layout Section
Controllers
\end_layout

\begin_layout Standard
We have discovered some use cases for the experimental 
\begin_inset Quotes eld
\end_inset

lambda-args
\begin_inset Quotes erd
\end_inset

 syntax suggested for E.
 In particular, we have found that computations which carry an implicit
 context or effect can be well-modeled with the syntax, and so we have adapted
 it for Monte, dubbing this syntax the controller interface.
\end_layout

\begin_layout Subsection
Introduction
\end_layout

\begin_layout Standard
A controller is a 
\begin_inset ERT
status open

\begin_layout Plain Layout


\backslash
df
\end_layout

\end_inset

 object which can build a plan incrementally from small program fragments
 and instructions.
 The plan is encoded syntactically.
 A listing is worth a thousand words.
 Here is a controller in Full-Monte:
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

controller (in0, …, ini) do arg0, …, argj { action() }
\end_layout

\end_inset


\end_layout

\begin_layout Standard
And the same controller, with only controller syntax desugared:
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

(controller :DeepFrozen).control("do", i, j, fn {
\end_layout

\begin_layout Plain Layout

  [[in0, …, ini], fn param0, …, paramj, ej {
\end_layout

\begin_layout Plain Layout

    def [arg0, …, argj] exit ej := [param0, …, paramj]
\end_layout

\begin_layout Plain Layout

    action()
\end_layout

\begin_layout Plain Layout

  }]
\end_layout

\begin_layout Plain Layout

}).controlRun()
\end_layout

\end_inset


\end_layout

\begin_layout Standard
This controller receives a single command, consisting of an instruction
 
\begin_inset Quotes eld
\end_inset

do
\begin_inset Quotes erd
\end_inset

, an arity 
\begin_inset Formula $i$
\end_inset

 of inputs 
\begin_inset Formula $[\text{in}_{0},\text{in}_{1},\dots,\text{in}_{i}]$
\end_inset

, an arity 
\begin_inset Formula $j$
\end_inset

 of arguments 
\begin_inset Formula $[\text{arg}_{0},\text{arg}_{1},\dots,\text{arg}_{j}]$
\end_inset

, and a thunk known as the block.
 When called, the block returns a pair containing a list of all 
\begin_inset Formula $i$
\end_inset

 inputs and another thunk, known as the lambda.
 The lambda is the user-provided part of the plan; when called, it will
 take in 
\begin_inset Formula $j$
\end_inset

 parameters and run the user-specified action.
 The controller is expected to generate a plan based on the contents of
 the block; the plan will probably call the block, extract the inputs, pass
 the inputs to the lambda, and return the lambda's return value.
 Since the block and lambda are both thunks, they may be called zero-or-more
 times based on the design of the controller.
\end_layout

\begin_layout Subsection
Monads
\end_layout

\begin_layout Standard
Monadic actions can be fully captured by controllers.
 Compare and contrast the following Haskell:
\end_layout

\begin_layout Standard
\begin_inset listings
lstparams "language=Haskell"
inline false
status open

\begin_layout Plain Layout

return 42 >>= 
\backslash
x -> do {
\end_layout

\begin_layout Plain Layout

  return $ x + 1
\end_layout

\begin_layout Plain Layout

} >>= 
\backslash
x -> do {
\end_layout

\begin_layout Plain Layout

  return $ x * 2
\end_layout

\begin_layout Plain Layout

}
\end_layout

\end_inset


\end_layout

\begin_layout Standard
With the following Monte:
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

m (m.unit(42)) do x {
\end_layout

\begin_layout Plain Layout

  m.unit(x + 1)
\end_layout

\begin_layout Plain Layout

} lift x {
\end_layout

\begin_layout Plain Layout

  x * 2
\end_layout

\begin_layout Plain Layout

}
\end_layout

\end_inset


\end_layout

\begin_layout Standard
We must pass our monad controller 
\begin_inset Formula $m$
\end_inset

 since we have neither implicit parameters nor typeclasses.
 The 
\begin_inset Quotes eld
\end_inset

do
\begin_inset Quotes erd
\end_inset

 instruction takes some values extracted from the monadic context and returns
 a monadic action.
 The 
\begin_inset Quotes eld
\end_inset

lift
\begin_inset Quotes erd
\end_inset

 instruction is similar, but performs an automatic unit wrapping to return
 to the monadic context.
\end_layout

\begin_layout Subsection
Kanren
\end_layout

\begin_layout Standard
Logic programming can be difficult without a domain-specific language.
 The Kanren family, including miniKanren and µKanren, is a popular choice
 for embedding logic programming into general-purpose languages.
 
\begin_inset CommandInset citation
LatexCommand cite
key "Kanren,friedman2005the"

\end_inset


\end_layout

\begin_layout Standard
We can construct a Kanren program from a controller.
 This short logic program creates two logic variables, 
\begin_inset Formula $x$
\end_inset

 and 
\begin_inset Formula $y$
\end_inset

, and asserts that 
\begin_inset Formula $x\equiv\text{true}\land x\equiv y$
\end_inset

:
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

kanren () exists x, y {
\end_layout

\begin_layout Plain Layout

  kanren.unify(x, true)
\end_layout

\begin_layout Plain Layout

  kanren.unify(x, y)
\end_layout

\begin_layout Plain Layout

}
\end_layout

\end_inset


\end_layout

\begin_layout Standard
When values are extracted from this program, there will be one satisfying
 assignment, where both 
\begin_inset Formula $x$
\end_inset

 and 
\begin_inset Formula $y$
\end_inset

 are assigned 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
true
\end_layout

\end_inset

.
\end_layout

\begin_layout Standard
While the 
\begin_inset Quotes eld
\end_inset

exists
\begin_inset Quotes erd
\end_inset

 instruction might be the main workhorse for program fragments, our Kanren
 controller is also capable of composing logic programs.
 In this example from real-world code, we compose many fragments of logic
 at the edges of a sheaf into a single coherent assignment, using the 
\begin_inset Quotes eld
\end_inset

forAll
\begin_inset Quotes erd
\end_inset

 instruction to unify a list of logic variables:
\end_layout

\begin_layout Standard
\begin_inset listings
inline false
status open

\begin_layout Plain Layout

kanren (fullSection) forAll v, value {
\end_layout

\begin_layout Plain Layout

  kanren.unify(vars[index[v]], value)                
\end_layout

\begin_layout Plain Layout

} (consistency) forAll vs, goalMaker {
\end_layout

\begin_layout Plain Layout

  def swizzle := [for v in (vs) vars[index[v]]]             
\end_layout

\begin_layout Plain Layout

  M.call(goalMaker, "run", swizzle, [].asMap())
\end_layout

\begin_layout Plain Layout

}
\end_layout

\end_inset


\end_layout

\begin_layout Section
Sealed Exceptions
\end_layout

\begin_layout Standard
Monte exceptions are easily thrown.
 Any object may become an exception by being passed to 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
throw.run/1
\end_layout

\end_inset

.
 However, catching an exception does not grant the catcher a reference to
 the originally-thrown object.
 Instead, the catcher receives a sealed exception which is opaque.
\end_layout

\begin_layout Standard
This asymmetry leads to two distinct tools for non-local control flow.
 The first tool is the escape-expression.
 An escape-expression introduces an ejector, and computation may be aborted
 by firing the ejector.
 In this way, an escape-expression syntactically indicates where and when
 control flow will resume, and who gets the result of the inner computation;
 control flow resumes at the end of the escape-expression and the result
 is passed to the catcher.
 The code which holds the escape-expression gets to manage the computation
 inside of it, and none of the intervening code may catch or otherwise interfere
 with the ejection.
\end_layout

\begin_layout Standard
Now, examining exceptions, we would expect that try-expressions fill the
 same role as escape-expressions.
 However, a try-expression does not grant direct access to any caught exceptions
, because they are sealed.
 So, who gets the result instead? In general, we say that the result should
 be delivered to the caller who caused the current turn, and not to any
 intervening code inside the turn.
\end_layout

\begin_layout Standard
There are several ways to unseal exceptions.
 Exceptions which reach the end of a turn are unsealed and used to smash
 the turn's resolver, generating either a broken promise in a subsequent
 turn, or an exception in the runtime debug log.
 An exception can be logged in the debug log with the convenience method
 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
traceln.exception/1
\end_layout

\end_inset

, which logs both the exception and its call stack.
 And, finally, the unsafe scope contains 
\begin_inset Flex Code
status open

\begin_layout Plain Layout
unsealException
\end_layout

\end_inset

, for cases when an exception must be unsealed for display.
\end_layout

\begin_layout Section
Conclusion
\end_layout

\begin_layout Standard
We have only skimmed the surface of Monte, but we have demonstrated several
 interesting facets of its capability-security design.
\end_layout

\begin_layout Subsection
Future Directions
\end_layout

\begin_layout Itemize
Controllers could be extended in several directions.
 Possibilities include asynchronous or promise-aware variants of current
 loop syntax, monad comprehensions, 
\begin_inset CommandInset citation
LatexCommand cite
key "Giorgidze11bringingback"

\end_inset

 LINQ-style queries, and comonadic (
\begin_inset Quotes eld
\end_inset

codo
\begin_inset Quotes erd
\end_inset

) syntax.
 
\begin_inset CommandInset citation
LatexCommand cite
key "Orchard_anotation"

\end_inset


\end_layout

\begin_layout Itemize
Work is ongoing to produce a 
\begin_inset Quotes eld
\end_inset

lib/iterators
\begin_inset Quotes erd
\end_inset

 library with useful combinators for iterators, with inspiration from the
 Python 
\begin_inset Quotes eld
\end_inset

itertools
\begin_inset Quotes erd
\end_inset

 library.
 
\begin_inset CommandInset citation
LatexCommand cite
key "PythonItertools"

\end_inset


\end_layout

\begin_layout Itemize
Research into ways to manipulate modules is also ongoing.
 In particular, it may be possible to make a 
\begin_inset Quotes eld
\end_inset

muffin
\begin_inset Quotes erd
\end_inset

 module, where subordinate modules have been statically bundled with an
 entrypoint to create a monolithic program.
\end_layout

\begin_layout Itemize
The Monte language and standard library continue to evolve as our contributors
 explore their own interests.
 Several contributors have started building alternative runtimes for Monte.
 We are considering including support for modern capability-relevant technologie
s like Cap'n Proto 
\begin_inset CommandInset citation
LatexCommand cite
key "CapnProto"

\end_inset

 and Named Data Networking 
\begin_inset CommandInset citation
LatexCommand cite
key "NDN"

\end_inset

 as standard library modules.
 Community members have suggested auditors for enforcing algebraic properties,
 or for enforcing the correctness of primitive recursive arithmetic.
\end_layout

\begin_layout Subsection
Acknowledgments
\end_layout

\begin_layout Standard
We thank the Monte community at large for many helpful comments made while
 this paper was being drafted.
 We also thank the original creators of E for motivating our work.
 Finally, we thank W.
 Allen Short for being the other author of Monte, and Emily Dunham for convincin
g us to write and submit this paper.
\end_layout

\begin_layout Standard
\begin_inset CommandInset bibtex
LatexCommand bibtex
bibfiles "corbin-ocap17-monte"
options "plain"

\end_inset


\end_layout

\end_body
\end_document