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.