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

Bohdan Liesnikov, David Binder, Tim Süberkrüb

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 t…