bearophile via Digitalmars-d
2014-10-12 16:21:49 UTC
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.
bearophile
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.
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,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.<
bearophile