digitalmars.D - Refined types [almost OT]
- bearophile (43/54) Oct 12 2014 A series of small OCaML projects that implement bare-bones type
- Meta (15/15) Oct 12 2014 On Sunday, 12 October 2014 at 16:21:50 UTC, bearophile wrote:
- bearophile (7/10) Oct 12 2014 If you are using refined types, and D is somewhat assuming they
- Meta (4/14) Oct 12 2014 It's not possible to issue a compile-time error for runtime
- Timon Gehr (3/20) Oct 12 2014 Yes it is. Why wouldn't it be? Values needn't be completely determined
- Meta (4/6) Oct 12 2014 They do if you want to check, for example, n < 3. D doesn't
- Timon Gehr (2/7) Oct 12 2014 (bearophile isn't discussing current language features.)
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
Oct 12 2014
On Sunday, 12 October 2014 at 16:21:50 UTC, bearophile wrote:
What happens if one of these conditions fails? Is an exception
thrown? Note that you can also sort of do this using template
constraints, but that of course only works at compile time:
double get2dimensional(int n, int m, int i, int j, double[] arr)()
if (n >= 0
&& m >= 0
&& 0 <= i
&& i < m
&& 0 <= j
&& j < n
&& arr.length == m * n)
{
return arr[i * n + j];
}
Oct 12 2014
Meta:On Sunday, 12 October 2014 at 16:21:50 UTC, bearophile wrote: What happens if one of these conditions fails? Is an exception thrown?If you are using refined types, and D is somewhat assuming they are refinements of those types, and one of those condition fails, then you surely have a compile-time type error, because those conditions are an intrinsic part of those type definition. Bye, bearophile
Oct 12 2014
On Sunday, 12 October 2014 at 19:36:35 UTC, bearophile wrote:Meta:It's not possible to issue a compile-time error for runtime arguments, though, and it can already be done in D using template constraints for compile-time arguments.On Sunday, 12 October 2014 at 16:21:50 UTC, bearophile wrote: What happens if one of these conditions fails? Is an exception thrown?If you are using refined types, and D is somewhat assuming they are refinements of those types, and one of those condition fails, then you surely have a compile-time type error, because those conditions are an intrinsic part of those type definition. Bye, bearophile
Oct 12 2014
On 10/12/2014 09:41 PM, Meta wrote:On Sunday, 12 October 2014 at 19:36:35 UTC, bearophile wrote:Yes it is. Why wouldn't it be? Values needn't be completely determined in order to be reasoned about.Meta:It's not possible to issue a compile-time error for runtime arguments, though,On Sunday, 12 October 2014 at 16:21:50 UTC, bearophile wrote: What happens if one of these conditions fails? Is an exception thrown?If you are using refined types, and D is somewhat assuming they are refinements of those types, and one of those condition fails, then you surely have a compile-time type error, because those conditions are an intrinsic part of those type definition. Bye, bearophileand it can already be done in D using template constraints for compile-time arguments.
Oct 12 2014
On Sunday, 12 October 2014 at 20:58:58 UTC, Timon Gehr wrote:Yes it is. Why wouldn't it be? Values needn't be completely determined in order to be reasoned about.They do if you want to check, for example, n < 3. D doesn't currently support the type of analysis necessary to implement something like that.
Oct 12 2014
On 10/13/2014 01:48 AM, Meta wrote:On Sunday, 12 October 2014 at 20:58:58 UTC, Timon Gehr wrote:(bearophile isn't discussing current language features.)Yes it is. Why wouldn't it be? Values needn't be completely determined in order to be reasoned about.They do if you want to check, for example, n < 3. D doesn't currently support the type of analysis necessary to implement something like that.
Oct 12 2014
On Monday, 13 October 2014 at 00:01:02 UTC, Timon Gehr wrote:On 10/13/2014 01:48 AM, Meta wrote:Ridiculous, I'm positive that D fully supports refined types in the language. Please check your facts.On Sunday, 12 October 2014 at 20:58:58 UTC, Timon Gehr wrote:(bearophile isn't discussing current language features.)Yes it is. Why wouldn't it be? Values needn't be completely determined in order to be reasoned about.They do if you want to check, for example, n < 3. D doesn't currently support the type of analysis necessary to implement something like that.
Oct 12 2014
On Monday, 13 October 2014 at 03:48:45 UTC, Meta wrote:On Monday, 13 October 2014 at 00:01:02 UTC, Timon Gehr wrote:Meta, go home, you're drunk. This technique is for statically checking certain conditions for the runtime values. This is what dependently typed languages do using some proofs (ATS is worth mentioning here, it solves linear integer conditions automatically using Presburger arithmetic and lets using more involved proofs to solve nonlinear ones) and languages with liquid/refined types do using an external SAT solver. Other than simple value range propagation D doesn't do anything like this. Arithmetic and conditions in the compile-time part of the language is not it.On 10/13/2014 01:48 AM, Meta wrote:Ridiculous, I'm positive that D fully supports refined types in the language. Please check your facts.On Sunday, 12 October 2014 at 20:58:58 UTC, Timon Gehr wrote:(bearophile isn't discussing current language features.)Yes it is. Why wouldn't it be? Values needn't be completely determined in order to be reasoned about.They do if you want to check, for example, n < 3. D doesn't currently support the type of analysis necessary to implement something like that.
Oct 13 2014
"Meta" <jared771 gmail.com> On Monday, 13 October 2014 at 08:20:15 UTC, thedeemon wrote:That was a joke.Ridiculous, I'm positive that D fully supports refined types in the language. Please check your facts.Meta, go home, you're drunk.
Oct 13 2014