Preface

There are 223 pages in my thesis...

so I will mainly focus on $D_{<:}$.

Preliminaries

Dependent Object Types (DOT)

  • DOT is a core calculus of Scala.
  • The first DOT was drafted in 2012 [Amin et al. 12].
  • Soundness proofs, however, only appear since 2016 [Amin et al. 16, Rompf and Amin 16, Rapoport et al. 17].

There are three core features:

  • path dependent types (x.A),
  • intersection types (T $\wedge$ U), and
  • $\mu$ types.

Let's focus on path dependent types.

Path Dependent Types (Account)


class NotEnoughBalance(amount : Long) extends RuntimeException

trait Account {
  type B <: Bank 
  def id : Int
  protected var _balance : Long
  def balance : Long = _balance
  def deposit(amount : Long) : Long = {
    _balance += amount
    balance
  }
  def withdraw(amount : Long) : Long = {
    if (amount > balance) {
      throw new NotEnoughBalance(amount)
    }
    _balance -= amount
    balance
  }
}
                        

Path Dependent Types (Bank)


trait Bank { self =>
  type A <: Account { type B = self.type }
  def lookupAccount(id : Int) : A
  def createAccount(initialBalance : Long = 0) : A
  def transfer(amount : Long, from : self.A,
    toBank : Bank, to : toBank.A) : Unit = {
    from.withdraw(amount)
    to.deposit(amount)
  }
}
                        

Note that to has type toBank.A which depends on a previous input.

Path Dependent Types (Example)


object BankOfWaterloo extends Bank { /* ... */ }
object WaterlooBank extends Bank { /* ... */ }
val david = BankOfWaterloo.createAccount(200)
val elly = WaterlooBank.createAccount(300)
                        

def transfer(amount : Long, from : self.A,
  toBank : Bank, to : toBank.A) : Unit
                        
BankOfWaterloo.transfer(10, david, WaterlooBank, elly)

This program transfers 10 dollars from David to Elly.

It type checks as David is with Bank of Waterloo and Elly is with Waterloo Bank.


BankOfWaterloo.transfer(10, david, BankOfWaterloo, ellyelly)
                                                   ^^^^
                            

What about this program?

Notice that Elly is with Waterloo Bank so she has type WaterlooBank.A and the program will be rejected.

Path depedent types are powerful and flexible, but...

How do we type check path dependent types?

  • Is it subtyping decidable with the presence of path dependent types?
  • If not, what is a decidable fragment?

$D_{<:}$ and Decidability Analysis

$D_{<:}$ is the simplest calculus in the DOT calculi family. It has only path depedent types out of the three core features.

The idea is to show that a complete type checking algorithm is impossible, i.e. type checking is undecidable.

Definition of $D_{<:}$

$$\dfrac{ }{\Gamma \vdash T <: \top}\text{Top}$$
$$\dfrac{ }{\Gamma \vdash \bot <: T}\text{Bot}$$
$$\dfrac{ }{\Gamma \vdash T <: T}\text{Refl}$$
$$\dfrac{\Gamma \vdash S_2 <: S_1 \quad \Gamma \vdash U_1 <: U_2}{\Gamma \vdash \{ A : S_1 .. U_1 \} <: \{ A : S_2 .. U_2 \}}\text{Bnd}$$
$$\dfrac{\Gamma \vdash S_2 <: S_1 \quad \Gamma;x : S_2 \vdash U_1 <: U_2}{\Gamma \vdash \forall(x : S_1)U_1 <: \forall(x : S_2)U_2}\text{All}$$
$$\dfrac{\Gamma \vdash \Gamma(x) <: \{A : S .. \top\}}{\Gamma \vdash S <: x.A}\text{Sel1}$$
$$\dfrac{\Gamma \vdash \Gamma(x) <: \{A : \bot .. U\}}{\Gamma \vdash x.A <: U}\text{Sel2}$$
$$\dfrac{\Gamma \vdash S <: T \quad \Gamma \vdash T <: U}{\Gamma \vdash S <: U}\text{Trans}$$

Reduction

For two decision problems $Q(x)$ and $P(x)$, $Q \le P$ if there exists a mapping $M$ such that $Q(x)$ outputs yes iff $P(M(x))$ outputs yes.
To show $D_{<:}$ is undecidable:

  1. find an undecidable problem $Q$ to reduce from,
  2. find a right mapping $M$, and
  3. show the if-and-only-if proof.

