\overline{1}

Subtyping

We start with a set of base types (Nat, Int, Bool, etc) and a set of type constructors (→, List, {}, ref etc). An ordering on the base types e.g.

Nat ⩽ Int ⩽ Float

induces an ordering on all types:

  ListNat  ⩽ ListInt
  Float→Float→Bool ⩽ Nat→Nat→Bool
  {a:Bool, b:Int}  ⩽ {b : Float}
  refInt  ⩽ refInt

Denotational Intuition: inclusion Operational Intuition: implicit coercion Examples:

• Record Types (and simple objects)

• Partially Abstract Types

• Local Types(?)

\overline{2}

Syntax

expressions e ::= x
|  λx.e
|  e_{1}e_{2}
|  let x = e_{1} in e_{2}
types τ ::= a
|  α
|  Tτ_{1} … τ_{n}
constrained type schemes κ ::= τ
|  ∀\overline{α}\C.σ
simple type schemes σ ::= τ
|  ∀α.σ
|  ∀α⩽τ.σ

\overline{3}

Subtype Orderings

The base subtype ordering will be written as a signature:

•  The empty signature
Σ′, a  unbounded base type
Σ′, a ⩽ τ bounded base type

• Each base type has at most one upper bound

• τ contains only base types occurring in Σ′. If τ is always a base type, the signature is atomic. Type operators have a polarity corresponding to their subtyping behaviour.

\begin{aligned}List & : & (+) \\ → & : & (−, +) \\ ref & : & (=) \end{aligned}

\frac{Σ ⊢ τ_{1} ⩽ τ_{2} Σ ⊢ τ_{2} ⩽ τ_{3}}{Σ ⊢ τ_{1} ⩽ τ_{3}} (Trans)
\frac{Σ ⊢ τ_{i} ⋄_{i}^{T} τ′_{i}}{Σ ⊢ Tτ_{1} … τ_{n} ⩽ Tτ′_{1} … τ′_{n}}  (Cons)

\overline{Σ ⊢ τ ⩽ τ}  (Taut)

\overline{Σ ⊢ a ⩽ Σ(a)}  (Var)

djs Type Inference with Subtypes November 28, 1996

\overline{4}
λ_{⩽}

Sufficient to add subsumption to the typing rules for λ_{→}.

\frac{Γ ⊢ e : τ_{1}  Σ ⊢ τ_{1} ⩽ τ_{2}}{Γ ⊢ e : τ_{2}}  (Sub)

with let-polymorphism…

if > : Float→Float→Bool
let fun max x y = if x > y then x else y
  in (max(3,4), max (3.0, 7.0)) end

max needs to have type ∀α\{α⩽Float}.α→α→α

so we’d better have typed it under the assumption

α⩽Float.

\overline{5}
ML_{⩽}

\frac{Γ(x) = σ}{Γ; C ⊢ x : σ}  (Var)
\frac{Γ; C_{1} ⊢ e : κ Σ; C_{2} ⊢ κ ⪯ τ}{Γ; C_{1} ⊢ e : τ}  (Inst)
\frac{Γ; C_{1} ∪ C_{2} ⊢ e : τ  \overline{α} ∩ F V (Γ) = ∅}{Γ; C_{1} ∪ C_{2} ⊢ ∀\overline{α}\C_{1}.τ} (Gen)
\frac{Γ, x:τ_{1}; C ⊢ e : τ_{2}}{Γ; C ⊢ λx.e : τ_{1}→τ_{2}}  (Abs)
\frac{Γ; C_{1} ⊢ e_{1} : τ_{1}→τ_{2}  Γ; C_{2} ⊢ e_{2} : τ_{2}}{Γ; C_{1} ∪ C_{2} ⊢ e_{1}e_{2} : τ_{2}} (App)
\frac{Γ; C_{1} ⊢ e_{1} : κ_{1}  Γ, x:κ_{1}; C_{2} ⊢ e_{2} : κ_{2}}{Γ; C_{1} ∪ C_{2} ⊢ let x = e_{1} in e_{2} : κ_{2}} (Let)

