[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hello, On Tue, 18 Feb 2020 at 14:36, François Pottier <[email protected]> wrote: > [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list > ] > > If I am not mistaken, already deciding the *equivalence* of two types > in the presence of recursive and parameterized type abbreviations is > extremely costly: Marvin Solomon proved it equivalent to the DPDA > equivalence problem ("Type definitions with parameters", POPL'78). > Indeed; Sénizergues later discovered this is decidable [1] but super-exponential, and this applies already to *nested datatypes* like Exploding-List ([2, Sec. 3.4.3]); I'm not familiar with the decision algorithm, but nobody describes it as practical in this context [2, 3]. I wonder if subtyping would reduce to DPDA containment, similarly to Solomon's result, and whether *that* problem is decidable. If you take F_{\omega\mu} but restrict fixpoints to result kind * (which excludes nested datatypes), definable types are equivalent to regular trees— so equivalence can be decided [2] by an extension of Amadio-Cardelli's algorithm that normalizes types first, as earlier conjectured by François Pottier [3]. That paper only deals with type equivalence, but Amadio-Cardelli's algorithm decides equirecursive subtyping; a combination of the two algorithms should decide F_{\omega\mu<:}. That appears to be equivalent to what you Isaac are doing (tho I suspect the "standard coinductive subtyping" is the Brandt-Henglein reformulation [4]), but I do not think anybody worked out the details and especially correctness/type soundness proofs? [1] Géraud Sénizergues. “Some Applications of the Decidability of DPDA’s Equivalence.” https://doi.org/10.1007/3-540-45132-3_7. Corollary 6. [2] Yufei Cai, Paolo G. Giarrusso, and Klaus Ostermann. “System F-Omega with Equirecursive Types for Datatype-Generic Programming.” http://dl.acm.org/citation.cfm?id=2837660. [3] François Pottier. http://lists.seas.upenn.edu/pipermail/types-list/2011/001525.html [4] Michael Brandt and Fritz Henglein. “Coinductive Axiomatization of Recursive Type Equality and Subtyping.” http://dl.acm.org/citation.cfm?id=2379036.2379037. Cheers, -- Paolo G. Giarrusso
