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

[gc@pps.jussieu.fr]

Tim Sweeney wrote:
>>
>> 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.
>>

Thank you very much, I am very glad you liked it.

>> 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.
>>

I cannot give a general answer (I would love to) but just a partial one based
on some form of poor-man dependent types.

First of all, even though the paper omitted them, CDuce has singleton types.
So for instance you can specify, that the successor function λx.x+1 has type
  (Int → Int) ∧	(2 → 3) where 2 and 3 are the singleton types containing the
values 2 and 3 respectively.

Now in their seminal paper
    A Modest Model of Records, Inheritance and Bounded Quantification.
    Inf. Comput.  87(1/2):196-239 (1990)
Bruce and Longo showed that record types can be interpreted as an indexed 
product that is as a first order quantification on finite sets of labels. 
Roughly the record type { a: Int, b: Bool} is the universal quantification 
∀x:{a,b}.F(x) where F is the mapping { a ↦ Int, b ↦ Bool}.
    Interestingly in CDuce record types are obtained by an intersection. Morally
they are an intersection of maps from singleton types to types or, if you
prefer, they are overloaded functions whose domains are singleton types of labels.
That is { a:Int, b:Bool } corresponds in CDuce to the overloaded function type
( a→Int ) ∧ (b→Bool) where again here a and b denote the two singleton types
containing the respective labels. So in this simple perspective you can see a
correspondence between ∀x:{a,b}.F(x) and (a→F(a)) ∧ (b→F(b)) which, if I
understood correctly, is what you were asking for. Of course this is a very
reductive example and whether this can be extended to general case you point out
in your post (and that if remember correctly you also evoked in your POPL talk)
I cannot say. But I would be delighted to see more examples of its use to
exactly understand what you are looking for. Do you have any pointer to
pseudocode you would like to type with such a technique?
   [Advertisement]In the meanwhile if you want to try to play with the CDuce
   singleton recursive intersection and union types and you do not want to
   install it, you can use our online interpreter at
   http://cduce.org/cgi-bin/cduce [/Advertisement]
   That said the combination of singleton types and semantic subtyping is a
funny beast since stunningly related problems about singleton types naturally
pop out from applying semantic subtyping to settings so different as parametric 
polymorphism (Hosoya et al. POPL'05) and pi-calculus (Castagna et al. LICS '05)

For those interested in this and similar problems they can find in LNCS n.3701 a
non-technical (well, let me say as less technical as possible) survey titled
    Semantic subtyping: challenges, perspectives, and open problems.
which I gave as invited talk at ICTCS '05
http://www.pps.jussieu.fr/~gc/papers/ictcs05a.pdf

There you will see that among the perspectives for semantic subtyping I consider
the application to dependent types quite an interesting topic for future
investigation. I think it would be a very nice topic for a PhD dissertation
(I would love to supervise).

>>
>> 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.
>>

Personally, I do not consider it a contradiction nor does it makes me feel
uneasy.  More precisely I do not care whether I cannot precisely associate each
type to a set that represents all its programs. All I really care is that I can
reason on types as if they were sets, and use this reasoning to deduce their
inclusion. In fact all that matters for me is that my programs do not go wrong,
and for that what I need to know is whether I can use an expression of some type
where one of a different type is expected. Once I can establish it I am happy
even if I  cannot say what the two types at issues exactly denoted but just how
they were related. Actually this is the essence of our approach.

---Beppe---



>> 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
>>