\frac{τ_{1} ⩽ τ_{2} ∈ C}{Σ; C ⊢ τ_{1} ⩽ τ_{2}}  (Hyp)

Σ; C ⊢ ∀\overline{α}\C′.τ_{1} ⪯ τ_{2} if there are types \overline{τ} such that Σ; C ⊢ [\overline{τ}/\overline{α}]c for all c ∈ C′, and Σ; C ⊢ [\overline{τ}/\overline{α}]τ_{1} ⩽ τ_{2}.

\overline{6}

Type Inference for ML_{⩽}

Generate both a type and a constraint set.

\frac{Γ(α) = ∀\overline{α}\C.τ  \overline{β} fresh}{Γ; [\overline{β}/\overline{α}]C ⊢ α : κ}  (Var)
\frac{Γ, x:τ_{1}; C ⊢ e : τ_{2}}{Γ; C ⊢ λx.e : τ_{1}→τ_{2}}  (Abs)
\frac{\begin{matrix}Γ; C_{1} ⊢ e_{1} : τ_{1} \\ Γ; C_{2} ⊢ e_{2} : τ_{2} \\ α ∉ F V (C) ∪ F V (Γ) \end{matrix}}{Γ; C_{1} ∪ C_{2} ∪ \{τ_{1} ⩽ τ_{2}→α\} ⊢ e_{1}e_{2} : α} (App)
\frac{\begin{matrix}Γ; C_{1} ⊢ e_{1} : τ_{1} \\ \overline{α} = F V (C_{1}) ∪ F V (τ_{1}) − F V (Γ) \\ Γ, x:∀\overline{α}\C_{1}.τ; C_{2} ⊢ e_{2} : τ_{2} \end{matrix}}{Γ; C_{1} ∪ C_{2} ⊢ let x = e_{1} in e_{2} : τ_{2}} (Let)

The constraint set had better have a solution!

\overline{7}

Too many constraints

letrec filter =
  fun (f) fun (x)
    if empty x then []
    else if f (hd x)
      then cons (hd x) (filter f (tl x))
      else filter f (tl x);
> filter:
> All(
> 'a->'b->'d < 'c, 'b < List 'l, 'b < List 'e,
> 'b < List 't, 'b < List 'h, 'b < List 'o,
> 'l < 'k, List 'k < 'g, 'g < 'd,
> 'q < List 'k, List 'f < 'd, 'j < Bool,
> 'v < 'g, 'a < 'i->'j, 'n < 'p->'q,
> 'c < 'm->'n, 's < 'u->'v, 'c < 'r->'s
> ) 'a->'b->'d

\overline{8}

Reducing the constraint set

Simplification We reduce the number of constraints without changing the set of possible solutions. Powerful, Heuristic, Incomplete.

Automatic choice Automatically choose a particular solution of the constraints, usually the one which gives the least unconstrained type. Simple, but fails in many cases (max).

Coercion We allow the programmer to supply a bounded type scheme to say what type the function has.

letrec filter:
All(X) (X->Bool) -> List X -> List X  =
fun (f) fun (x)
 if empty x then []
 else if f (hd x)
   then cons (hd x) (filter f (tl x))
   else filter f (tl x);
> filter:
All(X) (X->Bool) -> List X -> List X

\overline{9}

Coercions

We generalise ML’s generic instance relation

Γ ⊢ σ_{1} ⪯ σ_{2}

“σ_{2} is a generic instance of σ_{1}” to

Σ ⊢ κ ⩽ σ

A Σ-instance of ∀\overline{α}\C.τ is an instantiation of \overline{α} by \overline{τ} such that Σ ⊢ [\overline{τ}/\overline{α}]c for all c ∈ C.

