Variance of GADT parameters; a pragmatic work in progress
April 19th, 2012
Strathclyde, Glasgow
Abstract:
OCaml is getting GADTs soon. It also has some subtyping, which
(happily) one can mostly ignore, except maybe in its link to the
relaxed value restriction. It turns out that the pragmatic
implications of combining those two features are not
well-known. What does it mean for a GADT to be contravariant in some
parameter? Is there a simple criterion for checking this, that can
be implemented without fuss and understood by users? While not
world-changing, the study of these questions raises intriguing
language design questions.
# What variance is
Semantically, the type constructor (T ᾱ) has been asigned variance
(≤̄) with each ≤i in {≤,≥,=} when
(∀i, αi ≤i α'i) iff (T ᾱ ≤ T ᾱ')
(What this order (≤) is depends on the language. Could be subtyping
in OO languages, polymorphic instantiation in ML languages,
existence-of-a-function... Here it will be a not-too-well-defined
subtyping relation. We also write (+) for (≥) and (-) for (≤))
In practice it suffices to check that "positive occurences" get a (+)
or a (=) and that "negative" occurences get a (-) or a (=).
Remark that when we define a new generative type (T ᾱ), we can
mostly pick any variance we want (in particular impose
invariance everywhere), as long as it is "more restrictive" than the
underlying variance. For soundness we must have that
T ᾱ ≤ T ᾱ' entails τ̄ ≤ τ̄'
indeed,
τ̄ τ̄'
| ∧
| K | \(K x̄) → x̄
| |
v ≤ |
T ᾱ ——————> T ᾱ'
Variance in a type expression; variance is a compositional property.
# Why I care about variance
Value restriction
let x = ref []
does *not* have type (∀α. α list ref)
two known problematic cases:
- expressions that never return
- expressions that build polymorphic data structures
let li = (fun x -> x) []
This last case happens in real life through abstraction barriers:
module Expr : sig
type 'a t
val inject : 'a -> 'a t
end = struct
type 'a t = 'a
let inject x = x
end
let empty = Expr.inject []
Relaxed value restriction
Generalize values, or type variables that only occur in covariant
positions.
Simple safety argument, solves the case of expressions that build
data structures
Having sufficient covariance is important in practice for OCaml
library programmers.
# What GADTs are
a datatype T ᾱ defined by constructors of the form:
K : ∀β̄. (τ̄ → T σ̄)
or, equivalently
K : ∀α ∀β̄ [ᾱ = σ̄] τ̄ → T ᾱ
or, equivalently
K : ∀α (∃β̄ [ᾱ = σ̄] τ̄) → T ᾱ
A good example:
type expr α =
| Val : α → expr α
| Int : int → expr int
| Prod : expr β * expr γ -> (β * γ) expr
# Variance through categorical glasses
Observation from Neil Ghani and Patricia Johann:
a type with constructor
| Prod : ∀α∀βγ[α = β*γ] expr β * expr γ -> α expr
does not look like a functor, how should we write
map : (α → α') → (expr α → expr α')
α of the form β * γ does not imply that
f : (α → α') is of the form (f₁ : β → β', f₂ : γ → γ') for some β',γ'
?
=> they consider it a functor from the discrete category |C| to C:
the only arrows in |C| are identities, so everyting is a functor.
The idea of this talk, through categorical glasses:
If one instead takes the category C≤ of C with subtyping relations
as arrows, one gets a richer structure where (α expr) may still be
a functor (covariant or contravariant).
Indeed consider (β * γ) ≤ α': if C is the OCaml type system, we
can deduce that α is of the form β' * γ' with β≤β', γ≤γ'.
# Life is not all good : two counter-examples
type eq (=α, +β) =
| Refl : eq (α,α)
(Explanation of private types: pint ≤ int, and more generally we have
private σ ≨ σ)
type pint = private int
type expr +α =
| PInt : pint -> expr pint
Conservative OCaml solution:
instantiated types must be invariant
Need a serious soundness proof to go any further.
# The soundness argument : Simonet & Pottier
More general formulation of *guarded* ADTs with constraints D
K : ∀ᾱ (∃β̄[D] τ̄) → T ᾱ
Soundness requirement:
T ᾱ ≤ T ᾱ' must entail (∃β̄ [D] τ̄) ≤ (∃β̄' [D'] τ̄')
or, equivalently
T ᾱ ≤ T ᾱ' ∧ D must entail ∃β̄'. D' ∧ (τ̄ ≤ τ̄')
that is, if we have assigned a variance for (T ᾱ), this
constructor can only be accepted if this requirement is met:
(∀i. αi ≤i α'i) ∧ D must entail ∃β̄'. D' ∧ (τ̄ ≤ τ̄')
For example, on the
Prod : ∀α ∀βγ[α=β*γ] β expr * γ expr → α expr
constructor, this gives
α ≤ α' ∧ α = β*γ must entail ∃βγ. α' = β*γ ∧ (expr β ≤ expr β') ∧ ..γ..
in particular β*γ≤α' must entail α' =: β'*γ' for this constructor to
be well-typed under this variance annotation.
How can the type system check this constraint?
# An equivalent, checkable criterion for the equality case
K : ∀ᾱ (∃β̄[αi = Ti(β̄)] τ̄) → T ᾱ
Decomposition of the criterion:
parameters
——————————
T ᾱ ≤ T ᾱ' ∧ D must entail ∃β̄'. D' ∧ (τ̄ ≤ τ̄')
——————
types
In types, life would be good if the the D were independent
(no β occurs in two equality constraint) => independent
characterization + non-interference criterion.
1. upward/downward closure:
αi ≤i α'i ∧ αi = Ti(β̄) must entail ∃β̄'. α'i = Ti(β̄)
2. non-interference
if a β appears in several Ti(β̄), all its occurences must be
invariant in (T (T₁(β̄),T₂(β̄),...))
(draw picture of (T (T₁(β̄),T₂(β̄),...)) with ≤i and ≤i,iv)
3. constructor parameter variance
(∀i∀v βiv ≤i,iv β'iv) iff τ̄' ≤ τ̄'
# Closed world vs open world assumption
Can we assume upward/downward closure?
downward closure => no we can't, because of private types
upward closure: we can for non-private, non-extensible types
upward/downward is part of the semantic interface for a type; we
should be able to publish it through abstraction boundaries
But what if we add 'blind' types later? Closed-world vs. Open-world
assumption.
Idea: upward/downward assignations should forbid further extension
of the subtyping lattice at this point, just like 'final' classes in
OOP.
# A totally open solution
Inspired by the move from logical relations to kripke logical
relations (and a lot of similar ideas), and Simonet&Pottier
generalization to arbitrary constraints:
Move from
type expr α =
| Val : α → expr α
| Int : int → expr int
| Prod : expr β * expr γ -> (β * γ) expr
that is
type expr α =
| Val : ∀α∀β[α=β] β → expr α
| Int : ∀α[α=int] int → expr α
| Prod : ∀α∀βγ[α=β*γ] expr β * expr γ -> α expr
to the different type
type expr α =
| Val : ∀α∀β[α≥β] β → expr α
| Int : ∀α[α≥int] int → expr α
| Prod : ∀α∀βγ[α≥β*γ] expr β * expr γ -> α expr
This is obviously covariant. The downside is that we get weaker
hypotheses when destructing elements at that type.
Happily, one can still write `eval : expr α → α`:
eval :: expr α → α
eval (Val β (α≥β) (v::β)) = (v :: β ≤ α)
eval (Int (α≥int) (n::int)) = (n :: int ≤ α)
eval (Prod β γ (α≥β*γ) (b,c)) = ((eval b, eval c) :: β*γ ≤ α)
Is this sufficient in pratice? I suspect it is, and this is
orthogonal to the upward/downward closure considerations (which can
be considered as a way to regain equalities from weaker
subtyping hypotheses).
However, this solution is problematic in practice, as current type
system engines are very good at unification (equalities) and much
less used to manipulating subtyping hypotheses. Type inference in
particular is likely to be more difficult or at least to require
more changes to the type system, which is problematic from
a pragmatic point of view.