Preliminaries

Dependent Object Types (DOT)

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)

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

$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_{<:}$

Reduction

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

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

A Phenomenon: Bad Bounds

$D_{<:}$ Normal Form

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

Food for Thought

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_{<:}$

A Problem of Kernel $D_{<:}$

Consider

Strong Kernel $D_{<:}$

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

Intersection Types $S \wedge U$

$D_{\wedge}$ Normal Form

Data member types are covariant.

Intersection types are monotone.

Intersection types are greatest lower bounds.

Strong Kernel $D_{\wedge}$

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