## Polymorphic variants : Subtyping and variance

Here are some expressions in the top-level involving polymorphic variant types.

# let x = [ `On; `Off ];; val x : [> `Off | `On ] list = [ `On; `Off ]The notation

`[> `Off | `On ]`

represents a type
that **at least**contains the constructors

``Off`

and ``On`

. Of course, there are an unlimited number of
such types so `[> `Off | `On ]`

is a set in fact.

# let n = `Number 1;; val n : [> `Number of int ] = `Number 1The value

`n`

is of a type that **at least**contains the constructor

``Number of int`

.

# let f = function | `On → 1 | `Off → 0 | `Number n → n;; val f : [< `Number of int | `Off | `On ] → int = <fun>The function

`f`

accomodates exactly three cases
corresponding to the
constructors ``Off`

, ``On`

and ```
`Number
of int
```

. This informs us that ```
[< `Number of int |
`Off | `On ]
```

is of a type that **at most**has the constructors

``Off`

, ``On`

and ```
`Number
of int
```

.
The expression `(`

$expr$```
:>
```

$typexpr$`)`

coerces the expression $expr$ to
type $typexpr$. The expression `(`

$expr$ `:`

$typ_{1}$ `:>`

$typ_{2}$ `)`

coerces the
exprssion $expr$ from $typ_{1}$ to $typ_{2}$. It is only possible
to coerce an expression $expr$ from type $typ_{1}$ to type
$typ_{2}$, if the type of $expr$ is an instance of $typ_{1}$ and
$typ_{1}$ is a subtype of $typ_{2}$.

# let f x = (x :> [ `A | `B ]);; val f : [< `A | `B ] → [ `A | `B ] = <fun>We see

`x`

needs to be coercible to type ```
[ `A |
`B ]
```

. So, we read `[< `A | `B ]`

as a type
that at most contains the constructors ``A`

and ``B`

. `[ `A ]`

, `[ `B ]`

and `[ `A | `B ]`

are the subtypes of ```
[ `A | `B
]
```

. It follows then that `[< `A | `B ]`

is
the set of subtypes of `[ `A | `B ]`

.

# let f x = (x :> [ `A | `B ] * [ `C | `D ]);; val f : [< `A | `B ] * [< `C | `D ] → [ `A | `B ] * [ `C | `D ] = <fun>We see

`x`

needs to be coercible to ```
[ `A | `B ] *
[ `C | `D ]
```

. This coercion can only proceed
if `x`

designates a pair with first component a subtype
of `[ `A | `B ]`

and second component a subtype
of `[ `C | `D ]`

. So we see, ```
[< `A | `B ] *
[< `C | `D ]
```

is the set of subtypes of ```
[ `A | `B ]
* [ `C | `D ]
```

.

# let f x = (x :> [ `A ] → [ `C | `D ]);; val f : ([> `A ] → [< `C | `D ]) → [ `A ] → [ `C | `D ] = <fun>We see

`x`

needs to be coercible to ```
[ `A ] → [
`C | `D ]
```

. This coercion can only proceed if `x`

designates an arrow where the argument is of a type that at least
contains the constructor ``A`

. That is ```
[ `A
]
```

, `[ `A | ... ]`

where the "`...`

"
represent more constructors. From this we see that ```
[>
`A]
```

is the set of supertypes of `[ `A ]`

. The
return value of `x`

(by logic we've already
established) is a subtype of ```
[ `C | `D
]
```

. So, `[> `A ] → [< `C | `D ]`

is the
set of subtypes of `[ `A ] → [ `C | `D ]`

.
The transformation represented by `f`

above, has
coerced an arrow `x`

to a new arrow. The type of the
argument of `x`

is `[> `A ]`

and the
type of the argument of the resulting arrow is ```
[ `A
]
```

. That is, for the argument, the transformation between
types has taken a supertype to a subtype. The argument type is
said to be in a "contravariant" position. On the other hand, the
result type of `x`

is `[< `C | `D ]`

and
the arrow that is produced from it, `f x`

, has result
type `[ `C | `D ]`

. That is, the coercion for the
result type has taken a subtype to a supertype : the result type
in `x`

is said to be in "covariant" position.

In the following, the type `α t`

is abstract.

# type α t;; # let f (x : [ `A ] t) = (x :> [ `A | `B ] t);; Error: Type [ `A ] t is not a subtype of [ `A | `B ] tIndeed,

`[ `A ]`

is a subtype of ```
[ `A | `B
]
```

but that, *a priori*, does not say anything about the subtyping relationship between

`[ `A ] t`

and `[ `A | `B ] t`

. For this coercion to be legal, the
parameter `α`

must be given a covariant
annotation:
# type +α t;; # let f (x : [ `A ] t) = (x :> [ `A | `B ] t);; val f : [ `A ] t → [ `A | `B ] t = <fun>The declaration

`type +α t`

declares that the
abstract type is covariant in its parameter : if the type $\tau$
is a subtype of $\sigma$, then $\tau\;t$ is a subtype of
$\sigma\;t$. Here, $\tau = $`[ `A ]`

, $\sigma =
$`[ `A | `B ]`

, $\tau$ is a subtype of $\sigma$
and `[ `A ] t`

is a subtype of ```
[ `A | `B]
t
```

.
Here is a similar example, but this time, in the other direction.

# type α t;; # let f (x : [ `A | `B ] t) = (x :> [ `A ] t);; Error: This expression cannot be coerced to type [ `A ] tThe type variable can be annotated as contravariant however, and the coercion function typechecks.

# type -α t;; # let f (x : [`A | `B] t) = (x :> [ `A ] t);; val f : [ `A | `B ] t → [ `A ] t = <fun>The declaration

`type -α t`

declares that the abstract
type `t`

is contravariant in its parameter : if $\tau$
is a subtype of $\sigma$ then $\sigma\;t$ is a subtype of
$\tau\;t$. In this example, $\tau = $`[ `A ]`

and
$\sigma = $`[`A | `B]`

, $\tau$ is a subtype of $\sigma$
and
`[ `A | `B ] t`

is a subtype of `[ `A ] t`

.
In the following, `type α t`

is **not**
abstract and variance can be inferred.

# type α t = {x : α} ;; # let f x = (x : [`A] t :> [`A | `B] t);; val f : [ `A ] t → [ `A | `B ] t = <fun>Introducing a constraint however inhibits variance inference.

# type α t = {x : α} constraint α = [< `A | `B ];; # let f x = (x : [ `A ] t :> [ `A | `B ] t);; Error: Type [ `A ] t is not a subtype of [ `A | `B ] tThis situation can be overcome by introducing a covariance annotation.

# type +α t = {x : α} constraint α = [< `A | `B ];; # let f x = (x : [ `A ] t :> [ `A | `B ] t);; val f : [ `A ] t → [ `A | `B ] t = <fun>In the following example,

`α`

does not
participate in the definition of `type α t`

.
# type α t = {x : int};; # let f x = (x : [ `A ] t :> [ `B ] t);; val f : [ `A ] t → [ `B ] t = <fun>In this case, any conversion between

`δ t`

and `ε t`

is legal : the
types `δ`

and `ε`

are not
required to have a subtyping relation between them.