3
$\begingroup$

It seems that row polymorphism with union types can be used in dynamic languages to approximate overloading, e.g. given the following python function:

def f(foo, o):
    if foo:
        return o.x
    return o.y

Depending on the value of foo, the type of o could be $\forall \alpha, \left. \rho_1 \middle/ x \right.. \{x: \left. \alpha \mathrel{}\middle|\mathrel{} \rho_1 \right.\}$ or $\forall \beta, \left. \rho_2 \middle/ y \right.. \{y: \left. \beta \mathrel{}\middle|\mathrel{} \rho_2 \right.\}$, where $\alpha$ and $\beta$ are regular type variables, and $\rho_1$ and $\rho_2$ are row variables, lacking an $x$, respectively $y$ label. It would seem natural to extend this system to give f the type $\forall \alpha, \beta, \left. \rho_1 \middle/ x \right., \left. \rho_2 \middle/ y \right.. \{x: \left. \alpha \mathrel{}\middle|\mathrel{} \rho_1 \right.\} \cup \{y: \left. \beta \mathrel{}\middle|\mathrel{} \rho_2 \right.\} \rightarrow ()$, where $\cup$ stands for the union of the two types.

On the other hand I have seen intersection types used for the same purpose, e.g. f could be typed as $\forall \alpha, \left. \rho_1 \middle/ x \right.. \{x: \left. \alpha \mathrel{}\middle|\mathrel{} \rho_1 \right.\} \rightarrow () \wedge \forall \beta, \left. \rho_2 \middle/ y \right.. \{y: \left. \beta \mathrel{}\middle|\mathrel{} \rho_2 \right.\} \rightarrow ()$ where $\wedge$ stands for the intersection of the two types.

What is the difference between the two approaches? Which would be better for a type inferred system? What I'm interested in is if the two approaches are equivalent, i.e., they allow the same set of programs to be typed correctly, and which one is more amiable to type inference, if any.

$\endgroup$
  • 1
    $\begingroup$ Hmm, my money is on union types. Intersection types with implicit subtyping are too powerful to be even decidable: a lambda term is typable iff it is strongly normalizing. Union types don't seem as powerful. $\endgroup$ – Gilles Feb 18 '15 at 17:28
  • $\begingroup$ That being said, row polymorphism for polymorphic variants in OCaml does use intersections of label sets, though they don't often come up in places where programmers declare types. I don't know the details well enough to explain them, the right place to learn about them is probably Didier Rémy's papers (I assume you've already read the chapter in ATTAPL). $\endgroup$ – Gilles Feb 19 '15 at 11:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.