An Attempt: Reduction from $F_{<:}$ [Amin et al. 16]

$$\dfrac{ }{\Gamma \vdash T <: \top}\text{F-Top}$$
$$\dfrac{ }{\Gamma \vdash X <: X}\text{F-VarRefl}$$
$$\dfrac{X <: T \in \Gamma \quad \Gamma \vdash T <: U}{\Gamma \vdash X <: U}\text{F-Tvar}$$
$$\dfrac{\Gamma \vdash S_2 <: S_1 \quad \Gamma;X <: S_2 \vdash U_1 <: U_2}{\Gamma \vdash \forall X <: S_1 .U_1 <: \forall X <: S_2.U_2}\text{F-All}$$
$$\dfrac{\Gamma \vdash S_2 <: S_1 \quad \Gamma \vdash U_1 <: U_2}{\Gamma \vdash S_1 \to U_1 <: S_2 \to U_2}\text{F-Fun}$$
[Pierce 92] $F_{<:}$ subtyping is undecidable.
$$\begin{align} M(\top) &= \top \\ M(X) &= x_X.A \\ M(S \to U) &= \forall(x : M(S))M(U) \\ M(\forall X<:S .U) &= \forall(x_X : \{A : \bot .. M(S)\})M(U) \\ M(\Gamma) &= \{ x_X : \{ A : \bot .. M(T) \} | X <: T \in \Gamma \} \end{align}$$
[Amin et.al. 16] If an $F<:$ judgment $\Gamma \vdash S <: U$ holds, then the $D_{<:}$ judgment $M(\Gamma) \vdash M(S) <: M(U)$ holds.
Problem: Reduction is an if-and-only-if proof!
In fact, the other direction does not hold!
$$\begin{align} M(\top) &= \top \\ M(X) &= x_X.A \end{align}$$
$$\begin{align} M(S \to U) &= \forall(x : M(S))M(U) \\ M(\forall X<:S .U) &= \forall(x_X : \{A : \bot .. M(S)\})M(U) \end{align}$$

Consider a rejected judgment in $F_{<:}$: $\vdash (\top \to \top) <: (\forall X <: \top. \top)$.

$$\begin{align} M(\top \to \top) &= \forall(x : \top)\top \\ M(\forall X<:\top .\top) &= \forall(x_X : \{A : \bot .. \top\})\top \\ \end{align}$$ But in $D_{<:}$, they have a subtyping relation concluded by All! $$ \dfrac{\vdash \{A : \bot .. \top\} <: \top \text{(Top)} \quad x : \{A : \bot .. \top\} \vdash \top <: \top \text{(Refl)} }{\vdash (\forall(x : \top)\top) <: (\forall(x_X : \{A : \bot .. \top\})\top)}\text{All} $$

Solution: Reduction from $F^-_{<:}$

Definition of $F_{<:}$:

Removing function types ($\to$) from $F_{<:}$ gives $F^-_{<:}$.

$$\dfrac{ }{\Gamma \vdash T <: \top}\text{F-Top}$$
$$\dfrac{ }{\Gamma \vdash T <: T}\text{F-Refl}$$
$$\dfrac{X <: T \in \Gamma \quad \Gamma \vdash T <: U}{\Gamma \vdash X <: U}\text{F-Tvar}$$
$$\dfrac{\Gamma \vdash S_2 <: S_1 \quad \Gamma;X <: S_2 \vdash U_1 <: U_2}{\Gamma \vdash \forall X <: S_1 .U_1 <: \forall X <: S_2.U_2}\text{F-All}$$
$$\dfrac{\Gamma \vdash S_2 <: S_1 \quad \Gamma ; X <: S_2 \vdash U_1 <: U_2}{\Gamma \vdash S_1 \to U_1 <: S_2 \to U_2}\text{F-Fun}$$
$F^-_{<:}$ subtyping is undecidable.
The proof in Pierce 92 does not rely on function types.

A Phenomenon: Bad Bounds

Consider the following subtyping derivation:

Let $\Gamma = x : \{ A : S .. U\}$:

$$\dfrac{\dfrac{\Gamma\vdash \{ A : S .. U \} <: \{ A : S .. \top \}}{\Gamma \vdash S <: x.A}\text{Sel1} \quad \dfrac{\Gamma\vdash \{ A : S .. U \} <: \{ A : \bot .. U \}}{\Gamma \vdash x.A <: U}\text{Sel2}} {\Gamma\vdash S <: U}\text{Trans}$$
Bad bounds can prove subtyping between any two types given the right context!
Bad Bounds are consequences of the Sel1, Sel2 and Trans rules.

