[Pre-Pitch] Runtime Type Guarantees

Evolution Pitches
11

The way I see it, you're sort-of attaching some restrictions to a type at the point where you're defining the value without really changing its nature. Let's call this a decorator.

decorator NonEmpty: Collection {
   // things that must be true at any time
   invariant {
      assert(!isEmpty)
   }
}

The decorator's main role is maintaining this invariant. To that end, it has to forbid all the mutating methods that could break that invariant, such as array.removeAll(). This is tricky since there can be any number of methods that could mutate the value and break the invariant. To ensure correctness the compiler should insert a call to the invariant after mutations, whether it is caused by a mutating method or by passing it inout to some other function. Statically forbidding some methods (such as removeAll) then becomes a nice convenience for catching some issues at compile-time but is not necessary for correctness.

Some notes about enforcing the invariant:

  • can't really enforce it with reference types since other references could have no decorators and mutate the object skipping the invariant
  • a remove method can put the collection in a non-empty state if you're removing the last element, but should nonetheless be allowed so you can remove elements except the last one
  • a removeAll method can be statically guarantied to fail the invariant so should be statically disallowed when possible

Once you can ensure the invariant is properly maintained, you can think about adding some affordances. It might look something like this:

decorator NonEmpty: Collection {
   // things that must be true at any time
   invariant {
      assert(!isEmpty)
   }

   // Add decorator to the function's return type.
   // The implementation isn't changed.
   // `invariant` is run on the returned value when applying NonEmpty to it.
   refine func map<T>(_ transform: (Element) -> T) -> NonEmpty Array<T>

   // don't change `func filter`:  can't guaranty the result is NonEmpty

   // Add decorator to the function's return type.
   // `NotNullable`'s `invariant` is run upon returning the value.
   refine var first: NotNullable Element?
   // Ideally, the compiler could see `NotNullable Element?` as equivalent 
   // to `Element` and allow an automatic conversion. Or better, it could 
   // allow us to write a plain `Element` as the return type as a special case.
}

Note that instead of reducing the number of checks, all this does is evaluate the invariant automatically at every turn so any correctness issue is caught early. This is likely to run slower unless the optimizer is very smart about it and can turn decorators added to function signatures to its advantage. But it makes it easier to express correctness constraints and it enables some affordances.

1 Like