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.

翻译：表达式问题描述了两种可扩展性之间的基本权衡：一种是通过模式匹配代数数据类型（如函数式编程中）来扩展类型的新操作，另一种是通过实现接口的新对象（如面向对象编程中）来扩展类型的新构造器。大多数依赖类型语言通过归纳类型对前一种风格提供了良好支持，但通过余归纳类型对后一种风格的支持通常较为薄弱。Polarity 是一种将这两种类型对称处理并允许开发者在类型表示间切换的语言，然而它目前缺乏现代依赖类型语言所期望的若干特性，例如隐式参数。本文的核心目标是提供一种尊重语言核心对称性的隐式参数算法类型系统与推断算法。我们的工作贡献包括：为 Polarity 提供完整的算法类型系统描述，以及涵盖任意归纳与余归纳类型的统一算法全面阐述。我们给出了归约语义规则、转换检查规则以及用于模式匹配的统一算法，这些对于实际可用的实现至关重要。本文算法的初步实现可在 https://polarity-lang.github.io/ 获取。我们期望该统一算法的完整阐述及设计决策能为其他对称支持归纳与余归纳类型的依赖类型语言提供蓝图。