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

[moez at cs.rice.edu]

Hello,
Have you checked Kennedy and Pierce's paper "On Decidability of Nominal Subtyping with Variance"?
-Moez
From: Types-list <types-list-bounces at lists.seas.upenn.edu> on behalf of Isaac <isaac.oscar.gariano at ecs.vuw.ac.nz>
Sent: Tuesday, February 18, 2020, 07:49
To: types-list at lists.seas.upenn.edu
Subject: [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,

I am currently working on writing a type-checker for an object-oriented structural type-system with generics and recursive types. In particular, it's supports recursive parametric type alias, e.g:
        type List[X] = { head -> X; tail -> List[X]}

Then, if T is a type, a "List[T]" is any object with a head method that returns "T"s and a tail method that returns "List[T]"s.
Note that partially-applied type aliases are not allowed, e.g. "List" is not a valid type.
Type-alias can have any number of type-parameters, including zero, and can also be mutually recursive.

Now since this type-system is structurally typed, if I define:
        type Integer-List = { head -> Integer; tail -> Integer-List; sum -> Integer }

I should have that Integer-List is a sub-type of List[Integer] (which I will denote Integer-List <: List[Integer])
In this simple case, I can use a standard con-inductive algorithm for recursive types:
    - Integer-List <: List[Integer]?
    - { head -> Integer; tail -> Integer-List; sum -> Integer } <: {head -> Integer; tail -> List[Integer]}?
    - Integer <: Integer? and Integer-List <: List[Integer]?
    - Yes (by reflexivity) and yes (by co-induction, since we are already trying to work out if Integer-List <: List[Integer])

Ok, now on to the hard bit, what if I have:
        type Exploding-List[X] = { head -> X; explode -> Exploding-List[Exploding-List[X]] }
        type Integer-Explosion = { head-> Integer; explode -> Exploding-List[Integer-Explosion] }

Is Integer-Explosion a sub-type of Exploding-List[Integer]?
    - Integer-Explosion <: Exploding-List[Integer]?
    - { head-> Integer; explode -> Exploding-List[Integer-Explosion] } <: { head -> Integer; explode -> Exploding-List[Exploding-List[Integer]] }?
    - Integer <: Integer? and Exploding-List[Integer-Explosion] <: Exploding-List[Exploding-List[Integer]]?
    - yes (by reflexivity) and
              { head -> Integer-Explosion; explode -> Exploding-List[Exploding-List[Integer-Explosion]] }
          <: { head -> Exploding-List[Integer]; explode -> Exploding-List[Exploding-List[Exploding-List[Integer]]] }
    - Integer-Explosion <: Exploding-List[Integer] and Exploding-List[Exploding-List[Integer-Explosion]] <: Exploding-List[Exploding-List[Exploding-List[Integer]]]
    - yes (by co-induction) and ....

If I keep going I will get increasingly large sub-type tests of form Exploding-List[... Exploding-List[Integer-Explosion] ... ] <: Exploding-List[...Exploding-List[Integer]...].
Co-induction wont save me here as there are an infinite number of such sub-type tests I need to perform (since there are an infinite number of types).

The question is, is anyone aware of any algorithm I could use to compute such sub-typing relations? or does anyone know of an existing type-checker that already does this?

After some research, the only language I could find that appears to support such constructs is the one from this paper (which they call λ-rec-abs)  https://link.springer.com/content/pdf/10.1007%2F978-3-642-39212-2_28.pdf.
However they do not discuss sub-typing.

I find this particularly interesting as I don't think that such infinitely expanding sub-type tests are that pathological, for example it might be reasonable to have a List[T] type with a split(T) -> List[List[T]] method: the idea being that list.split(x) will split the list on occurrences of "x" (like you can do with strings in many languages: "1,2,3".split(",") = ["1", "2", "3"].

I'm not aware of any real-world programming languages that support structural typing like the above, I've tried Scala but it is not possible to have a recursive type alias, and OCaml, which only allows type alias with simple recursion like my original "List" example, and flat out rejects my Exploding-List type.

— Isaac Oscar Gariano​