We could define Σ ⊢ κ ⪯ σ to mean “for any Σ-instance τ_{σ} of σ, there is a Σ-instance τ_{κ} of κ such that Σ ⊢ τ_{κ} ⩽ τ_{σ}”

But consider

Int ⊢ ∀α\{Int→Int⩽α}.α ⪯ ∀α⩽Int→Int.α

What happens if we want to extend the signature by

Nat ⩽ Int ?

So… Σ ⊢ κ ⪯ σ if “for any extension Σ′ of Σ, and any Σ′-instance τ_{σ} of σ, there is a Σ′-instance τ_{κ} of κ such that Σ′ ⊢ τ_{κ} ⩽ τ_{σ}”

\overline{10}

Testing the instance relation

Proposition. Suppose σ is of the form ∀α_{1}(⩽τ_{1}) … ∀α_{n}(⩽τ_{n}).τ_{σ}. Let Σ′ = Σ, a_{1}(⩽τ_{1}), a_{2}(⩽[a_{1}/α_{1}]τ_{2}) . . .. Then

Σ ⊢ ∀\overline{α}\C.τ_{κ} ⪯ σ

iff there is a substitution θ : \overline{α}→dom(Σ′) such that Σ′ ⊢ θc for all c ∈ C ∪ \{τ_{κ} ⩽ [\overline{a}/\overline{α}]τ_{σ}\}

Consider the function

fun(x) fun(y) if x 0 > y 0 then x else y

which we might want to have type ∀α⩽Nat→Float.α→α→α Solution over atomic signatures isn’t enough.

\overline{11}

Constraints over Atomic Signatures

Proposition. A syntax-directed version of the subtyping order is obtained by replacing the rules Var, Trans, and Taut with

\frac{a ⩽ b ∈ Q_{Σ}}{Σ ⊢ a ⩽ b}  (Atom)

where Q_{Σ} is the transitive closure of Σ An Algorithm...

Tτ_{1} … τ_{n} ⩽ Tτ′_{1} … τ′_{n}, C ⇒ {τ_{i} ⋄_{i}^{T} τ′_{i}}, C
α ⩽ Tτ_{1} … τ_{n}, C  ⇒ {β_{i} ⋄_{i}^{T} τ_{i}}, [Tβ_{1} … β_{n}/α_{i}]C
Tτ_{1} … τ_{n} ⩽ α, C  ⇒ {β_{i} ⋄_{i}^{T} τ_{i}}, [Tβ_{1} … β_{n}/α_{i}]C

Come down to constraints between variables and base types only (or fail!)

Exponential time, but we can use similar techniques to test for satisfiability in O(n^{3}) time if Σ is a lattice (Tiuryn) or a tree (Benke).

\overline{12}

Non-atomic Signatures

Not quite so straightforward...

α ⩽ Tτ_{1} … τ_{n}, C ⇒ {β_{i} ⩽ τ_{i}}_{i}, [β_{i}/α_{i}]C

breaks completeness: α could stand for a base type.

Proposition. The following rules define a syntaxdirected version of the subtype ordering over a nonatomic signature:

\overline{Σ ⊢ a ⩽ a}  (TautVar)

\frac{Σ ⊢ Σ(a) ⩽ τ}{Σ ⊢ a ⩽ τ}  (Prom)

\frac{Σ ⊢ τ_{i} ⋄_{i}^{T} τ′_{i}}{Σ ⊢ Tτ_{1} … τ_{n} ⩽ Tτ′_{1} … τ′_{n}} (Cons)

But not syntax-directed enough: α ⩽ Tτ_{1} … τ_{n}?

\overline{13}

A complete class of reductions

a is a leaf in Σ if it doesn’t occur in the bound of any base type in Σ.

Proposition 1. If a is a leaf in Σ, and C has a solution over Σ, and a doesn’t occur in C, then C has a solution which doesn’t mention a.

Proposition 2. Σ ⊢ τ ⩽ τ′, and either a is a bounded leaf which occurs positively in τ or negatively in τ′ or a is an unbounded leaf then τ and τ′ are either both a, or of the form Tτ_{1} … τ_{n}, Tτ′_{1} … τ′_{n}.

