## Tuesday, March 7, 2017

### Polymorphic variants : Subtyping and variance

Polymorphic variants : subtyping and variance

## 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.