Refined types [almost OT]

[thedeemon via Digitalmars-d]

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.