MMH: High-level programming with the Mu-Mu-Tilde-calculus

Abstract

The 𝜇𝜇-̃ calculus is a small core programming language, for which the separation between data and codata is essential. To make the power of this separation more accessible, we introduce MMH, a high-level functional programming language that compiles to the 𝜇𝜇-̃ calculus. We show how 𝜆-calculus programs can be converted to 𝜇𝜇-̃ calculus programs, and extend the calculus with programmer-friendly features, such as nested (co-)pattern matching. We introduce a polymorphic typing system to the 𝜇𝜇-̃ calculus for which type inferencing is decidable, and allow MMH to reap the benefits.