[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hello, Have you checked Kennedy and Pierce's paper "On Decidability of Nominal Subtyping with Variance"? -Moez From: Types-list <[email protected]> on behalf of Isaac <[email protected]> Sent: Tuesday, February 18, 2020, 07:49 To: [email protected] 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
