Efficient compilation of polymorphic record calculi

Abstract

Labeled records are widely used data structures and constitute essential building blocks in various data-intensive applications. Despite their practical importance, existing polymor- phic programming languages do not adequately support these data structures. To make a sound polymorphic programming language that supports labeled records while having efficient compilation, Ohori has provided a type inference algorithm based on the notion of a kind. This system, however, had the limitation of lacking support for extensible records. Recently, a record calculus with extensible records has been developed, although without a compilation mechanism. Firstly, this thesis aims to implement the compilation relation defined by Ohori. For this purpose, an interpreter for the record calculus will be developed using Haskell as the programming language of choice. This will allow us to test and evaluate Ohori's algorithm and prove its efficiency and robustness. Furthermore, it's intended to explore extending the compilation algorithm to the cal- culus with extended records. Ohori showed that his algorithm preserves types and that the compilation calculus has the subject reduction property, thus showing that the compilation algorithm preserves the operational behavior of the original polymorphic record calculus. Therefore, it's believed that an efficient compilation algorithm can also be defined for the new calculus since variables still range over complete record types, and the information that was added to kinds to deal with extensible operations only affects type inference, not compilation. The lack of extensible record-based operations, such as adding or removing fields, in polymorphic record calculi is often accepted in practical implementations of languages with record types, in a trade for efficiency, or due to the difficulty in guaranteeing the correctness of types for more flexible operations. As such, the successful development of an efficient compilation method for a record calculus with extensible records holds significant potential contributions to both theoretical and practical aspects of record calculi. This advancement may find applications in real programming languages, addressing the longstanding challenge of balancing flexibility and efficiency in handling record types. ii