$D_{<:}$ Normal Form

$$\dfrac{ }{\Gamma \vdash T <: \top}\text{Top}$$
$$\dfrac{ }{\Gamma \vdash \bot <: T}\text{Bot}$$
$$\dfrac{ }{\Gamma \vdash T <: T}\text{Refl}$$
$$\dfrac{\Gamma \vdash S_2 <: S_1 \quad \Gamma \vdash U_1 <: U_2}{\Gamma \vdash \{ A : S_1 .. U_1 \} <: \{ A : S_2 .. U_2 \}}\text{Bnd}$$
$$\dfrac{\Gamma \vdash S_2 <: S_1 \quad \Gamma;x : S_2 \vdash U_1 <: U_2}{\Gamma \vdash \forall(x : S_1)U_1 <: \forall(x : S_2)U_2}\text{All}$$
$$\dfrac{\Gamma \vdash \Gamma(x) <: \{A : S .. \top\}}{\Gamma \vdash S <: x.A}\text{Sel1}$$
$$\dfrac{\Gamma \vdash \Gamma(x) <: \{A : \bot .. U\}}{\Gamma \vdash x.A <: U}\text{Sel2}$$
$$\dfrac{\Gamma \vdash S <: T \quad \Gamma \vdash T <: U}{\Gamma \vdash S <: U}\text{Trans}$$
$$\dfrac{\Gamma \vdash S <: T \quad \Gamma \vdash T <: U}{\Gamma \vdash S <: U}\text{Trans}$$
$$\dfrac{\Gamma \vdash \Gamma(x) <: \{A : S .. \top\} \quad \Gamma \vdash \Gamma(x) <: \{A : \bot .. U\}}{\Gamma \vdash S <: U}\text{BB}$$

This new definition of $D_{<:}$ is called $D_{<:}$ normal form.

$D_{<:}$ normal form admits transitivity.
$D_{<:}$ normal form is equivalent to the original $D_{<:}$.

