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.