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 1
The 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 ] t
Indeed, [ `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 ] t
The 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 ] t
This 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.
