<p>Here are a few things to keep in mind:</p>

<ul>
<li>Although we generally think we know what we mean by set-theoretic intersection and union, there have been several different takes on what exactly intersection and union types <em>are</em>.  So, it's worth pinning this down before you embark on an implementation.</li>
<li>One element which I think is awfully important for understanding intersections and unions is the concept of <em>type refinement</em>, essentially the idea that a program has a certain intrinsic "archetype" (e.g., "<em>foo</em> is a function from integers to integers"), which can then be refined to express more precise properties (e.g., "<em>foo</em> takes even integers to even integers and odd integers to odd integers"). With the concept of refinement in hand, the key property which distinguishes intersections and unions from products and sums is that the intersection/union of two types can be formed only if they refine the same archetype.  In other words, the type formation rules for intersections and unions may be expressed like so (read "$S \sqsubset A$" as "$S$ refines $A$")
$$\frac{S\sqsubset A \quad T \sqsubset A}{S\cap T\sqsubset A}\qquad
\frac{S\sqsubset A \quad T \sqsubset A}{S\cup T\sqsubset A}$$
whereas the formation rules for ordinary products and sums are 
$$\frac{S\sqsubset A \quad T \sqsubset B}{S* T\sqsubset A*B}\qquad
\frac{S\sqsubset A \quad T \sqsubset B}{S+T\sqsubset A+B}$$</li>
<li>Since intersections and unions can be used to make more precise assertions about the run-time behavior of a program, it is natural that typing becomes sensitive to evaluation order. For example, papers <a href="http://www.cs.cmu.edu/~fp/papers/icfp00.pdf">(2)</a> and <a href="http://www.cs.cmu.edu/~joshuad/papers/tridirectional-typechecking-TR/Dunfield04_tridirectional-TR.pdf">(4)</a> below explained why  the "obvious" (and fairly standard) typing and subtyping rules for intersections and unions are actually unsound for ML-like languages (due to the presence of side effects and non-termination). <a href="http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/11/23/telling_lies.lhs/">You have been warned!</a></li>
<li>For similar reasons, global type inference generally becomes impractical or undecidable. Indeed, the whole concept of "principal type" is arguably a red-herring, since a function may satisfy many different properties which are irrelevant to its intended use (e.g., "<em>foo</em> takes prime integers to integers greater than 7"). Instead, practical approaches to intersections and unions (see <a href="http://reports-archive.adm.cs.cmu.edu/anon/2005/CMU-CS-05-110.pdf">(3)</a>, <a href="http://www.cs.cmu.edu/~joshuad/papers/tridirectional-typechecking-TR/Dunfield04_tridirectional-TR.pdf">(4)</a>) are generally based on a combination of inference and checking.</li>
</ul>

<p>I suppose some of the above points might sound negative, though I wouldn't call them "cons" but merely "realities" of intersection and union types. On the other hand, from a language design perspective, one reason for making the effort of supporting intersections and unions (and for getting them right!) is that they allow more precise properties of programs to be expressed in a fairly incremental way, requiring a much less drastic transformation than, say, dependent type theory.</p>

<p>A brief reading list:</p>

<ol>
<li><a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.42.9976&amp;rep=rep1&amp;type=pdf">Design of the Programming Language Forsythe</a> by John C. Reynolds</li>
<li><a href="http://www.cs.cmu.edu/~fp/papers/icfp00.pdf">Intersection Types and Computational Effects</a> by Rowan Davies and Frank Pfenning</li>
<li><a href="http://reports-archive.adm.cs.cmu.edu/anon/2005/CMU-CS-05-110.pdf">Practical Refinement-Type Checking</a> by Rowan Davies (dissertation)</li>
<li><a href="http://www.cs.cmu.edu/~joshuad/papers/tridirectional-typechecking-TR/Dunfield04_tridirectional-TR.pdf">Tridirectional Typechecking</a> by Joshua Dunfield and Frank Pfenning</li>
</ol>

CC BY-SA 3.0
2014-01-14T13:15:01.000Z
Great answer, many thanks. The links have been particularly useful and enlightening - so thanks for pointing me in the right directions!
mikera
CC BY-SA 3.0
2014-01-11T10:57:30.550Z
2014-01-11T10:57:30.550Z
Noam Zeilberger
<p>I'm designing a simple statically typed functional programming language as a learning experience.</p>

<p>It appears that the type system I have implemented so far could (with a little extra work) incorporate intersection and union types, e.g. you could have:</p>

<ul>
<li><code>&lt;Union String Integer&gt;</code></li>
<li><code>&lt;Union Integer Foo&gt;</code></li>
<li>The intersection of the two types above would be a plain <code>Integer</code></li>
<li>The union of the two types would be <code>&lt;Union String Integer Foo&gt;</code></li>
</ul>

