Sometimes the int or double type just doesn’t cut it. One way to enrich our type system is to add "refinement types" that allow constraints to be placed on values that a type may take. The notation is very familiar to anyone who has worked with set builder notation in mathematics (or list comprehensions in Python). One simple application of refinement types is to define specialized real and integer types, as below:

type Probability = {x:Num; 0 <= x <= 1 }
type PositiveInt = {x:Int; x >= 0}
type PositiveNum = {x:Num; x >= 0}
type Counting = {x:Int; x > 0}
type Odd = {x:Int; x > 0, x % 2 == 1}

These types should be quite readable. The compiler can use them in two ways. The first is to search at compile time for possible allowed inputs that would lead to violation of the constraints. This can be accomplished with an SMT solver. However, I do not expect all programs to be provable at compile time since this would require more upfront specification than many programmers want to provide. A second way to use refinement information is to generate runtime assertions. This is easy to implement as contracts that morloc generates in wrappers around functions calls. Of course there is a cost to runtime evaluation of contracts, but this can be minimzed by 1) only generating contracts where proofs are not possible or 2) by allowing contract evaluation to be toggled either globally or via pragmas in code.

Constraints may also be placed over functions. The following function signature fully specifies the transpose function:

transpose :: xs:[a]_{m,n} -> ys:[a]_{n,m} where
    all [xs[i,j] == ys[j,i]; i <- [1..m], j <- [1..n]]

This type signature enforces the constraint that xs[i,j] = ys[j,i] for all i and j. I may implement a shortcut where i and j are assumed to span indices if they are not defined, then we could write:

transpose :: xs:[a]_{m,n} -> ys:[a]_{n,m} where
    xs[i,j] == ys[j,i]

Where i and j represent all possible indices from 1 to m or 1 to j, respectively. This notation is elegant and reminiscent of mathematical notation, but I have not decided if it is practical for a programming language.

The transpose function is a cherry-picked example where a concise mathematical description fully describes the function. An important question to consider is exactly how general we want the constraint language to be. We could allow any term in the constraint language, then any function could be "fully specified", but then we will have layered a second implementation on top of the first. This may be worth doing. The type implementation would serve as a reference implementation for how the function ought to behave. But often having to implement everything twice would be more trouble than it is worth, so complete definitions should be optional. Also, allowing arbitrary functions to be used in the type definition will not in general be statically checkable, so they will instead have to serve as runtime contracts. And if the functions used in the runtime contracts themselves have contracts to fullfil, infinite contractual obligations could ensue.

One reasonable solution would be to only allow terms in the contract language for which we have an applicable model in our solver. This would limit the contract language to mostly arithmetic and logic. Further work on this topic will require a deep dive into what SMTs, for example Z3, are capable of handling.