07.07.2023; Kolloquium
Echtzeit-AGProcess Composition with Typed UNIX Pipes
This work discusses and introduces a type-system for pipelines in UNIX-like shells. Command interpreters, such as UNIX shells, provide a text based user interface for launching processes and are commonly used by developers and power-users as their primary vehicle for daily work and administrative tasks. The ability to construct pipelines of commands, where the output of one process is used as input to another process, is one of the most powerful features of shells. However, as pipelines become more sophisticated, their biggest strength – the flexibility to combine anything with anything, can also become a problem if it leads to combination of incompatible proceses. To solve this, we propose using a type-system with a special type-constructor (the ladder-type) and a thereby induced structural subtyping relation to ensure that the input and output of each command match the expected types. We present a system to extend existing shells with a type-check routine and demonstrates its utility through a series of examples and case studies, showing how it can improve the safety and reliability of pipelines.
(Großer Beleg)