[TYPES] Has anyone seen a language with sub-typing and recursive parametric type aliases?

[Isaac]

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 <p.giarrusso at gmail.com>
Sent: 19 February 2020 3:14 AM
To: Isaac <Isaac.Oscar.Gariano at ecs.vuw.ac.nz>; Types list <types-list at lists.seas.upenn.edu>
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 <francois.pottier at inria.fr<mailto:francois.pottier at inria.fr>> 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