Lambda the Ultimate

This concept only makes sense, as far as I can tell, for two tuples which share the first nth elements. Your examples would all be undefined I believe (or would be empty?).

The generalized concept might be described as "the operation which promotes a supertype to a subtype"?

Ta \ Tb = f
f(Tb) = Ta

What do you think?

...because (A,B,C)\(A,B) would simply be (A,B,C) if interpreted as set difference. ;-)

Also, note that CDuce is not higher-order nor polymorphic, IIRC. And yet its type system is pretty complex, and efficient algorithms for checking subtyping in it are an open problem IIRC.

...because (A,B,C)\(A,B) would simply be (A,B,C) if interpreted as set difference. ;-)

Good point!

...this wasn't quite correct: since there is subtyping (A,B,C)≤(A,B), the latter set would include the former. So in fact, the difference would be empty.

Of course, that does not meet your requirements either...

I see. Here is my fundamental problem, I wish to express the following subtyping rule for functions in the Cat language:

(A->B) <: (C->D)
<=> A <: C, B <: D, A\C = B\D

I am having problems expressing clearly the fact that the promotion function from C to A must be the same as the promotion function from D to B for the arrow type (function) to be valid.

(A->B) <: (C->D)
<=> A <: C, B <: D, A\C = B\D

This rule is wrong. You need C <: A (contravariance), otherwise it's unsound.

Also, I would suggests not using the notation A->B for your function types, since it pretends more generality than there actually is: IIUC, A and B always have to be tuples, since you have a stack language. That is, you actually have n-ary function types, not compositional function and tuple types.

And once you make the notation "honest", expressing the desired constraint is no longer a problem, because you don't have to resort to some weird adhoc concept on general types:

(A1..Am->B1..Bn) <: (C1..Ck->D1..Dl)
<=> m<k, l<n, for i≤m: Ci <: Ai, for j≤l: Bj <: Dj

This rule is wrong. You need C <: A (contravariance), otherwise it's unsound.

I understand that to be true for many languages, but I don't see it for Cat, and this is what I am trying to express. In a stack based language like Cat you can use a function such as id : ()->() when a function such as f : (int int)->(int int) is expected. Since function f satisfies the substitutability principle, it is a subtype of of id. The contravariance rule would fail in Cat.

I think part of the confusion is the fact that Cat has an ad-hoc notation for types. The input and output tuples of a function represents the configuration of the top of the stack, not the entire stack.

Also, I would suggests not using the notation A->B for your function types, since it pretends more generality than there actually is: IIUC, A and B always have to be tuples, since you have a stack language.

I didn't realize that was the implication. I was just trying to saving myself the headache of writing tuples longhand, but I appreciate you pointing out the problem.

I am not familiar with the term "compositional function and tuple types", can you elaborate?

(A1..Am->B1..Bn) <: (C1..Ck->D1..Dl)
<=> m<k, l<n,
for i≤m: Ci <: Ai, for j≤l: Bj <: Dj, 

Is actually incomplete according to the semantics of Cat, the following would be more accurate.

(A1..Am->B1..Bn) <: (C1..Ck->D1..Dl)
<=> k-m=l-n, m<k, l<n,
for i≤m: Ci <: Ai, for j≤l: Bj <: Dj, for i=m≤k: Ai = Bi

So this kind of notation would be more familiar to researchers?
I really appreciate your help on these issues!

The contravariance rule would fail in Cat.

I see. Interesting!

Now the whole story somewhat reminds me of record polymorphism. Your functions actually operate on extensible tuples (the stack). Your types ()->() and (int int)->(int int) can be interpreted as

forall rho. (rho) -> (rho)
forall rho. (int, int, rho) -> (int, int, rho)

where rho is a so-called row variable, representing the tail of a tuple (or record) type. The latter type scheme clearly is an instantiation of the former, so there is a natural subsumption relation.

But maybe the subtyping view is easier to understand, despite being somewhat non-standard.

I am not familiar with the term "compositional function and tuple types", can you elaborate?

Nothing technical here, I just meant function types and tuple types as orthogonal concepts. They are not independent in your language, and tuples are not first class, AFAICS.

So this kind of notation would be more familiar to researchers?

Well, it definitely is more obvious.

If the A1..An sequences get too long-winded you can of course abbreviate them, say, with something like \bar{A} or \vec{A}. But this clearly is a distinct syntactic category from type terms, so there is no confusion that they could actually be arbitrary types on their own.

Thank you very much for sharing that link with me Andreas. The notation you suggest makes a lot of sense, and is a very accurate rerpresentation of what it is that I am trying to achieve.

Morrow is a great paper that deals with row polymorphism.

Thank you very much for pointing the paper and discussion out to me!

If by higher-order you mean arrow types and first class functions, then yes, CDuce is higher-order. (Adding arrow types to XDuce was precisely the starting point of my work on CDuce.)

Polymorphism: Haruo, Castagna and I had a paper about adding polymorphism to XDuce (and it is implemented in the current version of XDuce). Unfortunately, this extension does not mix well with higher-order.

As for subtyping, the current algorithms are quite efficient in practice, even if the subtyping problem is DEXPTIME-complete (inclusion of regular tree languages).

Thanks Alain for clarifying. In particular, I mixed up CDuce with XDuce, sorry for that!