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

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];
}

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

On Sunday, 12 October 2014 at 19:36:35 UTC, bearophile wrote:
> 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

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 10/12/2014 09:41 PM, Meta wrote:
> On Sunday, 12 October 2014 at 19:36:35 UTC, bearophile wrote:
>> 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
>
> It's not possible to issue a compile-time error for runtime arguments,
> though,

Yes it is. Why wouldn't it be? Values needn't be completely determined in order to be reasoned about.

> and it can already be done in D using template constraints for
> compile-time arguments.

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.

On 10/13/2014 01:48 AM, Meta wrote:
> 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.

(bearophile isn't discussing current language features.)

On Monday, 13 October 2014 at 00:01:02 UTC, Timon Gehr wrote:
> On 10/13/2014 01:48 AM, Meta wrote:
>> 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.
>
> (bearophile isn't discussing current language features.)

Ridiculous, I'm positive that D fully supports refined types in the language. Please check your facts.

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:
>> On 10/13/2014 01:48 AM, Meta wrote:
>>> 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.
>>
>> (bearophile isn't discussing current language features.)
>
> Ridiculous, I'm positive that D fully supports refined types in the language. Please check your facts.

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 Monday, 13 October 2014 at 08:20:15 UTC, thedeemon wrote:
>> Ridiculous, I'm positive that D fully supports refined types in the language. Please check your facts.
>
> Meta, go home, you're drunk.

That was a joke.