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

[Dan Smith]

Thank you all for your useful pointers.

In skimming a number of papers related to these references, I have yet  
to come upon the ideal presentation I'm looking for.  I would love to  
see a paper that:

- Extends lambda-sub (the simply-typed lambda-calculus with subtyping)  
with intersection and union types.

- Defines typing and subtyping in this calculus using simple  
operational semantics, in the style used by Pierce.

- Develops a subtyping algorithm in two stages: first, by defining  
subtyping "declaratively" -- explicitly including rules like  
transitivity -- and then redefining it using syntax-directed rules  
(and proving that the two definitions are equivalent).

- Includes in its declarative subtyping definition the two rules I  
mentioned below for distribution over arrow types.

Of course, this is just the lazy route -- given the papers that I  
*have* seen, I ought to be able with some effort to extract the  
concepts that would be presented in my ideal paper.  And I can accept  
that.  (My apologies if any of the references I've been pointed to  
meet these criteria, and I just wasn't perceptive enough to catch  
it.)  But I thought I'd be more explicit about what I'm looking for,  
just in case anyone is aware of something that meets or is close to  
these criteria.

--Dan


On Apr 9, 2008, at 10:15 AM, Dan Smith wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list 
>  ]
>
> Benjamin Pierce's PhD work involved a calculus combining System F,
> intersection types, and bounded quantification (Programming With
> Intersection Types and Bounded Polymorphism, 1991).  His earlier work
> aspired to including union types in this calculus as well, but that
> was apparently dropped (Programming with Intersection Types, Union
> Types, and Polymorphism, 1991).
>
> What is the best place to find a similar calculus that includes union
> types?  In particular, I'm looking for a similar formal treatment of
> subtyping that includes the following rules ("&" is intersection; "|"
> is union):
>
> S->T1 & S->T2 <: S->(T1 & T2)
>
> S1->T & S2->T <: (S1 | S2)->T
>
> Any help would be appreciated.
>
> --Dan