Support for "Undefined" Values & Types

[DavePearce]

The construction of arrays in templates leads to some annoying things. This provides the canonical example:

type Vector<T> is {
   T[] elements,
   int length
} where length >= 0 && length > |elements|

public function Vector(int capacity, T default) -> Vector<T>:
   return { elements: [default; capacity], length: 0 }

The problem is that we were required to provide a default value which is used to initialise the array generator. What we really want to do is write something like this:

public function Vector(int capacity, T default) -> Vector<T>:
   return { elements: [_; capacity], length: 0 }

where _ indicates an unknown value of the appropriate type (which, potentially, can be decided at template instantiation time). Some points:

• Ideally, want to statically check that undefined values are never used.

• In above, the type T|null for items gets us a long way to what we want, but null could be part of T ... hence, the potential for interference.

[DavePearce]

The suggest approach here is through the use of the `?' for values and types. The above would be rewritten as:

type Vector<T> is {
   (T?)[] elements,
   int length
} 
// length is within bounds
where 0 <= length && length < |elements|
// all elements below length are defined
where all { i in 0..length | elements[i] is T }

public function Vector(int capacity) -> Vector<T>:
   return { elements: [?; capacity], length: 0 }

public function get(Vector vec, int index) -> (T r)
requires 0 <= index && index < length:
   // Extract element with undefined type
   T? element = vec.elements[index]
   // Fall back on verifier to check it is defined
   assert element is T
   // Done
   return element   

The key thing here is the use of the assert statement to retype element. This forces the verifier to check this.

NOTE: one issue is how to check at run time that a type is defined or not?

[DavePearce]

@GraemeSmith you may be interested in this!