Developing a type system for a configuration specification language

Abstract

Elektra ist eine Initiative zur Entwicklung, Wartung und Bereitstellung einer universellen Programmbibliothek für Konfiguration. Die Programmbibliothek abstrahiert über verschiedene Konfigurationsbestandteile um einheitlich darauf über Schlüssel-Werte-Paare zugreifen zu können. Es können auch Metainformationen zu diesen Schlüssel-Werte-Paaren gespeichert werden. Diese Metainformationen können verwendet werden um Konfigurationsspezifikationen zu definieren, welche die Semantik von Konfigurationen beschreibt. Beispiele für solche Metainformationen sind Bedingungen auf dem Wert eines Schlüssels, Verbindungen um Beziehungen zwischen Schlüssel-Werte-Paaren zu spezifizieren, und Transformationen, um Konfigurationsbestandteile aus anderen ableiten zu können. Konfigurationsspezifikationen können fehlerhaft sein, was zu unerwartetem oder falschem Verhalten zur Laufzeit führen kann. In dieser Diplomarbeit wird das Problem von fehlerhaften Konfigurationsspezifkationen gelöst indem ein Typsystem für Elektra entwickelt wird. Dieses Typsystem erkennt manche Fehler in einer Konfigurationsspezifikation statisch, um daraus resultierende Fehler zur Laufzeit zu reduzieren. Das HM(X)-Gerüst wird als die formale Basis des zu entwickelnden Typsystems HM(RGX) verwendet. HM(X) ist ein generisches formales Gerüst um domänenspezifische Hindley-Milner-artige Typsysteme zu spezifizieren. Die nötigen Beweisauflagen, die vom HM(X) Gerüst vorgegeben werden, werden erfüllt, um zu zeigen, dass das Typsystem in sich konsistent ist. Ein Prototyp dieses Typsystems wird in Form einer eingebetteten domänenspezifischen Sprache (EDSL) in der Programmiersprache Haskell entwickelt. Dafür wird ein Plugin für den Glasgow Haskell Compiler (GHC) geschrieben, mit dem die Semantik von HM(RGX) bei der Typüberprüfung umgesetzt wird. Es wird ebenso ein Plugin für Elektra entwickelt das Konfigurationsspezifikationen, die mit dieser EDSL beschrieben werden, auf Typfehler überprüft. Darüber hinaus wird ein weiteres Elektra Plugin geschrieben, das Metainformationen von Elektra über Schlüssel-Werte-Paare in die EDSL übersetzt. Eine Fallstudie wird durchgeführt um zu analysieren welche von Elektra aktuell unterstützten Metainformationen mit HM(RGX) beschrieben werden können.

Elektra is an initiative for developing, maintaining and providing a universal library for systemand application configuration. This library abstracts over various configuration items to provide a unified access, based on key-value pairs. Key-value pairs can store meta-information. This meta-information can be used to write configuration specifications describing the semantics of configuration. Examples for such meta-information are conditions on the value of a key, links to specify relationships between keys, and transformations to derive information based on other keys. Configuration specifications can be erroneous, leading to unexpected or faulty behavior at runtime. We improve the problem of erroneous configuration specifications by developing a type system for Elektra. This type system detects some errors in a configuration specification statically to reduce failures at runtime. We use the HM(X) framework as the foundation to describe our type system HM(RGX). HM(X) is a generic formal framework for specifying Hindley-Milner-style type systems. We fulfill the necessary proofs as imposed by this framework in order to show that our type system is sound and supports type inference. We implement a protoype of our type system by creating an embedded domain specific language (EDSL) in the general purpose programming language Haskell. We extend the Glasgow Haskell Compiler (GHC) by using a typechecker plugin to realize the semantics of HM(RGX). We develop a plugin for Elektra that typechecks configuration specifications written in our EDSL. We create another Elektra plugin that translates key-value pairs and their meta-information into our EDSL so it can be typechecked. We conduct a case study where we analyzed what kind of meta-information currently supported by Elektra can be described using HM(RGX).