Search code examples
scalapath-dependent-type

Reestablish link between path dependent type and its parent at runtime?


I am experimenting with path dependent types. In my simple example I am using a Currency object to ensure that Money calculations can only be performed on Money of the same currency.

// Simple currency class
case class Currency(code: String, name: String, symbol: String) {

  // Money amounts in this currency
  // Operations are only supported on money of the same currency
  case class Money(amount: BigDecimal) {
    override def toString: String = s"$code $amount"

    val currency: Currency.this.type = Currency.this

    def +(rhs: Money): Money = Money(amount + rhs.amount)

    def -(rhs: Money): Money = Money(amount - rhs.amount)
  }
}

Using the above class simple calulations in the repl are straigh forward.

val e1 = Euro.Money(5)
val e2 = Euro.Money(9)
e1 + e2 // Compiles fine

val d1 = Dollar.Money(6)
d1 + e2 // Doesn't compile as expected

These are simple because the compiler can easily prove that e1 and e2 share a common currency. However proving that money instances share a common currency is much harder when I read a list of money amounts from a file or database. For instance I cannot see how to implement the collate function below.

trait CurrencyAndMonies {
  val currency: Currency
  val monies: List[currency.Money]
}

// Take a list of money in different currencies and group them by currency
// so their shared Currency type is available to static type checking
// in further calculations
def collate(Seq[Currency#Money]): List[CurrencyAndMonies] = ???

Is it possible to sort monies based on currency and reestablish the link between them? And if so how? I don't mind changing the signature or the way Money amounts are read from the database.


Solution

  • You can downcast:

    new CurrencyAndMonies {
      val currency = foo
      val monies = bars.map(_.asInstanceOf[currency.Money])
    }
    

    Group by Money#currency.

    The downcast is not runtime-checked, so you'll have to make sure the monetary value has the right currency (which you already do by grouping by currency), but it will compile.