Marshall with partiality, nondeterminism, and pattern matching

This modified version of the Marshall programming language accompanies the paper the LICS 2018 paper "Computable decision-making on the reals and other spaces via partiality and nondeterminism" by Benjamin Sherman, Luke Sciarappa, Michael Carbin, and Adam Chlipala. The two example Marshall programs from the paper are found in examples/car_LICS.asd and examples/roots_LICS.asd. To use these libraries, run

#use "examples/car_LICS.asd";;
#use "examples/roots_LICS.asd";;

in the Marshall interpreter.

Marshall

Marshall is a programming language for exact real arithmetic based on ideas from Abstract Stone Duality (ASD) and the construction of the Dedekind reals in ASD. See also Andrej Bauer's talk on Efficient computations with Dedekind reals.

The main idea of Marshall is that a real number x is given as a Dedekind cut, i.e., as a pair of predicates describing which numbers are smaller than x and which ones larger. For example, the sqrt function is defined in Marshall as

let sqrt =
  fun a : real =>
    cut x
      left  (x < 0 \/ x * x < a)
      right (x > 0 /\ x * x > a)

See example.asd for more examples.

Prerequisites

To compile Marshall you will need Ocaml, version 3.12 and the menhir parser generator.

Both are available through standard packaging systems on Linux distributions, and on MacOS X via opam. On Windows you might get away with Wodi -- we wish you good luck.

If you install the rlwrap or ledit command-line editing wrappers, Marshall will use them automatically in the interactive mode.

Compilation

Compilation should run smoothly or not at all. Type

./configure
make

The configure command accepts standard autoconf options, see configure --help. The compiled executable is called marshall and you can run it in place.

Installation

To install Marshall type

make install

This will install the Marshall exectuable in /usr/local/bin unless you specified a different location with configure. You do not actually have to install Marshall to run it.

Examples

There are examples in the example subdirectory. It may be instructive to look at prelude.asd.

A small Haskell implementation

In etc/haskell you can find a small Haskell implementation of real numbers that somewhat follows the ideas of Marshall. It was implemented as part of a graduate course on computable topology in 2009 at the Faculty of Computer Science and Informatics, University of Ljubljana. Of particular help might be the notes etc/haskell/notes.tex.

Compiling with MPFR

In theory Marshall can be compiled with the MPFR library, but this requires extra work. At the moment MPFR is not used by autoconf. Here are some obsolete instruction that may or may not work.

0. You need the prerequisites listed above.

1. You need the usual building tools, such as subversion, make, and gcc. Under Microsoft Windows you can get those by installing Cygwin.

2. You need camlidl, which is available in GODI as well.

3. You need MPFR, or through your package manager.

4. You need mlgmpidl. You should get the latest subversion version which includes some patches that we submitted. Check out mlgmpidl from subversion:

   svn checkout svn://scm.gforge.inria.fr/svn/mlxxxidl/mlgmpidl

(Just in case, this repostitory includes the patch in mpfr.idl.patch. But you should not have to apply it if you get mlgmpidl from subversion.) Proceed with installation of mlgmpidl.

6. TODO How to "register" it with ocamlfind?

7. To compile the bytecode version with Mpfr library, type in the src subdirectory

   ocamlbuild -use-ocamlfind marshall_mpfr.byte

To compile bytecode, native, and the documentation, type in the src subdirectory

ocamlbuild -use-ocamlfind all.otarget