The Implementation of Functional Programming Language with Linear Types

A pure functional programming language is often considered as a conservativee extension of $\lambda$-calculus and uses it as the formalisation of the notion of evaluation. The Curry——Howard correspondence states that there is an isomorphism between terms of dependently typed $\lambda$-calculus and formulae of intuitionistic predicate logic, thus by changing the underlying logic one can obtain type systems with different properties. This idea spawned a plethora of various programming languages, both functional and imperative, which utilise different type systems. Many if not most of such programming languages use type systems as a way to improve expressiveness of the language and to enforce safety and rarely use types to improve both time and memory performance. In general, the evaluation of $\lambda$-terms is independent of type system, since $\beta$-reduction is merely a term rewriting system. However real world implementation are more than abstract symbolic machines and suffer from the limitations of existing hardware. We develop the idea that more elaborate type systems allow to create not only more expressive and safe programmes, but to write better implementations of pure functional programming languages, and prove it by implementing a functional programming language with linear type system. We base our work on the recent research in the area of programming language theory as well as well-established ideas used in the industry for a long time. We extend the existing programming language Quill with practical improvements and provide an implementation of the named language. The ideas developed in this paper can be applied to other pure functional programming languages with non-strict evaluation models. The recent advent of popularity of functional approach to programming languages and popularity of Rust, which uses a variant of affine type system, the type system closely related to the linear types considered in this work, indicates that the research in this area will find application in the industry.