Projekt

Zurück zur Übersicht

Effects as Implicit Capabilities

Titel Englisch Effects As Implicit Capabilites
Gesuchsteller/in Odersky Martin
Nummer 166154
Förderungsinstrument Projektförderung (Abt. I-III)
Forschungseinrichtung Laboratoire de méthodes de programmation 1 EPFL - IC - IIF - LAMP1
Hochschule EPF Lausanne - EPFL
Hauptdisziplin Informatik
Beginn/Ende 01.04.2016 - 31.03.2019
Bewilligter Betrag 631'548.00
Alle Daten anzeigen

Keywords (6)

Scala; type systems; effects; functional programming; implicit parameters; programming languages

Lay Summary (Deutsch)

Lead
Effects as Implicit CapaibilitiesMartin Odersky
Lay summary

 

Der Zweck eines Computer-Programms besteht darin, einen Effekt auf die Umgebung auszuüben, z.B. Pixel auf den Bildschirm zu zeichnen, einen Eintrag in einer Datenbank vorzunehmen, oder einen Roboter zu steuern. Wir reden auch von Effekten wenn eine Prozedur mit ihrer Umgebung auf andere Weise interagiert als einfach Argumente zu übernehmen und Resultate zurückzugeben.

Es scheint logisch, Effekte mit Hilfe einen statischen Typ-Disziplin zu modellieren, ähnlich wie das für FunktIons-Argumente und -Resultate gemacht wird. Um ein Programm als ganzes zu verstehen, sind schließlich die möglichen Effekte einer Prozedur mindestens genauso wichtig wie die Typen ihrer Argumente oder ihres Resultats. Allerdings wurde diese Idee sehr selten in der Praxis umgesetzt, obwohl mittlerweile über 30 Jahre an dem Thema geforscht wird. Das einzige weitverbreitete Beispiel wo Effekte statisch geprüft werden ist die Ausnahmebehandlung in Java. Aber diese Sprachkonstrukte werden weithin als wenig hilfreich betrachtet, und keine modernere Sprache hat sie kopiert. 

Wir werden einen neuen Ansatz zur Effekt-Prüfung erforschen, der die notationellen Schwierigkeiten bisheriger
Ansätze weitestgehend vermeidet. Die Kern-Idee ist, anstelle von Effekten von "Fähigkeiten" (englisch: "capabilities") zu sprechen. Fähigkeiten nehmen die Form von Werten eines speziellen Typs an. Solche Werte können an Funktionen übergeben werden und bilden somit Teil der Typsignatur einer Funktion.
 

 

Direktlink auf Lay Summary Letzte Aktualisierung: 14.06.2016

Verantw. Gesuchsteller/in und weitere Gesuchstellende

Mitarbeitende

Verbundene Projekte

Nummer Titel Start Förderungsinstrument
125199 Foundations of Scala 01.04.2009 Projektförderung (Abt. I-III)
124850 High-level concurrent programming with actors and transactions 01.04.2009 Projektförderung (Abt. I-III)

Abstract

The purpose of running a computer program is to have some effect onthe outside world -- paint pixels on a screen, enter a record in adatabase, control a robot, to give some examples. We also talk of aneffect if a procedure interacts with its environment in a waydifferent from just taking some arguments and producing aresult. Examples of such internal effects are updating or reading amutable store, or throwing an exception. In the presence ofeffects, order of evaluation matters; in fact that's how Sabry defineseffectfulness. Consequently, in order to understand aprogram that makes use of effects one must take its execution history intoaccount.It seems quite natural that one should track effects by means of astatic typing discipline, similarly to what is done for arguments andresults of functions. After all, the possible effects of a procedureare just as important as the types of its arguments and results inorder to understand the procedure's contract and how it can becomposed. However, despite 30 years of research on thesubject, very little of it has been applied in practice.We propose to investigate a new approach to effect checking that isfundamentally different from previous research. It promises to bequite usable in practice, and avoids in particular the notationaldifficulties of Java exceptions and monads.The central idea is that instead of talking about effects we talk aboutcapabilities. For instance, instead of saying a function ``throws anIOException'' we say that the function ``needs the capability to throwan IOException''. Capabilities are modelled as values of somecapability type. For instance, the abovementioned capability could bemodelled as a value of type `CanThrow[IOException]`. A function thatmight throw an `IOException` needs to have access to an instance ofthis type. Typically it takes an argument of the type as a parameter.At first glance, capabilities fit our definition of effects verywell. They generally form sets (order does not matter), and they canpropagate along the call graph by passing capabilities from the callerto the callee that needs them. What's more, capabilities followscoping rules. It suffices to have a capability somewhere in thecontext to be able to use it. This makes it possible to guard a wholeblock with a capability and avoids having to pass it to each use siteexplicitly. It turns out that this also gives a simple and naturalsolution to the problem of effect polymorphism. But there are twoareas where work is needed to make capabilities as effects sound andpractical.First, when implemented naively, capabilities as parameters are evenmore verbose than effect declarations such as throws clauses. Not onlydo they have to be declared, but they also have to be propagated asadditional arguments at each call site. We propose to make use of theconcept of implicit parameters to cut down on the boilerplate.Implicit parameters make call-site annotations unnecessary, but theystill have to be declared just like normal parameters. To avoidrepetition, we propose to investigate a way of abstracting implicitparameters into implicit function types.Second, there is one fundamental difference between the usual notionsof capabilities and effects: Capabilities can be captured inclosures. This means that a capability present at closure constructiontime can be preserved and accessed when the closure isapplied. Effects on the other hand, are temporal: it generally doesmake a difference whether an effect occurs when a closure isconstructed or when it is used. We propose to address this discrepancyby introducing a ``pure function'' type, instances of which are notallowed to close over effect capabilities.The proposed work will explore the idea of effects as capabilities indetail. We will work on minimal formalizations for implicit parametersand pure functions and study encodings of higher-level languageconstructs into these calculi. Based on the theoretical modelizationwe will develop a specification and implementation for adding effectsto Scala. A high-quality implementation in Scala will requireconsiderable effort, but will give an excellent means to validate theideas and promote them if they are deemed successful.As most languages, Scala currently does not track effects. So addingan effect system to the language raises the problem of migration. Howcan we add effects gradually to an existing codebase and libraryecosystem? How can we extend these technique to a multi-languageenvironment (noting that Scala runs on a host language such as Java orJavaScript, so ultimately effects in the host language are alsoeffects of the Scala program calling into it). Capabilities offer aunique advantage here: One can get started with a global``escape-hatch'' capability that allows arbitrary effects. As long asthis capability is in scope, code will type check as before. Themigration then consists in gradually reducing the scope of the escapehatch, thereby rendering code locally effect-safe.
-