All Projects → TiarkRompf → Scala Escape

TiarkRompf / Scala Escape

Licence: bsd-3-clause
A compiler plug-in to control object lifetimes in Scala

Labels

Projects that are alternatives of or similar to Scala Escape

Ledgertheory
Stars: ✭ 12 (-80%)
Mutual labels:  coq
Paramcoq
Coq plugin for parametricity [[email protected]]
Stars: ✭ 32 (-46.67%)
Mutual labels:  coq
Poleiro
A blog about Coq
Stars: ✭ 42 (-30%)
Mutual labels:  coq
Hello World
A Hello World program in Coq.
Stars: ✭ 14 (-76.67%)
Mutual labels:  coq
Profunctor Monad
Bidirectional programming in Haskell with monadic profunctors
Stars: ✭ 30 (-50%)
Mutual labels:  coq
Parseque
Total Parser Combinators in Coq
Stars: ✭ 37 (-38.33%)
Mutual labels:  coq
Coqjvm
Coq executable semantics and resource verifier
Stars: ✭ 10 (-83.33%)
Mutual labels:  coq
Verlang
Stars: ✭ 52 (-13.33%)
Mutual labels:  coq
Nuprlincoq
Implementation of Nuprl's type theory in Coq
Stars: ✭ 31 (-48.33%)
Mutual labels:  coq
Pornview
Porn browser formally-verified in Coq
Stars: ✭ 42 (-30%)
Mutual labels:  coq
Vvclocks
Verified vector clocks, with Coq!
Stars: ✭ 14 (-76.67%)
Mutual labels:  coq
Hott
Homotopy type theory
Stars: ✭ 946 (+1476.67%)
Mutual labels:  coq
Certint
A Certified Interpreter for ML with Structural Polymorphism
Stars: ✭ 39 (-35%)
Mutual labels:  coq
Jt89
sn76489an compatible Verilog core, with emphasis on FPGA implementation and Megadrive/Master System compatibility
Stars: ✭ 14 (-76.67%)
Mutual labels:  coq
Metalib
The Penn Locally Nameless Metatheory Library
Stars: ✭ 47 (-21.67%)
Mutual labels:  coq
Stalin Sort
Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️
Stars: ✭ 868 (+1346.67%)
Mutual labels:  coq
Compcert
The CompCert formally-verified C compiler
Stars: ✭ 984 (+1540%)
Mutual labels:  coq
Perennial
Verifying concurrent crash-safe systems
Stars: ✭ 57 (-5%)
Mutual labels:  coq
Silveroak
Formal specification and verification of hardware, especially for security and privacy.
Stars: ✭ 51 (-15%)
Mutual labels:  coq
Freespec
A framework for implementing and certifying impure computations in Coq
Stars: ✭ 41 (-31.67%)
Mutual labels:  coq

2nd-Class Values with Bounded Lifetimes

First-class functions dramatically increase expressiveness, at the expense of static guarantees.

In ALGOL or PASCAL, functions could be passed as arguments but never escape their defining scope. Therefore, function arguments could serve as temporary access tokens or capabilities, enabling callees to perform some action, but only for the duration of the call.

In modern languages, such programming patterns are no longer available.

The central thrust of this work is to re-introduce second-class functions and other values alongside first-class entities in modern languages.

This Scala compiler plug-in exposes a programming model to enforce a no-escape policy for certain objects.

There are many potential uses:

  • Effects: Objects can serve as capabilities. But we must limit the scope of capabilities to retain control. Compare to Monads, which do not compose well.
  • Region based memory: Deallocate and/or reuse memory in a timely manner (note that we do not aim to do this for all allocations, just for big chunks).
  • Resource control: Ensure that resources such as file handles are properly closed.
  • Staging: Scope extrusion. We must limit the scope of binders to guarantee well-typed generated code.
  • Distributed systems: We do not want to serialize large data by accident (see Spores).

The key ideas for combining first- and second-class values in a single language are as follows:

  • First-class functions may not refer to second-class values through free variables
  • All functions must return first-class values, and only first-class values may be stored in object fields or mutable variables

Together, these rules ensure that second-class values never escape their defining scope.

More details are described in our OOPLA'16 paper:

The coq subdirectory contains mechanized proofs for the theorems in the paper.

We also provide a modified version of the Scala distribution, where higher-order functions in the standard library (especially collections) are annotated as second class where possible:

A High-Level Example

If a variable or function parameter is marked @local, it will be second-class, and thus it must not escape.

// For exception handling, we would like to enforce that
// exceptions can only be raised within a try/catch block.

def trycatch(f: @local (Exception => Nothing) => Unit): Unit

// The closure passed to trycatch may not leak its argument.

trycatch { raise =>
  raise(new Exception)  // ok: raise cannot escape
}

// Inside a try block we can use `raise` in safe positions,
// but not in unsafe ones, where it could be leaked.

def safeMethod(@local f: () => Any): Int
def unsafeMethod(f: () => Any): Int

trycatch { raise =>
  safeMethod { () =>
    raise(new Exception)  // ok: closure is safe
  }
  unsafeMethod { () =>
    raise(new Exception)  // not ok
  }
}

See the test suite for complete code.

Rationale and Background

The concept of higher-order and first-class language constructs goes hand in hand. In a higher-order language, many things are first-class: functions, mutable references, etc.

Being first-class means that there are no restrictions on how an object may be used. Functions can be passed to other functions as arguments and returned from other functions. First class reference cells may hold functions or other reference cells.

Lexical scope is central to most modern programming languages. First-class functions close over their defining scope. Hence they are also called closures.

While programming with first-class objects is incredibly useful, it is sometimes too powerful, and one loses some useful guarantees.

For example, in a language without closures, function calls follow a strict stack discipline. A local variable's lifetime ends when the function returns and its space can be reclaimed. Contrast this with higher-order languages, which allocate closure records on the heap. The lifetime of a variable may be indefinite if it is captured by a closure.

Binding the lifetime of (certain -- not all) objects is important. So maybe not all objects should be first class?

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].