[ 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