<p>The fact that this is possible, of course, doesn't necessary mean it is a good design idea. In particular, I'm a somewhat concerned about the implementation difficulties of keeping the types disjoint and/or handling overlaps.</p>

<p>What are the pros/cons of incorporating such features in the type system?</p>

<type-theory><functional-programming><type-inference><language-design>
What are the practical issues with intersection and union types?
mikera
# What are the practical issues with intersection and union types?

(Asked by: username_0 on 2014-01-10)

I'm designing a simple statically typed functional programming language as a learning experience.

It appears that the type system I have implemented so far could (with a little extra work) incorporate intersection and union types, e.g. you could have:

* The intersection of the two types above would be a plain `Integer`
* The union of the two types would be

The fact that this is possible, of course, doesn't necessary mean it is a good design idea. In particular, I'm a somewhat concerned about the implementation difficulties of keeping the types disjoint and/or handling overlaps.

What are the pros/cons of incorporating such features in the type system?

**Tags:** type-theory, functional-programming, type-inference, language-design

---

## 1 answers

### Answer by username_1 on 2014-01-11. Score: 27 | Accepted answer

Here are a few things to keep in mind:

* Although we generally think we know what we mean by set-theoretic intersection and union, there have been several different takes on what exactly intersection and union types *are*. So, it's worth pinning this down before you embark on an implementation.
* One element which I think is awfully important for understanding intersections and unions is the concept of *type refinement*, essentially the idea that a program has a certain intrinsic "archetype" (e.g., "*foo* is a function from integers to integers"), which can then be refined to express more precise properties (e.g., "*foo* takes even integers to even integers and odd integers to odd integers"). With the concept of refinement in hand, the key property which distinguishes intersections and unions from products and sums is that the intersection/union of two types can be formed only if they refine the same archetype. In other words, the type formation rules for intersections and unions may be expressed like so (read "$S \sqsubset A$" as "$S$ refines $A$")
  $$\frac{S\sqsubset A \quad T \sqsubset A}{S\cap T\sqsubset A}\qquad
  \frac{S\sqsubset A \quad T \sqsubset A}{S\cup T\sqsubset A}$$
  whereas the formation rules for ordinary products and sums are
  $$\frac{S\sqsubset A \quad T \sqsubset B}{S\* T\sqsubset A\*B}\qquad
  \frac{S\sqsubset A \quad T \sqsubset B}{S+T\sqsubset A+B}$$
* Since intersections and unions can be used to make more precise assertions about the run-time behavior of a program, it is natural that typing becomes sensitive to evaluation order. For example, papers [(2)](http://www.cs.cmu.edu/~fp/papers/icfp00.pdf) and [(4)](http://www.cs.cmu.edu/~joshuad/papers/tridirectional-typechecking-TR/Dunfield04_tridirectional-TR.pdf) below explained why the "obvious" (and fairly standard) typing and subtyping rules for intersections and unions are actually unsound for ML-like languages (due to the presence of side effects and non-termination). [You have been warned!](http://goto.ucsd.edu/~rjhala/liquid/haskell/blog/blog/2013/11/23/telling_lies.lhs/)
* For similar reasons, global type inference generally becomes impractical or undecidable. Indeed, the whole concept of "principal type" is arguably a red-herring, since a function may satisfy many different properties which are irrelevant to its intended use (e.g., "*foo* takes prime integers to integers greater than 7"). Instead, practical approaches to intersections and unions (see [(3)](http://reports-archive.adm.cs.cmu.edu/anon/2005/CMU-CS-05-110.pdf), [(4)](http://www.cs.cmu.edu/~joshuad/papers/tridirectional-typechecking-TR/Dunfield04_tridirectional-TR.pdf)) are generally based on a combination of inference and checking.

I suppose some of the above points might sound negative, though I wouldn't call them "cons" but merely "realities" of intersection and union types. On the other hand, from a language design perspective, one reason for making the effort of supporting intersections and unions (and for getting them right!) is that they allow more precise properties of programs to be expressed in a fairly incremental way, requiring a much less drastic transformation than, say, dependent type theory.

A brief reading list:

1. [Design of the Programming Language Forsythe](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.42.9976&rep=rep1&type=pdf) by John C. Reynolds
2. [Intersection Types and Computational Effects](http://www.cs.cmu.edu/~fp/papers/icfp00.pdf) by Rowan Davies and Frank Pfenning
3. [Practical Refinement-Type Checking](http://reports-archive.adm.cs.cmu.edu/anon/2005/CMU-CS-05-110.pdf) by Rowan Davies (dissertation)
4. [Tridirectional Typechecking](http://www.cs.cmu.edu/~joshuad/papers/tridirectional-typechecking-TR/Dunfield04_tridirectional-TR.pdf) by Joshua Dunfield and Frank Pfenning

> **Comments:**
> **username_0**: Great answer, many thanks. The links have been particularly useful and enlightening - so thanks for pointing me in the right directions!  

---

