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.