Refinement Types

Overview

  • Well-typed programs can still go wrong
    • Divison by zero: The fact that a divisor is an int does not remove the possibility of a run-time division by zero error
    • Buffer overflows: The fact that an array or string index is an int does not remove the possiblity of a segmentation fault from out-of-bounds access
    • Logic bugs: With classical types we can insure that a data structure contains suitable (could be int) fields for holding day, month and year. But no guarantee that day is actually a valid day for the given month and year
  • Refinement types allows us to enrich the type system with predicates to narrow down the set of values described by a type
  • While an int can be any integer value, we can define a refined type that describes only non-negative integer values:
type nat = int[v| 0 <= v]
  • The combination of types and predicates allows for contracts that describe legal inputs and outputs of functions:
val size : x:array(a) => nat[v| v = length(x)]
val get  : x:array(a) => [v| v < length(x)] => a
  • size(arr) ensures that the returned integer value is euql to the number of elements in arr
  • get(arr, i) requires that the index i is within the bounds of arr
  • Give these specifications, the type checker can guarantee at compile-time that all operations respect their contracts, that is, to ensure that all array accesses are safe at run-time

References