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$
2
  • 2
    $\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$ Feb 18, 2015 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$ Feb 19, 2015 at 11:58

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Browse other questions tagged or ask your own question.