How to compute variance of a type

How to compute variance of a type

[Tom Primožič]

[-- Attachment #1: Type: text/plain, Size: 762 bytes --]

I am writing a type inference engine for a simple ML-like language, and I am
wondering how to infer the variance of type parameters. I know a little
about variance already, so I could figure it out for some basic cases, like
in type

    type ('a, 'b) funct = 'a -> 'b

the type variable 'a is contravariant, and 'b is covariant, and in case one
variable would be co- and contravariant at the same time, it is invariant

    type ('a, 'b) both   =   Left of 'a -> 'b   |   Right of 'b -> 'a.

But I have no idea on how to compute variance of complex types, like

    type ('a, 'b, 'c) long_funct = ('a -> 'b) -> 'c

since the whole ('a -> 'b) is in contravariant position, so 'a is twice
contravariant, and b is first contra-, and the covariant.

Any resources?

[-- Attachment #2: Type: text/html, Size: 983 bytes --]

Re: [Caml-list] How to compute variance of a type

[rossberg]

Tom Primožiè wrote:
>
> But I have no idea on how to compute variance of complex types, like
>
>    type ('a, 'b, 'c) long_funct = ('a -> 'b) -> 'c
>
> since the whole ('a -> 'b) is in contravariant position, so 'a is twice
contravariant,
> and b is first contra-, and the covariant.
>
> Any resources?

Off-hand I don't have any easy resources I could point to, but the basic
rule is very simple: whenever you descent into a type argument where the
respective type constructor has negative polarity (like the left argument
of "->"), you just negate the variances. Thus, in your example, long_funct
is covariant in 'a and 'c, and contravariant in 'b. It is straightforward
to formulate that as a recursive algorithm.

- Andreas

Re: [Caml-list] How to compute variance of a type

[Andrej Bauer]

There is nothing strange or complicated about variance. Whenever you
descend to the left of an arrow, you have to switch the variance.

I enclose a simple example of how to compute variance for simple types.

Andrej

P.S. Feel free to knock on my office door when you have such questions :-)

--------------------------------------------------------
type name = string

type ty =
  | Var of name      (* type variable *)
  | Prod of ty * ty  (* product *)
  | Arrow of ty * ty (* function type *)

type variance =
  | Variant
  | Covariant
  | Mixed

(** Join variances *)
let join u v =
  if u = v then v else Mixed

let opposite = function
  | Variant -> Covariant
  | Covariant -> Variant
  | Mixed -> Mixed

(** Add a type variable [x] with variance [v] to a given association
    list of variances. *)
let rec add x v = function
  | [] -> [(x,v)]
  | (y,u)::lst ->
      if x = y then
	(x, join u v) :: lst
      else
	(y,u) :: (add x v lst)

(** Compute variances of all type variables appearing
    in a type. Return an association list mapping type parameters
    to their variances.
 *)
let variance t =
  let rec var c lst = function
    | Var v -> add v c lst
    | Prod (t1, t2) -> var c (var c lst t1) t2
    | Arrow (t1, t2) -> var c (var (opposite c) lst t1) t2
  in
    var Variant [] t

(** Examples. *)

let t1 = Arrow (Arrow (Var "a", Var "b"), Var "c")
let v1 = variance t1

let t2 = Arrow (Var "a", Arrow (Var "b", Var "c"))
let v2 = variance t2

let t3 = Arrow (Prod (Var "a", Var "b"), Var "a")
let v3 = variance t3
---------------------------------------------------------