Proposition 3. If a is a bounded leaf and there is no constraint τ_{1} ⩽ τ_{2} ∈ C in which a positively in τ_{1} or negatively in τ_{2}, then C has a solution only if [Σ(a)/a]C does.

So… pick a leaf a. If there’s a constraint satisfying the hypotheses of (2), we can reduce the constraint. Otherwise if a is bounded, we can substitute its bound using (3). Then the conditions of (1) are satisfied, so we can prune a from Σ.

Again we can test for satisfiability in O(n^{3}) time.

\overline{14}

First-class polymorphism

\overline{τ ⩽ τ}

\frac{σ′_{1} ⩽ σ_{1} σ_{2} ⩽ σ′_{2}}{σ_{1}→σ_{2} ⩽ σ′_{1} ⩽ σ′_{2}}

\frac{[τ/α]σ ⩽ σ′}{∀α.σ ⩽ σ′}

\frac{σ ⩽ σ′ α ∉ fv(σ)}{σ ⩽ ∀α.σ′}

To test the instance relation, transform into a mixed-prefix unification problem:

∀a∃α∀b∃β … τ_{1}=τ′_{1} ∧ τ_{2}=τ′_{2} …

If θ is a solution, θ(α) cannot contain b.

Analogously, mixed-prefix subtype problems:

∀a∃α∀b⩽a→a∃β … τ_{1}⩽τ′_{1} ∧ τ_{2}⩽τ′_{2} …

\overline{15}

Syntax

expressions e ::= x
|  λx.e
|  λx:σ.e
|  e_{1}e_{2}
|  let x = e_{1} in e_{2}
|  let x:σ = e_{1} in e_{2}
types τ ::= a
|  α
|  Tτ_{1} … τ_{n}
constrained type schemes κ ::= τ
|  ∀\overline{α}\C.σ
|  σ→κ
simple type schemes σ ::= τ
|  ∀α.σ
|  ∀α⩽τ.σ
|  σ_{1}→σ_{2}

\overline{16}

Combining the subtype relations

\overline{Σ ⊢ σ⩽σ}  (Taut)

\frac{Σ ⊢ σ_{1}⩽σ_{2}  Σ ⊢ σ_{2}⩽σ_{3}}{Σ ⊢ σ_{1}⩽σ_{3}}  (Trans)

\overline{Σ ⊢ a⩽Σ(a)}  (Var)

\frac{Σ ⊢ τ_{i} ⋄_{i}^{T} τ′_{i}}{Σ ⊢ T τ_{1} … τ_{n}⩽T τ′_{1} … τ′_{n}}  (Cons)

\frac{Σ ⊢ σ′_{1}⩽σ_{1}  Σ ⊢ σ_{2}⩽σ′_{2}}{Σ ⊢ σ_{1}→σ_{2}⩽σ′_{1}→σ′_{2}}  (Arrow)

\frac{Σ ⊢ [τ/α]σ_{1} ⩽ σ_{2}}{Σ ⊢ ∀α.σ_{1} ⩽ σ_{2}}  (∀-left)

\frac{Σ, a ⊢ σ_{1} ⩽ [a/α]σ_{2} a does not occur in σ_{1} or σ_{2}}{Σ ⊢ σ_{1} ⩽ ∀α.σ_{2}}  (∀-right)

\frac{Σ ⊢ [τ_{1}/α]σ_{1} ⩽ σ_{2}  Σ ⊢ τ_{1} ⩽ τ}{Σ ⊢ ∀α⩽τ.σ_{1} ⩽ σ_{2}}  (∀_{⩽}-left)

\frac{Σ, a⩽τ ⊢ σ_{1} ⩽ [a/α]σ_{2} a does not occur in σ_{1} or σ_{2}}{Σ ⊢ σ_{1} ⩽ ∀α⩽τ.σ_{2}}  (∀_{⩽}-right)

