Path Dependent Types

Some sort of path-dependent type (whereby values can have type members) seems empirically useful in contracts. A general case where this issue arises is when a contract C defines some resource R; the simplest example of this pattern is a Money/Treasury contract, whereby a Treasury distributes currency (in practice, presumably with some underlying value).

owned contract Money {
  int value;
  /* assume that the ability to call this is restricted to the Treasury */
  protected Money(int v) {
    value = v;
  }

  /* when called on [m1], modifies [m1] to [m1'] and returns [m2],
   * such that [m2.value == amount] and [m1.value == m1'.value + m2.value].
   * If [amount > value], throws an exception. */
  transaction split(int amount) returns Money { ... }

  /* when called on [m1], consumes [m2] and modifies [m1] to [m1'],
   * such that [m1'.value == m1.value + m2.value]. */
  transaction merge(Money m2) { ... }
}

shared contract Treasury {
  Money reserves;

  /* the treasury will mint new money if it's out of money */
  transaction mint_new_money() {
    if (reserves.value == 0) {
      reserves.merge(new Money(10000));
    }
  }

  /* The treasury will give 1 Money to anyone who asks */
  transaction distribute_money() returns Money {
    return reserves.split(1);
  }
}

The above example is subtly problematic, however, because, although the Treasury contract can be constructed multiple times, all Treasury contracts share the same Money type. This defies what one would intuitively expect, namely that each instance of Treasury has its own type of Money.

There are several high-level options for adding support for this in the language.

Option 1: Do Nothing

In the absence of any language specific mechanism for value-specific types, the programmer can still distinguish at run-time whether two instances of Money are the same by storing a reference back to their Treasury:

owned contract Money {
  int value;
  Treasury treasury;
  protected Money(int v, Treasury t) {
    value = v;
    treasury = t;
  }

  ...

  transaction merge(Money m2) {
    if (this.treasury != m2.treasury) throw;
    ...  
  }
}

Option 2: Compiler-Generated Dynamic Checks

First of all, to generate checks automatically, it must be known to the compiler which types are related in this way. One way to do this simply with nesting:

contract Treasury {
  contract Money {
    ...
  }
  ...
}

The desired semantics of this is that each instance of t : Treasury has its own distinct type t.Money (even though the implementation for t1.Money and t2.Money may be the same).

We can make two reasonable assumptions here that allow us to generate checks automatically:

1. Assume recursive references to other members of Money inside the definition of Money must be associated with the same Treasury instance as this.
2. Assume any reference to Money inside the definition of Treasury refers to this.Money.

Assumption (1) would allow roughly the following check to be generated in the Money contract:

contract Money {
  ...
  transaction merge(Money m2) {
    ...
  }
}

==>

contract Money {
  Treasury t;
  ...
  transaction merge(Money m2) {
    if (this.treasury != m2.treasury) throw;
    ...  
  }
}

On the other hand, assumption (2) would allow roughly the following:

contract Treasury {
  contract Money { ... }
  transaction take_back_money(Money m) { ... }
  ...
}

==>

contract Treasury {
  contract Money {
    Treasury t;
    ...
  }
  transaction take_back_money(Money m) {
    if (m.t != this) throw;
    ...
  }
  ...
}

In practice, these assumptions likely hold true for most contracts. In the presumably rare case where these assumptions don't hold, a user can define the contracts separately and manually add checks (Option 1).

With these generated checks, the Money and Treasury contracts are insulated from mistypings, in the sense that dynamic errors are transparent to these contracts, and are only seen by callers when they pass incorrectly typed arguments. For other contracts that depend on Money/Treasury, this is perhaps not the case:

contract C {
  state No_Money {
    transaction add_money(Money m) { ->One_Money with {m1 = m}; }
  }
  state One_Money {
    Money m1;
    transaction add_money(Money m) { ->Two_Money with {m2 = m}; }
  }
  state Two_Money {
    Money m1, m2;
    transaction combine_money() { ->One_Money with {m1 = m1.merge(m2)}; }
  }
}

In the state Two_Money, the values of m1 and m2 may be different Money types, but it's not until they are merged in the combine_money transaction that this will actually manifest as an error. Indeed, if this is the case, the contract becomes stuck in the Two_Money state, which is non-obvious from looking at the code itself.

A slight improvement to this scheme might allow a contract to specify statically which instance of Money they mean (perhaps at deployment time):

/* at deployment time, this might be disambiguated to be specifically [t.Money] for some [t] */
import Money
contract C {
  transaction t(Money m) {
    /* we can generate checks here that [m] is type [t.Money], much like inside of [Treasury] */
    ...
  }
}

Option 3: Statically Checked Types