[TYPES] Formal treatment of intersection/union/arrow subtyping?

[Tim Sweeney]

This paper's treatment of subtyping as a subset relation is extremely insightful.  In particular, its definition of function arrows T->U as the complemented product ~(T x ~U) precisely captures the nature of contravariance and overloaded functions in the presence of subtyping.

In this sort of representation, is it recognized that universal and existential quantifiers coincide precisely with set-indexed intersection and union?  In particular, all(x:t) ux coincides with the intersection, for each element x from set t, of the set ux (which may reference x).  And similarly for existential quantifiers.

If this system is extended with such quantifiers, with a dependent-typed singleton-set constructor, a powerset constructor, and recursive definitions, then we have [my conjecture] the perfect type system for future programming languages, given its combination of power and expressiveness.

The singleton-set construct enables us to use the type-quantifiers over values, so that we types dependent on other types and on values.

For example, given a type of n-element arrays of elements with type t, we can use its existential quantifiers to express type of all arrays of type t, with n effectively erased (not bundled up into an existential dependent product).  Then we can use its universal quantifiers to express functions over arrays of any length, where we reconstruct the length through quantifier instantiation.  The resulting code is very concise, and this allows programming practices similar to C++ templates and Java generics, where the programmer writes simple code using libraries with complex types, and the compiler performs a lot of quantifier instantiation to fill in the implicit details during the typechecking phase.

Taking this approach does require a temporary suspension of disbelief.  As the author points out, cardinality arguments prevent us from interpreting types precisely as sets within ZF.  In this case, I think it's fruitful to explore the type theory first, and look to resolve the seeming contradictions later.  The author avoids trouble by referring to the subset relation only to establish subtyping, and not as a literal interpretation of types as sets.  But other approaches may be interesting, for example choosing a set theory such as NF which treats infinities differently than ZF, perhaps giving types a valid literal interpretation as sets.

Tim Sweeney
Epic Games

-----Original Message-----
From: types-list-bounces at lists.seas.upenn.edu [mailto:types-list-bounces at lists.seas.upenn.edu] On Behalf Of NOREPLY
Sent: Wednesday, April 09, 2008 2:59 PM
To: types-list at lists.seas.upenn.edu
Subject: Re: [TYPES] Formal treatment of intersection/union/arrow subtyping?

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Benjamin Pierce wrote:
> Also check out the CDuce web page.

If you do not want to check all the papers in the CDuce page my advice
is that your best bet is the following paper that will appear in
The Journal of the ACM:

Semantic Subtyping: dealing set-theoretically with function, union,
intersection, and negation types.

it can be found in my home page or directly by following this link
http://www.pps.jussieu.fr/~gc/papers/semantic_subtyping.pdf

Section 2 gives an relatively simple introduction of the subject, in
Sections 3-4 you have an overview of the main results. Then you can skip
Section 6 and jump directly to Section 7 which is a commentary on the more
technical results among which you will also find a discussion about the
relation with Benjamin's PhD and its follows up.

Please do not hesitate to contact me if you have any question or remark.

---Beppe---

(Giuseppe Castagna)