$D_{<:}$ Normal Form (Cont'd)

$$\dfrac{\Gamma \vdash S <: T \quad \Gamma \vdash T <: U}{\Gamma \vdash S <: U}\text{Trans}$$
$$\dfrac{\Gamma \vdash \Gamma(x) <: \{A : S .. \top\} \quad \Gamma \vdash \Gamma(x) <: \{A : \bot .. U\}}{\Gamma \vdash S <: U}\text{BB}$$
Let's compare both rules:
  • The BB rule is a specialization of the Trans rule: it is just transitivity on a path type x.A.
  • The equivalence, however, indicates that both rules have the same expressive power.
  • $D_{<:}$ normal form is simpler because the BB rule forces $T = x.A$ for some $x$.
$D_{<:}$ subtyping is undecidable.

By reduction from $F^-_{<:}$.

Food for Thought

We want to maintain transitivity and drop bad bounds.

But in $D_{<:}$, one cannot achieve both at the same time.

How do we decide subtyping in $D_{<:}$?

Since it is undecidable, we can only target a fragment of admissble subtyping.

In my thesis, there are 2 decidable fragments of $D_{<:}$.

Kernel $D_{<:}$

The following is the definition of $D_{<:}$:

First let's remove the BB rule.

Then make the parameter type of the All rule identical.

This is the definition of kernel $D_{<:}$.

$$\dfrac{ }{\Gamma \vdash T <: \top}\text{Top}$$
$$\dfrac{ }{\Gamma \vdash \bot <: T}\text{Bot}$$
$$\dfrac{ }{\Gamma \vdash T <: T}\text{Refl}$$
$$\dfrac{\Gamma \vdash S_2 <: S_1 \quad \Gamma \vdash U_1 <: U_2}{\Gamma \vdash \{ A : S_1 .. U_1 \} <: \{ A : S_2 .. U_2 \}}\text{Bnd}$$
$$\dfrac{\Gamma \vdash S_2 <: S_1 \quad \Gamma;x : S_2 \vdash U_1 <: U_2}{\Gamma \vdash \forall(x : S_1)U_1 <: \forall(x : S_2)U_2}\text{All}$$
$$\dfrac{\Gamma;x : \bbox[border:2px solid red]{S} \vdash U_1 <: U_2}{\Gamma \vdash \forall(x : \bbox[border:2px solid red]{S})U_1 <: \forall(x : \bbox[border:2px solid red]{S})U_2}\text{All'}$$
$$\dfrac{\Gamma \vdash \Gamma(x) <: \{A : S .. \top\}}{\Gamma \vdash S <: x.A}\text{Sel1}$$
$$\dfrac{\Gamma \vdash \Gamma(x) <: \{A : \bot .. U\}}{\Gamma \vdash x.A <: U}\text{Sel2}$$
$$\dfrac{\Gamma \vdash \Gamma(x) <: \{A : S .. \top\} \quad \Gamma \vdash \Gamma(x) <: \{A : \bot .. U\}}{\Gamma \vdash S <: U}\text{BB}$$
Kernel $D_{<:}$ is decidable.

A Problem of Kernel $D_{<:}$

Consider

$$\dfrac{\Gamma;x : S \vdash U_1 <: U_2}{\Gamma \vdash \forall(x : S)U_1 <: \forall(x : S)U_2}\text{K-All}$$
The following subtyping is rejected by kernel $D_{<:}$:
$$x : \{A : \top .. \top\} \vdash \forall(y : x.A)\top <: \forall(y : \top)\top$$

Strong Kernel $D_{<:}$

Now let's lift the previous limitation.

The idea is to realize that subtyping can be achieved by more than one context!

Consider
$$\dfrac{\Gamma \vdash S_2 <: S_1 \quad \Gamma;x : S_2 \vdash U_1 <: U_2}{\Gamma \vdash \forall(x : S_1)U_1 <: \forall(x : S_2)U_2}\text{All}$$

Pierce 92 explained that this rule introduces undecidability.

But his proof only works if there is only one context.

$$\dfrac{\Gamma \vdash S_2 <: S_1 \bbox[border:2px solid red]{\dashv \Gamma} \quad \Gamma;x : S_1 \vdash U_1 <: U_2 \bbox[border:2px solid red]{\dashv \Gamma ; x : S_2}} {\Gamma \vdash \forall(x : S_1)U_1 <: \forall(x : S_2)U_2 \bbox[border:2px solid red]{\dashv \Gamma}}\text{SK-All}$$

Now the premises of this rule are simply structurally smaller subproblems.

Strong Kernel $D_{<:}$ (Cont'd)

$$\dfrac{ }{\Gamma_1 \vdash T <: \top \dashv \Gamma_2}\text{SK-Top}$$
$$\dfrac{ }{\Gamma_1 \vdash \bot <: T \dashv \Gamma_2}\text{SK-Bot}$$
$$\dfrac{ }{\Gamma_1 \vdash x.A <: x.A \dashv \Gamma_2}\text{SK-VRefl}$$
$$\dfrac{\Gamma_1 \vdash S_1 >: S_2 \dashv \Gamma_2 \quad \Gamma_1 \vdash U_1 <: U_2 \dashv \Gamma_2}{\Gamma_1 \vdash \{ A : S_1 .. U_1 \} <: \{ A : S_2 .. U_2 \} \dashv \Gamma_2}\text{SK-Bnd}$$
$$\dfrac{\Gamma_1 \vdash S_1 >: S_2 \dashv \Gamma_2 \quad \Gamma_1;x : S_1 \vdash U_1 <: U_2 \dashv \Gamma_2 ; x : S_2}{\Gamma_1 \vdash \forall(x : S_1)U_1 <: \forall(x : S_2)U_2 \dashv \Gamma_2}\text{SK-All}$$
$$\dfrac{\Gamma_1 \vdash \{A : S .. \top\} >: \Gamma_2(x) \dashv \Gamma_2}{\Gamma_1 \vdash S <: x.A \dashv \Gamma_2}\text{SK-Sel1}$$
$$\dfrac{\Gamma_1 \vdash \Gamma_1(x) <: \{A : \bot .. U\} \dashv \Gamma_2}{\Gamma_1 \vdash x.A <: U \dashv \Gamma_2}\text{SK-Sel2}$$
Strong kernel $D_{<:}$ is decidable.

Intersection Types $S \wedge U$

The previous results of $D_{<:}$ naturally extend to $D_{\wedge}$ which extends $D_{<:}$ with intersection types and data member types.

$D_{\wedge}$ Normal Form

There is also a normal form for $D_{\wedge}$, which extends $D_{<:}$ normal form with the following rules:
$$\dfrac{\Gamma \vdash T_1 <: T_2}{\Gamma \vdash \{a : T_1\} <: \{ a : T_2\}}\text{Fld}$$
$$\dfrac{\Gamma \vdash S <: T}{\Gamma \vdash S \wedge U <: T}\text{And-E1}$$
$$\dfrac{\Gamma \vdash U <: T}{\Gamma \vdash S \wedge U <: T}\text{And-E2}$$
$$\dfrac{\Gamma \vdash T <: S \quad \Gamma \vdash T <: U}{\Gamma \vdash T <: S \wedge U}\text{And-I}$$

Data member types are covariant.

Intersection types are monotone.

Intersection types are greatest lower bounds.

$D_{\wedge}$ is undecidable.

Strong Kernel $D_{\wedge}$

There is also a decidable strong kernel by extending strong kernel $D_{<:}$ with a straightforward adaptation:

$$\dfrac{\Gamma_1 \vdash T_1 <: T_2 \dashv \Gamma_2}{\Gamma_1 \vdash \{a : T_1\} <: \{ a : T_2\} \dashv \Gamma_2}\text{SK-Fld}$$
$$\dfrac{\Gamma_1 \vdash S <: T \dashv \Gamma_2}{\Gamma_1 \vdash S \wedge U <: T \dashv \Gamma_2}\text{And-E1}$$
$$\dfrac{\Gamma_1 \vdash U <: T \dashv \Gamma_2}{\Gamma_1 \vdash S \wedge U <: T \dashv \Gamma_2}\text{And-E2}$$
$$\dfrac{\Gamma_1 \vdash T <: S \dashv \Gamma_2 \quad \Gamma_1 \vdash T <: U \dashv \Gamma_2}{\Gamma_1 \vdash T <: S \wedge U \dashv \Gamma_2}\text{And-I}$$
Strong kernel $D_{\wedge}$ is decidable.

Other Calculi

I have not discussed $\mu$ types.

$\mu$ types define objects in a way typical in object oriented languages.

In my thesis, I defined $\mu$-DART and jDOT, in which I constructed an incomplete algorithm for each (c.f. Chapter 6 and 7).

However, with $\mu$ it is very difficult to prove the calculus undecidable!

Future Work

$$\dfrac{\Gamma \vdash \Gamma(x) <: \{A : S .. \top\} \quad \Gamma \vdash \Gamma(x) <: \{A : \bot .. U\}}{\Gamma \vdash S <: U}\text{BB}$$

Strong kernels simply remove the BB rule. What is a decidable fragment of bad bounds?

As we've seen, the BB rule is equivalent to transitivity so recovering a fragment of bad bounds recovers a fragment of transitivity, which is a desirable property.

It is even unclear at this point whether the BB rule introduces undecidability!

Summary

features name decidable?
bad bounds full All
intersections $\mu$ types
yes yes
no no $D_{<:}$ no
no no no no (strong) kernel $D_{<:}$ yes
no yes no no $D_{<:}$ without Trans no
yes yes yes no $D_{\wedge}$ no
no no yes no strong kernel $D_{\wedge}$ yes
yes/no yes/no no yes $\mu$DART unknown
yes/no yes/no yes yes DOT unknown
yes/no yes/no yes yes jDOT unknown

Thanks for Your Attention

References:

[Pierce 92] Benjamin C. Pierce. 1992. Bounded quantification is undecidable. In Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '92).

[Amin et al. 12] Nada Amin, Adriaan Moors & Martin Odersky, FOOL'12: 19th International Workshop on Foundations of Object-Oriented Languages, October 2012

[Amin et al. 16] Amin N., Grütter S., Odersky M., Rompf T., Stucki S. (2016) The Essence of Dependent Object Types.

[Rompf and Amin 16] Tiark Rompf and Nada Amin. 2016. Type soundness for dependent object types (DOT). SIGPLAN Not. 51, 10 (October 2016), 624-641.

[Rapoport et al. 17] Marianna Rapoport, Ifaz Kabir, Paul He, and Ondřej Lhoták. 2017. A simple soundness proof for dependent object types. Proc. ACM Program. Lang. 1, OOPSLA, Article 46 (October 2017), 27 pages.

[Pierce 92] Benjamin C. Pierce. 2002. Types and Programming Languages (1st ed.). The MIT Press.