Please use this identifier to cite or link to this item: doi:10.22028/D291-29878
Title: Non-reformist reform for Haskell Modularity
Author(s): Kilpatrick, Scott
Language: English
Year of Publication: 2019
Free key words: programming languages
type systems
modularity
Haskell
ML
module systems
DDC notations: 004 Computer science, internet
600 Technology
Publikation type: Doctoral Thesis
Abstract: In this thesis, I present Backpack, a new language for building separately-typecheckable packages on top of a weak module system like Haskell’s. The design of Backpack is the first to bring the rich world of type systems to the practical world of packages via mixin modules. It’s inspired by the MixML module calculus of Rossberg and Dreyer but by choosing practicality over expressivity Backpack both simplifies that semantics and supports a flexible notion of applicative instantiation. Moreover, this design is motivated less by foundational concerns and more by the practical concern of integration into Haskell. The result is a new approach to writing modular software at the scale of packages.
Modulsysteme wie die in Haskell erlauben nur eine weiche Art der Modularität, in dem Modulimplementierungen direkt von anderen Implementierungen abhängen und in dieser Abhängigkeitsreihenfolge verarbeitet werden müssen. Modulsysteme wie die in ML andererseits erlauben eine kräftige Art der Modularität, in dem explizite Schnittstellen Vermutungen über Abhängigkeiten ausdrücken und jeder Modultyp überprüft und unabhängig ergründet werden kann. In dieser Dissertation präsentiere ich Backpack, eine neue Sprache zur Entwicklung separattypenüberprüfbarer Pakete über einem weichen Modulsystem wie Haskells. Das Design von Backpack überführt erstmalig die reichhaltige Welt der Typsysteme in die praktische Welt der Pakete durch Mixin-Module. Es wird von der MixML-Kalkulation von Rossberg und Dreyer angeregt. Backpack vereinfacht allerdings diese Semantik durch die Auswahl von Anwendbarkeit statt Expressivität und fördert eine flexible Art von geeigneter Applicative- Instantiierung. Zudem wird dieses Design weniger von grundlegenden Anliegen als von dem praktischen Anliegen der Eingliederung in Haskell begründet. Die Semantik von Backpack wird durch die Ausarbeitung in Mengen von Haskell-Modulen und „binary interface files“ definiert, und zeigt so, wie Backpack Interoperabilität mit Haskell erhält, während Backpack es mit Schnittstellen nachrüstet. In meiner Formalisierung Backpacks präsentiere ich ein neuartiges Typsystem für Haskellmodule und überprüfe einen entscheidenen Korrektheitssatz, um die Semantik von Backpack zu validieren.
Link to this record: urn:nbn:de:bsz:291--ds-298780
hdl:20.500.11880/28396
http://dx.doi.org/10.22028/D291-29878
Advisor: Dreyer, Derek
Date of oral examination: 15-Oct-2019
Date of registration: 2-Dec-2019
Third-party funds sponsorship: Max Planck Institute for Software Systems (MPI-SWS)
Description of the related object: Homepage for the Backpack project
Related object: http://plv.mpi-sws.org/backpack/
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
kilpatrick-thesis-nov-2019-publication.pdfDissertation1,3 MBAdobe PDFView/Open


Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.