[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Thanks Paolo and François, From my understanding of Solomon's paper, it seems that the problem of sub-typing would be equivalent to containment of deterministic context free languages, unfortunately this paper https://www.sciencedirect.com/science/article/pii/S0019995866800190 has proven it undecidable. That being said, I would be happy with a sound algorithm that works for reasonable practical cases (like my exploding list). — Isaac Oscar Gariano ________________________________ From: Paolo Giarrusso <[email protected]> Sent: 19 February 2020 3:14 AM To: Isaac <[email protected]>; Types list <[email protected]> Subject: Re: [TYPES] Has anyone seen a language with sub-typing and recursive parametric type aliases? Hello, On Tue, 18 Feb 2020 at 14:36, François Pottier <[email protected]<mailto:[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
