Filling the Gaps of Polarity: Implementing Dependent Data and Codata Types with Implicit Arguments

TL;DR

This paper develops an algorithmic type system and inference algorithm for implicit arguments in Polarity, a dependently typed language supporting both inductive and coinductive types symmetrically, enhancing its expressiveness and usability.

Contribution

It provides a complete algorithmic description of Polarity's type system with implicit arguments and a unification algorithm for arbitrary inductive and coinductive types.

Findings

Algorithmic type system for implicit arguments implemented

Unification algorithm covers both inductive and coinductive types

Implementation available at https://polarity-lang.github.io/

Abstract

The expression problem describes a fundamental tradeoff between two types of extensibility: extending a type with new operations, such as by pattern matching on an algebraic data type in functional programming, and extending a type with new constructors, such as by adding a new object implementing an interface in object-oriented programming. Most dependently typed languages have good support for the former style through inductive types, but support for the latter style through coinductive types is usually much poorer. Polarity is a language that treats both kinds of types symmetrically and allows the developer to switch between type representations.However, it currently lacks several features expected of a state-of-the-art dependently typed language, such as implicit arguments. The central aim of this paper is to provide an algorithmic type system and inference algorithm for implicit arguments that respect the core symmetry of the language. Our work provides two key contributions: a complete algorithmic description of the type system backing Polarity, and a comprehensive description of a unification algorithm that covers arbitrary inductive and coinductive types. We give rules for reduction semantics, conversion checking, and a unification algorithm for pattern-matching, which are essential for a usable implementation. A work-in-progress implementation of the algorithms in this paper is available at https://polarity-lang.github.io/. We expect that the comprehensive account of the unification algorithm and our design decisions can serve as a blueprint for other dependently typed languages that support inductive and coinductive types symmetrically.