\overline{17}

Syntax-directed version

Replace Taut, Trans, and Var with

\overline{Σ ⊢ a ⩽ a}  (TautVar)

\frac{Σ ⊢ Σ(a) ⩽ σ}{Σ ⊢ a ⩽ σ}  (Promote)

A derivation is canonical if it contains no instance of ∀-right or ∀_{⩽}-right directly above an instance of Promote, ∀-left, or ∀_{⩽}-left.

Proposition. If there’s a derivation of Σ ⊢ σ_{1} ⩽ σ_{2}, there’s a canonical derivation.

In a canonical derivation, the choice of the last rule in a proof of Σ ⊢ σ_{1} ⩽ σ_{2} is determined by the form of σ_{1} and σ_{2}. To reconstruct the derivation, we just need to find suitable witnesses for the ∀-left and ∀_{⩽}-left rules.

We can do this by translating Σ ⊢ σ_{1} ⩽ σ_{2} into a mixed prefix subtype problem.

\overline{18}

Mixed Prefix Subtype Problems

The problem P(Σ, σ_{1}, σ_{2}) is S(Σ)I(σ_{1}, σ_{2}).

S(∅)  = ∅  (The empty prefix)
S(Σ, α)  = S(Σ)∀α
S(Σ, α⩽τ)  = S(Σ)∀α⩽τ
I(σ1 ⩽ ∀α.σ2)  = ∀a.I(σ1 ⩽ [a/α]σ2)  a fresh
I(σ1 ⩽ ∀α⩽τ.σ2)  = ∀a⩽τ.I(σ1 ⩽ [a/α]σ2)  a fresh
I(∀α.σ1 ⩽ σ2)  = ∃α.I(σ1 ⩽ σ2)  α not free in σ2

σ2 is not quantified

I(∀α⩽τ.σ1 ⩽ σ2) = ∃α.α ⩽ τ ∧ I(σ1, σ2) α not free in σ2

σ2 is not quantified

I(σ1→σ2 ⩽ σ′1→σ′2) = I(σ′1 ⩽ σ1) ∧ I(σ2 ⩽ σ′2)  if one of σ1→σ2,

σ′1→σ′2 is not a type

I(α ⩽ σ1→σ2) = ∃α1, α2.α ⩽ α1→α2 if σ1→σ2 is not a type
∧ I(σ1 ⩽ α1) ∧ I(α2 ⩽ σ2)
I(σ1→σ2 ⩽ α) = ∃α1, α2.α1→α2 ⩽ α σ1→σ2 is not a type
∧ I(σ1 ⩽ α1) ∧ I(α2 ⩽ σ2)
I(τ1 ⩽ τ2)  = τ1 ⩽ τ2
I(σ1 ⩽ σ2)  = Fail  otherwise

Proposition. There is a canonical derivation of Σ ⊢ σ_{1} ⩽ σ_{2} iff there is a solution of P(Σ, σ_{1}, σ_{2}).

Proposition. The set of reductions given earlier is also complete for mixed-prefix subtyping problems.

\overline{19}

Principality

• Mixed prefix unification problems have principal unifiers. Hence

• The instance relation has a principal substitutions property. Hence

• Expressions have principal types

Constraint problems in general do not have principal unifiers.

Proposition. Suppose σ_{1} and σ_{2} contain free variables \overline{α}.

If we eliminate the universal quantifiers in P(Σ, σ_{1}, σ_{2}) which aren’t in S(Σ) we obtain a constraint set C with the following properties.

1. If θ is a solution of C, then Σ ⊢ θσ_{1} ⩽ θσ_{2}.

2. If θ is such that Σ ⊢ θσ_{1} ⩽ θσ_{2}, then there’s a substitution θ′ on fv(C) − \overline{α} which solves C.

So we have principal constraint sets

