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.