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

Researchers present an algorithmic type system and unification algorithm for Polarity, a dependently typed language that treats inductive (data) and coinductive (codata) types symmetrically. The work addresses the expression problem by enabling both pattern matching extensibility and interface-based extensibility while adding support for implicit arguments. The paper provides comprehensive algorithms for reduction semantics, conversion checking, and pattern-matching unification that maintain the language's core symmetry between data and codata types.