\overline{20}
ML_{∀⩽}
\frac{Γ; C_{1} ⊢ e : κ Γ; C_{2} ⊢ κ ⩽ σ}{Γ; C_{1} ∪ C_{2} ⊢ e : σ}  (Sub)
\frac{\begin{matrix}Γ; C_{1} ∪ C_{2} ⊢ e_{1} : κ \\ \overline{α} ∩ (fv(Γ) ∪ fv_{Γ}(C_{2})) = ∅ \end{matrix}}{Γ; C_{1} ⊢ e_{1} : ∀\overline{α}\C_{2}.κ}  (Gen)
\frac{Γ(x) = κ}{Γ; C ⊢ x : κ}  (Taut)
\frac{Γ, x:τ; C ⊢ e : κ}{Γ; C ⊢ λx.e : τ→κ}  (Abs)
\frac{fv(σ) = α_{1} … α_{n} Γ, a_{1} … a_{n}, x:[a_{1}/α_{i}]σ; C_{1} ⊢ e : κ Γ, a_{1} … a_{n}; C_{2} ⊢ κ ⩽ σ′ for some σ′ Γ; a_{1} … a_{n} ⊢ C_{1} ∪ C_{2} solvable}{Γ; C_{1} ⊢ λx:σ.e : [α_{i}/a_{i}](σ→κ)} (TypedAbs)
\frac{Γ; C_{1} ⊢ e_{1} : σ→κ Γ; C_{2} ⊢ e_{2} : σ}{Γ; C_{2} ⊢ e_{1}e_{2} : κ}  (App)
\frac{\begin{matrix}Γ; ∅ ⊢ e_{1} : κ_{1} \\ Γ, x:κ_{1}; C_{1} ⊢ e_{2} : κ_{2} \\ strip κ_{1} = (\overline{α}, C_{2}, σ) \end{matrix}}{Γ; C_{1} ∪ C_{2} ⊢ let x = e_{1} in e_{2} : κ_{2}}  (Let)
\frac{Γ; C ⊢ e_{1} : σ σ ∈ σ(Γ)}{Γ; C ⊢ (e_{1} : σ) : σ} (Coerce)

Proposition. This system has principal types djs Type Inference with Subtypes November 28, 1996

\overline{21}

Connection with F_{⩽}

If we extend the system with type declarations newtype T v_{1} … v_{n} = σ

\frac{Γ, T:∀\overline{α}.σ→T \overline{α}; C ⊢ e : κ}{Γ; C ⊢ newtype T \overline{α} = σ in e : κ}  (Inj)
\frac{Γ(T) = ∀\overline{α}.σ→T \overline{α}}{Γ ⊢ T^{−1} : ∀\overline{α}.T \overline{α}→σ}  (Proj)

then we can map any derivation from the following variant of F_{⩽} into a derivation in ML_{∀⩽}.

\overline{Γ ⊢ α⩽Γ(α)}  (Var)
\overline{Γ ⊢ σ⩽σ}  (Taut)
\frac{Γ ⊢ σ_{1}⩽σ_{2}  Γ ⊢ σ_{2}⩽σ_{3}}{Γ ⊢ σ_{1}⩽σ_{3}}  (Trans)
\frac{Γ ⊢ σ′_{1}⩽σ_{1}  Γ ⊢ σ_{2}⩽σ′_{2}}{Γ ⊢ σ_{1}→σ_{2}⩽σ′_{1}→σ′_{2}}  (Arrow)
\frac{Γ, α ⊢ σ_{1}⩽σ_{2}}{Γ ⊢ ∀α.σ_{1}⩽∀α.σ_{2}}  (∀)
\frac{Γ ⊢ σ′_{2}⩽σ′_{1} Γ, α ⊢ σ_{1}⩽σ_{2}}{Γ ⊢ ∀(α ⩽ σ′_{1})σ_{1}⩽∀(α ⩽ σ′_{2})σ_{2}} (∀_{⩽})

djs Type Inference with Subtypes November 28, 1996