QuB: A Resource Aware Functional Programming Language

TL;DR

The paper introduces QuB, a resource-aware functional programming language with a novel type system based on bunched implications, effectively managing resources like file handles and database connections at compile time.

Contribution

It presents a new type system that models resources as first-class citizens, ensuring resource correctness without losing functional programming benefits.

Findings

Guarantees resource correctness at compile time

Models resources as first-class citizens in the type system

Distinguishes between restricted and unrestricted objects

Abstract

Managing resources---file handles, database connections, etc.---is a hard problem. Debugging resource leaks and runtime errors due to resource mismanagement are difficult in evolving production code. Programming languages with static type systems are great tools to ensure erroneous code is detected at compile time. However, modern static type systems do little in the aspect of resource management as resources are treated as normal values. We propose a type system, Qub, based on the logic of bunched implications (BI) which models resources as first class citizens. We distinguish two kinds of program objects---restricted and unrestricted---and two kinds of functions---sharing and separating. Our approach guarantees resource correctness without compromising existing functional abstractions.