Set-theoretic types for polymorphic variants

Written by OlivierNicole (Olivier Nicole)
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.