Refined types [almost OT]

[bearophile via Digitalmars-d]

A series of small OCaML projects that implement bare-bones type 
systems. This implements a basic Refined Typing and explains the 
nice ideas:
https://github.com/tomprimozic/type-systems/tree/master/refined_types


This is one example (the unrefined underlying types are managed 
with a standard global inferencer):

function get_2dimensional(n : int if n >= 0, m : int if m >= 0,
                           i : int if 0 <= i and i < m, j : int if 
0 <= j and j < n,
                           arr : array[int] if length(arr) == m * 
n) {
   return get(arr, i * n + j)
}


In D syntax may become:

double get2dimensional(int n:        if n >= 0,
                        int m:        if m >= 0,
                        int i:        if 0 <= i && i < m,
                        int j:        if 0 <= j && j < n,
                        double[] arr: if arr.length == m * n) {
     return arr[i * n + j];
}


In theory pre-conditions could be used:


double get2D(in size_t row,   in size_t col,
              in size_t nRows, in size_t nCols,
              in double[] mat)
pure nothrow @safe @nogc in {
     assert(row < nRows);
     assert(col < nCols);
     assert(arr.length == nRows * nCols);
} body {
     return mat[row * nCols + col];
}


In practice I don't know if it's a good idea to mix the 
potentially very hard to verify pre-conditions with the limited 
but statically enforced type refinements. So perhaps using the ": 
if" syntax on the right of types is still the best option to use 
refinement typing in a D-like language. In this case the 
contracts keep being enforced at run-time, and can contain more 
complex invariants and tests that the refinement typing can't 
handle.

An interesting note on the limitations:

>The get_2dimensional function is particularly interesting; it 
>uses non-linear integer arithmetic, which is incomplete and 
>undecidable. Although Z3 can prove simple non-linear statements 
>about integers, such as x^2 = 0, it cannot prove that the array 
>is accessed within bound in the function get_2dimensional. 
>Instead, it has to convert the formula to real arithmetic and 
>use the NLSat solver [5]. Even though non-linear real arithmetic 
>is complete and decidable, this approach only works for certain 
>kinds of problems; for example, it cannot disprove equalities 
>that have real solutions but no integer ones, such as x^3 + y^3 
>== z^3 where x, y and z are positive.<

Bye,
bearophile