## Set-theoretic types for polymorphic variants

Published: 2016-09-17 (last updated: 2016-09-21)

In OCaml, union and intersection types are used to type polymorphic variants. But sometimes, their typing can be inflexible or unintuitive. See type of:

```
let f = function `Apple -> `Pomme
| `Cherry -> `Cerise
| x -> x
```

OCaml encodes unions and subtyping via unification, which has some shortcomings.

Our solution is:

- Use uion, intersection, and negation types directly
- Goal: have type reconstruction as in OCaml

# Our language

A fragment of OCaml with polymorphic variants and pattern matching.

The type system of OCaml is based on structural polymorphism [Guarrigue 2002].
Variant types are encoded via constraints and unification. Constraints introduce
*bounded polymorphism*.

We can get ill-typed programs:

```
let id = fun x -> match x with `A | `B -> x
[(id `A);`B] (* ill-typed! *)
```

We cannot express substraction of a type in the current OCaml system.

# Our approach

Opposite approach with respect to structural polymorphism: use rich types and subtyping.

# Types

Types are coinductively generated by:

`t ::= 'a | int | bool | c | t -> t | t × t | `tag(t) | t v t | not t | Empty`

# Type rules

Most rules are as in ML plus, the *subsumption rule* (see paper).

NB: no rule for intersection introduction.

With our way of encoding bounded polymorphism, we do not need constraints to introduce bounds.

# Patterns with set-theoretic types

Type connectives let us express exact types for patterns

# Reconstruction: constraint solving

To solve subtyping constraints we use the tallying algorithm of CDuce [Castagna et al '15].

# Results

Our set-theoretic type system is:

- complete
- more expressive
- features full-fledged union types and intersections & negations.

The reconstruction algorithm is both sound and complete.

Our system doesn't work with principal types though. But it allows completeness of reconstruction.

# Future work

- Attempt to define a notion of principality
- allow intersections of arrows for functions.
- consider other features of OCaml such as GADTs.