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

[Rodolphe Lepigre]

Hi,

Together with Christophe Raffalli, we defined a language called SubML that can
do more or less what you ask for. Here are a couple of links:
 - https://rlepigre.github.io/subml/ (online interpreter to play around),
 - https://github.com/rlepigre/subml/ (repository),
 - https://dl.acm.org/doi/10.1145/3285955 (TOPLAS paper, also on my web page).

When I say "more or less", I mean that we cannot directly express your example
in full. However, I see no reason why our technique could not apply given some
adaptation work. What is missing from SubML to handle your example is that the
type parameters of an inductive or coinductive type is fixed in its definition
due to the way they are defined (using least and greatest fixpoints).

The best I can do currently is:
==========
include "nat.typ"

type List(X) = νList   .{ head : X   ; tail : List    ; … }
type NatList = νNatList.{ head : Nat ; tail : NatList ; … }

check NatList ⊆ List(Nat)
check List(Nat) ⊆ NatList
check { head : Nat ; tail : NatList ; sum : Nat ; … }
    ⊆ { head : Nat ; tail : List(Nat) ; … }
check Nat ⊆ Nat

(* Note the "List" here. *)
type ExplList(X) = νExplList.{ head : X   ; explode : List(ExplList) ; … }
type NatExpl     = νNatExpl .{ head : Nat ; explode : List(NatExpl ) ; … }

check NatExpl ⊆ ExplList(Nat)
check { head : Nat ; explode : ExplList(NatExpl) ; … }
    ⊆ { head : Nat ; explode : ExplList(ExplList(Nat)) ; … }
check ExplList(NatExpl) ⊆ ExplList(ExplList(Nat))
check { head : Nat ; explode : ExplList(ExplList(NatExpl)) ; … }
    ⊆ { head : Nat ; explode : ExplList(ExplList(ExplList(Nat))) ; … }
check ExplList(ExplList(NatExpl)) ⊆ ExplList(ExplList(ExplList(Nat)))
==========

In fact, we can express your example in PML (https://github.com/rlepigre/pml),
which is a proof system built using similar techniques (with extensions).  But
currently these features are quite experimental so the subtyping relations you
want for your exploding lists cannot be proved by the system  (including those
that should be trivial...). I'll investigate when I have a moment.
==========
include lib.nat

type corec list⟨a:ο⟩ = { head : a   ; tail : list⟨a⟩ ; ⋯ }
type corec natlist   = { head : nat ; tail : natlist ; ⋯ }

assert natlist ⊂ list⟨nat⟩
assert list⟨nat⟩ ⊂ natlist
assert { head : nat ; tail : natlist ; sum : nat ; ⋯ } ⊂ { head : nat ; tail : list⟨nat⟩ ; ⋯ }
assert nat ⊂ nat

type corec any_expl⟨a:ο⟩ = { head : a   ; explode : any_expl⟨any_expl⟨a  ⟩⟩ ; ⋯ }
type corec nat_expl      = { head : nat ; explode : any_expl⟨any_expl⟨nat⟩⟩ ; ⋯ }

// FIXME do not work
//assert any_expl⟨nat⟩ ⊂ nat_expl // should be trivial
//assert nat_expl ⊂ any_expl⟨nat⟩ // should be trivial
//assert { head : nat ; explode : any_expl⟨nat_expl⟩ ; ⋯ } ⊂ { head : nat ; explode : any_expl⟨any_expl⟨nat⟩⟩ }
//assert any_expl⟨nat_expl⟩ ⊂ any_expl⟨any_expl⟨nat⟩⟩
//assert { head : nat ; explode : any_expl⟨any_expl⟨nat_expl⟩⟩; ⋯ } ⊂ { head : nat ; explode : any_expl⟨any_expl⟨any_expl⟨nat⟩⟩⟩ }
//assert any_expl⟨nat_expl⟩ ⊂ any_expl⟨any_expl⟨nat⟩⟩
==========

Now in terms of technique, what we do is (roughly):
  1) build cyclic subtyping proofs, and
  2) prove that the cyclic proof are well-founded.

To do that, our (inductive and coinductive) types are annotated with ordinals,
and we then check that there is some decrease in the ordinals along the cyclic
structure of the proof (in our work this is done using a variation of the size
change principle of Lee, Jones and Ben-Amram). Annotating types using sizes is
usually called "sized types" (they are often natural numbers in the literature
but sometimes also ordinals). Of course, size annotations are not always given
by the user explicitly. For subtyping I think they can always be automatically
inserted. However the size algebra that we currently use may not be expressive
enough (it is very minima and only has variables, successor and a large enough
constant to make all fixed points converge). Extensions are possible.

The SubML language relies on this cyclic proof mechanism for subtyping and for
termination checking, but it is certainly possible to only do the former.

I hope this helps, do not hesitate to ask me for more details.

Cheers,
Rodolphe.
-- 
Rodolphe Lepigre <lepigre at mpi-sws.org>
Max Planck Institute for Software Systems, Saarbrücken, Germany
https://lepigre.fr

On 18/02/20 01:13, Isaac wrote:
> [ 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