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

[ 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